val lemma_ior_nth (n:pos) (x y:natN (pow2 n)) : Lemma
  (forall (m:_{m==pow2_norm n}) (i:nat{i < n}).{:pattern (nth #n (ior #m x y) i)}
    nth #n (ior #m x y) i == (nth #n x i || nth #n y i))
let lemma_ior_nth n x y =
  FStar.Classical.forall_intro (lemma_ior_nth_i n x y)
val lemma_ior_nth (n:pos) (x y:natN (pow2 n)) : Lemma
  (forall (m:_{m==pow2_norm n}) (i:nat{i < n}).{:pattern (nth #n (ior #m x y) i)}
    nth #n (ior #m x y) i == (nth #n x i || nth #n y i))
let lemma_ior_nth n x y =
FStar.Classical.forall_intro (lemma_ior_nth_i n x y)
Vale.Arch.TypesNative.fst.checked
prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Vale.Arch.TypesNative.fst
Prims.pos Vale.Arch.TypesNative.natN Prims.pow2 FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan Prims.eq2 Prims.bool Vale.Arch.TypesNative.nth Vale.Def.Types_s.ior Prims.op_BarBar Vale.Arch.TypesNative.lemma_ior_nth_i Prims.unit
module Vale.Arch.TypesNative
open FStar.Mul

let lemma_equal_nth n x y =
  UInt.to_vec_lemma_2 #n x y

let lemma_zero_nth n =
  let f (i:nat{i < n}) : Lemma (not (nth #n 0 i)) = UInt.zero_nth_lemma #n i in
  FStar.Classical.forall_intro f //(UInt.zero_nth_lemma #n)

let lemma_quad32_vec_equal a b =
  let Mkfour a0 a1 a2 a3 = a in
  let Mkfour b0 b1 b2 b3 = b in
  UInt.to_vec_lemma_2 #32 a0 b0;
  UInt.to_vec_lemma_2 #32 a1 b1;
  UInt.to_vec_lemma_2 #32 a2 b2;
  UInt.to_vec_lemma_2 #32 a3 b3;
  ()

#push-options "--z3rlimit 60 --z3refresh"
let lemma_iand_nth_i n x y i =
  reveal_iand n x y

let lemma_ixor_nth_i n x y i =
  reveal_ixor n x y

let lemma_ior_nth_i n x y i =
  reveal_ior n x y

let lemma_inot_nth_i n x i =
  reveal_inot n x

let lemma_ishl_nth_i n x y i =
  reveal_ishl n x y

let lemma_ishr_nth_i n x y i =
  reveal_ishr n x y

let lemma_iand_nth n x y =
  FStar.Classical.forall_intro (lemma_iand_nth_i n x y)

let lemma_ixor_nth n x y =
  FStar.Classical.forall_intro (lemma_ixor_nth_i n x y)
val lemma_ior_nth (n:pos) (x y:natN (pow2 n)) : Lemma
  (forall (m:_{m==pow2_norm n}) (i:nat{i < n}).{:pattern (nth #n (ior #m x y) i)}
    nth #n (ior #m x y) i == (nth #n x i || nth #n y i))

    n: Prims.pos ->
    x: Vale.Arch.TypesNative.natN (Prims.pow2 n) ->
    y: Vale.Arch.TypesNative.natN (Prims.pow2 n)
  -> FStar.Pervasives.Lemma
    (ensures
      forall (m: Prims.pos{m == Vale.Arch.TypesNative.pow2_norm n}) (i: Prims.nat{i < n}).
        {:pattern Vale.Arch.TypesNative.nth (Vale.Def.Types_s.ior x y) i}
        Vale.Arch.TypesNative.nth (Vale.Def.Types_s.ior x y) i ==
        (Vale.Arch.TypesNative.nth x i || Vale.Arch.TypesNative.nth y i))