val lemma_concat2:
    #a:Type0
  -> len0:size_nat
  -> s0:lseq a len0
  -> len1:size_nat{len0 + len1 <= max_size_t}
  -> s1:lseq a len1
  -> s:lseq a (len0 + len1) ->
  Lemma
    (requires
      sub s 0 len0 == s0 /\
      sub s len0 len1 == s1)
    (ensures s == concat s0 s1)
let lemma_concat2 #a len0 s0 len1 s1 s =
  Seq.Properties.lemma_split s len0;
  Seq.Properties.lemma_split (concat s0 s1) len0;
  Seq.lemma_eq_intro s (concat s0 s1)
val lemma_concat2:
    #a:Type0
  -> len0:size_nat
  -> s0:lseq a len0
  -> len1:size_nat{len0 + len1 <= max_size_t}
  -> s1:lseq a len1
  -> s:lseq a (len0 + len1) ->
  Lemma
    (requires
      sub s 0 len0 == s0 /\
      sub s len0 len1 == s1)
    (ensures s == concat s0 s1)
let lemma_concat2 #a len0 s0 len1 s1 s =
Seq.Properties.lemma_split s len0;
Seq.Properties.lemma_split (concat s0 s1) len0;
Seq.lemma_eq_intro s (concat s0 s1)
Lib.Sequence.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.Calc.fsti.checked
Lib.Sequence.fst
Lib.IntTypes.size_nat Lib.Sequence.lseq Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.max_size_t FStar.Seq.Base.lemma_eq_intro Lib.Sequence.concat Prims.unit FStar.Seq.Properties.lemma_split
module Lib.Sequence

open FStar.Mul
open Lib.IntTypes
open Lib.LoopCombinators

#set-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 --using_facts_from '-* +Prims +FStar.Pervasives +FStar.Math.Lemmas +FStar.Seq +Lib.IntTypes +Lib.Sequence'"

let index #a #len s n = Seq.index s n

let create #a len init = Seq.create #a len init

let concat #a #len0 #len1 s0 s1 = Seq.append s0 s1

let to_list #a s = Seq.seq_to_list s

let of_list #a l = Seq.seq_of_list #a l

let of_list_index #a l i =
  Seq.lemma_seq_of_list_index #a l i

let equal #a #len s1 s2 =
  forall (i:size_nat{i < len}).{:pattern (index s1 i); (index s2 i)} index s1 i == index s2 i

let eq_intro #a #len s1 s2 =
  assert (forall (i:nat{i < len}).{:pattern (Seq.index s1 i); (Seq.index s2 i)}
    index s1 i == index s2 i);
  Seq.lemma_eq_intro #a (to_seq s1) (to_seq s2)

let eq_elim #a #len s1 s2 =
  assert (forall (i:nat{i < len}).{:pattern (Seq.index s1 i); (Seq.index s2 i)}
    index s1 i == index s2 i);
  Seq.lemma_eq_elim #a s1 s2

let upd #a #len s n x = Seq.upd #a s n x

let member #a #len x l = Seq.count x l > 0

let sub #a #len s start n = Seq.slice #a s start (start + n)

let update_sub #a #len s start n x =
  let o =
    Seq.append
      (Seq.append (Seq.slice s 0 start) x)
      (Seq.slice s (start + n) (length s)) in
  Seq.lemma_eq_intro (Seq.slice o start (start + n)) x;
  o

let lemma_update_sub #a #len dst start n src res =
  let res1 = update_sub dst start n src in
  Seq.lemma_split (sub res 0 (start + n)) start;
  Seq.lemma_split (sub res1 0 (start + n)) start;
  Seq.lemma_split res (start + n);
  Seq.lemma_split res1 (start + n);
  Seq.lemma_eq_intro res (update_sub dst start n src)
val lemma_concat2:
    #a:Type0
  -> len0:size_nat
  -> s0:lseq a len0
  -> len1:size_nat{len0 + len1 <= max_size_t}
  -> s1:lseq a len1
  -> s:lseq a (len0 + len1) ->
  Lemma
    (requires
      sub s 0 len0 == s0 /\
      sub s len0 len1 == s1)
    (ensures s == concat s0 s1)

    len0: Lib.IntTypes.size_nat ->
    s0: Lib.Sequence.lseq a len0 ->
    len1: Lib.IntTypes.size_nat{len0 + len1 <= Lib.IntTypes.max_size_t} ->
    s1: Lib.Sequence.lseq a len1 ->
    s: Lib.Sequence.lseq a (len0 + len1)
  -> FStar.Pervasives.Lemma
      (requires Lib.Sequence.sub s 0 len0 == s0 /\ Lib.Sequence.sub s len0 len1 == s1)
      (ensures s == Lib.Sequence.concat s0 s1)