val lemma_BitwiseXorWithZero (n:nat32) : Lemma (n *^ 0 == n)
let lemma_BitwiseXorWithZero n =
  lemma_ixor_nth_all 32;
  lemma_zero_nth 32;
  lemma_equal_nth 32 (n *^ 0) n
val lemma_BitwiseXorWithZero (n:nat32) : Lemma (n *^ 0 == n)
let lemma_BitwiseXorWithZero n =
lemma_ixor_nth_all 32;
lemma_zero_nth 32;
lemma_equal_nth 32 (n *^ 0) n
Vale.Arch.Types.fst.checked
Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Arch.Types.fst
Vale.Def.Words_s.nat32 Vale.Arch.TypesNative.lemma_equal_nth Vale.Arch.Types.op_Star_Hat Prims.unit Vale.Arch.TypesNative.lemma_zero_nth Vale.Arch.TypesNative.lemma_ixor_nth_all
module Vale.Arch.Types

open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Arch.TypesNative
open Vale.Lib.Seqs
open Vale.Def.Words_s
open Vale.Def.Words.Two
open FStar.Calc

let lemma_nat_to_two32 () =
  assert_norm (forall (x:nat64).{:pattern (nat_to_two 32 x)}
    nat_to_two 32 x == Mktwo (x % 0x100000000) (x / 0x100000000))

let lemma_BitwiseXorCommutative x y =
  lemma_ixor_nth_all 32;
  lemma_equal_nth 32 (x *^ y) (y *^ x)
val lemma_BitwiseXorWithZero (n:nat32) : Lemma (n *^ 0 == n)
n: Vale.Def.Words_s.nat32 -> FStar.Pervasives.Lemma (ensures n *^ 0 == n)