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 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''
Spec.Loops.fst.checked
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Spec.Loops.fst
FStar.Seq.Base.seq Prims.b2t Prims.op_Equality Prims.nat FStar.Seq.Base.length Prims.int FStar.Seq.Base.empty Prims.bool FStar.Seq.Properties.cons FStar.Seq.Properties.head Spec.Loops.seq_map2 FStar.Seq.Properties.tail Prims.l_and Prims.l_Forall Prims.l_imp Prims.op_LessThan Prims.eq2 FStar.Seq.Base.index
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))
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))

    f: (_: a -> _: b -> c) ->
    s: FStar.Seq.Base.seq a ->
    s': FStar.Seq.Base.seq b {FStar.Seq.Base.length s = FStar.Seq.Base.length s'}
  -> Prims.Tot
    (s'':
      FStar.Seq.Base.seq c
        { FStar.Seq.Base.length s = FStar.Seq.Base.length s'' /\
          (forall (i: Prims.nat). {:pattern FStar.Seq.Base.index s'' i}
              i < FStar.Seq.Base.length s'' ==>
              FStar.Seq.Base.index s'' i == f (FStar.Seq.Base.index s i) (FStar.Seq.Base.index s' i)
          ) })