val repeat_induction: #a:Type -> n:nat{n > 0} -> f:( a -> Tot a) -> x:a -> Lemma
  (repeat n f x == f (repeat (n-1) f x))
let rec repeat_induction #a n f x =
  if n = 1 then ()
  else repeat_induction (n-1) f (f x)
val repeat_induction: #a:Type -> n:nat{n > 0} -> f:( a -> Tot a) -> x:a -> Lemma
  (repeat n f x == f (repeat (n-1) f x))
let rec repeat_induction #a n f x =
if n = 1 then () else repeat_induction (n - 1) f (f x)
Spec.Loops.fst.checked
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Spec.Loops.fst
Prims.nat Prims.b2t Prims.op_GreaterThan Prims.op_Equality Prims.int Prims.bool Spec.Loops.repeat_induction Prims.op_Subtraction Prims.unit
module Spec.Loops

#reset-options "--max_fuel 0"

val seq_map:
  #a:Type -> #b:Type ->
  f:(a -> Tot b) ->
  s:Seq.seq a ->
  Tot (s':Seq.seq b{Seq.length s = Seq.length s' /\
    (forall (i:nat). {:pattern (Seq.index s' i)} i < Seq.length s' ==> Seq.index s' i == f (Seq.index s i))})
    (decreases (Seq.length s))
let rec seq_map #a #b f s =
  if Seq.length s = 0 then
    Seq.empty
  else
    let s' = Seq.cons (f (Seq.head s)) (seq_map f (Seq.tail s)) in
    s'


val seq_map2:
  #a:Type -> #b:Type -> #c:Type ->
  f:(a -> b -> Tot c) ->
  s:Seq.seq a -> s':Seq.seq b{Seq.length s = Seq.length s'} ->
  Tot (s'':Seq.seq c{Seq.length s = Seq.length s'' /\
    (forall (i:nat). {:pattern (Seq.index s'' i)} i < Seq.length s'' ==> Seq.index s'' i == f (Seq.index s i) (Seq.index s' i))})
    (decreases (Seq.length s))
let rec seq_map2 #a #b #c f s s' =
  if Seq.length s = 0 then Seq.empty
  else
    let s'' = Seq.cons (f (Seq.head s) (Seq.head s')) (seq_map2 f (Seq.tail s) (Seq.tail s')) in
    s''

val repeat: #a:Type -> n:nat -> (f: a -> Tot a) -> a -> Tot a (decreases n)
let rec repeat #a n f x =
  if n = 0 then x else repeat (n-1) f (f x)

#reset-options "--initial_fuel 2 --max_fuel 2"

val repeat_induction: #a:Type -> n:nat{n > 0} -> f:( a -> Tot a) -> x:a -> Lemma
  (repeat n f x == f (repeat (n-1) f x))
val repeat_induction: #a:Type -> n:nat{n > 0} -> f:( a -> Tot a) -> x:a -> Lemma
  (repeat n f x == f (repeat (n-1) f x))
n: Prims.nat{n > 0} -> f: (_: a -> a) -> x: a
  -> FStar.Pervasives.Lemma (ensures Spec.Loops.repeat n f x == f (Spec.Loops.repeat (n - 1) f x))