val lemma_repeat_gen_vec:
    w:pos
  -> n:nat
  -> a:(i:nat{i <= w * n} -> Type)
  -> a_vec:(i:nat{i <= n} -> Type)
  -> normalize_v:(i:nat{i <= n} -> a_vec i -> a (w * i))
  -> f:(i:nat{i < w * n} -> a i -> a (i + 1))
  -> f_v:(i:nat{i < n} -> a_vec i -> a_vec (i + 1))
  -> acc_v0:a_vec 0 ->
  Lemma
  (requires (forall (i:nat{i < n}) (acc_v:a_vec i).
   (assert (w * (i + 1) <= w * n);
    normalize_v (i + 1) (f_v i acc_v) ==
    Loops.repeat_right (w * i) (w * (i + 1)) a f (normalize_v i acc_v))))
  (ensures
    normalize_v n (Loops.repeat_right 0 n a_vec f_v acc_v0) ==
    Loops.repeat_right 0 (w * n) a f (normalize_v 0 acc_v0))
let rec lemma_repeat_gen_vec w n a a_vec normalize_v f f_v acc_v0 =
  if n = 0 then begin
    Loops.eq_repeat_right 0 n a_vec f_v acc_v0;
    Loops.eq_repeat_right 0 (w * n) a f (normalize_v 0 acc_v0) end
  else begin
    let next_p = Loops.repeat_right 0 (n - 1) a_vec f_v acc_v0 in
    let next_v = Loops.repeat_right 0 (w * (n - 1)) a f (normalize_v 0 acc_v0) in

    calc (==) {
      Loops.repeat_right 0 (w * n) a f (normalize_v 0 acc_v0);
      (==) { Loops.repeat_right_plus 0 (w * (n - 1)) (w * n) a f (normalize_v 0 acc_v0) }
      Loops.repeat_right (w * (n - 1)) (w * n) a f next_v;
      (==) { lemma_repeat_gen_vec w (n - 1) a a_vec normalize_v f f_v acc_v0 }
      Loops.repeat_right (w * (n - 1)) (w * n) a f (normalize_v (n - 1) next_p);
      (==) { }
      normalize_v n (f_v (n - 1) next_p);
      (==) { Loops.unfold_repeat_right 0 n a_vec f_v acc_v0 (n - 1) }
      normalize_v n (Loops.repeat_right 0 n a_vec f_v acc_v0);
    } end
val lemma_repeat_gen_vec:
    w:pos
  -> n:nat
  -> a:(i:nat{i <= w * n} -> Type)
  -> a_vec:(i:nat{i <= n} -> Type)
  -> normalize_v:(i:nat{i <= n} -> a_vec i -> a (w * i))
  -> f:(i:nat{i < w * n} -> a i -> a (i + 1))
  -> f_v:(i:nat{i < n} -> a_vec i -> a_vec (i + 1))
  -> acc_v0:a_vec 0 ->
  Lemma
  (requires (forall (i:nat{i < n}) (acc_v:a_vec i).
   (assert (w * (i + 1) <= w * n);
    normalize_v (i + 1) (f_v i acc_v) ==
    Loops.repeat_right (w * i) (w * (i + 1)) a f (normalize_v i acc_v))))
  (ensures
    normalize_v n (Loops.repeat_right 0 n a_vec f_v acc_v0) ==
    Loops.repeat_right 0 (w * n) a f (normalize_v 0 acc_v0))
let rec lemma_repeat_gen_vec w n a a_vec normalize_v f f_v acc_v0 =
if n = 0
then
  (Loops.eq_repeat_right 0 n a_vec f_v acc_v0;
    Loops.eq_repeat_right 0 (w * n) a f (normalize_v 0 acc_v0))
else
  let next_p = Loops.repeat_right 0 (n - 1) a_vec f_v acc_v0 in
  let next_v = Loops.repeat_right 0 (w * (n - 1)) a f (normalize_v 0 acc_v0) in
  calc ( == ) {
    Loops.repeat_right 0 (w * n) a f (normalize_v 0 acc_v0);
    ( == ) { Loops.repeat_right_plus 0 (w * (n - 1)) (w * n) a f (normalize_v 0 acc_v0) }
    Loops.repeat_right (w * (n - 1)) (w * n) a f next_v;
    ( == ) { lemma_repeat_gen_vec w (n - 1) a a_vec normalize_v f f_v acc_v0 }
    Loops.repeat_right (w * (n - 1)) (w * n) a f (normalize_v (n - 1) next_p);
    ( == ) { () }
    normalize_v n (f_v (n - 1) next_p);
    ( == ) { Loops.unfold_repeat_right 0 n a_vec f_v acc_v0 (n - 1) }
    normalize_v n (Loops.repeat_right 0 n a_vec f_v acc_v0);
  }
Lib.Vec.Lemmas.fst.checked
prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Lib.Vec.Lemmas.fst
Prims.pos Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Prims.op_LessThan Prims.op_Addition Prims.op_Equality Prims.int Lib.LoopCombinators.eq_repeat_right Prims.unit Prims.bool FStar.Calc.calc_finish Prims.eq2 Lib.LoopCombinators.repeat_right Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Prims.op_Subtraction FStar.Calc.calc_init FStar.Calc.calc_pack Lib.LoopCombinators.repeat_right_plus Prims.squash Lib.Vec.Lemmas.lemma_repeat_gen_vec Lib.LoopCombinators.unfold_repeat_right Prims.op_Multiply
module Lib.Vec.Lemmas

#set-options ""
#push-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 \
  --using_facts_from '-* +Prims +FStar.Pervasives +FStar.Math.Lemmas +FStar.Seq -FStar.Seq.Properties.slice_slice \
    +Lib.IntTypes +Lib.Sequence +Lib.Sequence.Lemmas +Lib.LoopCombinators +Lib.Vec.Lemmas'"
val lemma_repeat_gen_vec:
    w:pos
  -> n:nat
  -> a:(i:nat{i <= w * n} -> Type)
  -> a_vec:(i:nat{i <= n} -> Type)
  -> normalize_v:(i:nat{i <= n} -> a_vec i -> a (w * i))
  -> f:(i:nat{i < w * n} -> a i -> a (i + 1))
  -> f_v:(i:nat{i < n} -> a_vec i -> a_vec (i + 1))
  -> acc_v0:a_vec 0 ->
  Lemma
  (requires (forall (i:nat{i < n}) (acc_v:a_vec i).
   (assert (w * (i + 1) <= w * n);
    normalize_v (i + 1) (f_v i acc_v) ==
    Loops.repeat_right (w * i) (w * (i + 1)) a f (normalize_v i acc_v))))
  (ensures
    normalize_v n (Loops.repeat_right 0 n a_vec f_v acc_v0) ==
    Loops.repeat_right 0 (w * n) a f (normalize_v 0 acc_v0))

    w: Prims.pos ->
    n: Prims.nat ->
    a: (i: Prims.nat{i <= w * n} -> Type) ->
    a_vec: (i: Prims.nat{i <= n} -> Type) ->
    normalize_v: (i: Prims.nat{i <= n} -> _: a_vec i -> a (w * i)) ->
    f: (i: Prims.nat{i < w * n} -> _: a i -> a (i + 1)) ->
    f_v: (i: Prims.nat{i < n} -> _: a_vec i -> a_vec (i + 1)) ->
    acc_v0: a_vec 0
  -> FStar.Pervasives.Lemma
      (requires
        forall (i: Prims.nat{i < n}) (acc_v: a_vec i).
          [@@ FStar.Pervasives.inline_let ]let _ = assert (w * (i + 1) <= w * n) in
          normalize_v (i + 1) (f_v i acc_v) ==
          Lib.LoopCombinators.repeat_right (w * i) (w * (i + 1)) a f (normalize_v i acc_v))
      (ensures
        normalize_v n (Lib.LoopCombinators.repeat_right 0 n a_vec f_v acc_v0) ==
        Lib.LoopCombinators.repeat_right 0 (w * n) a f (normalize_v 0 acc_v0))