val is_prefix (#a: Type) (s ps: seq a) : Type0
val is_prefix (#a: Type) (s ps: seq a) : Type0
let is_prefix (#a:Type) (s:seq a) (ps: seq a): Type0 =
  length ps <= length s /\
  ps == prefix s (length ps)
module Zeta.SeqAux

open FStar.Seq

(* Legitimate values of an index of a sequence *)
inline_for_extraction
type seq_index (#a:Type) (s:seq a) = i:nat{i < length s}

(* Prefix of a sequence *)
val prefix (#a:Type) (s:seq a) (i:nat{i <= length s}): Tot (s':seq a{length s' = i})

let hprefix (#a:Type) (s:seq a{length s > 0}): seq a = 
  prefix s (length s - 1)

let telem (#a:Type) (s:seq a{length s > 0}): a =
  index s (length s - 1)

(* append a single element to the end of a sequence *)
let append1 (#a:Type) (s:seq a) (x:a): s':(seq a){length s' = length s + 1} =
  append s (create 1 x)

val prefix_slice (#a:Type) (s:Seq.seq a) (i:nat{i <= Seq.length s})
  : Lemma (Seq.equal (prefix s i) (Seq.slice s 0 i))

val lemma_prefix_index (#a:Type) (s:seq a) (i:nat{i <= length s}) (j:nat{j < i}):
  Lemma (requires (True))
        (ensures (index (prefix s i) j == index s j))
        [SMTPat (index (prefix s i) j)]

val lemma_prefix_prefix (#a:Type) (s:seq a) (i:nat{i <= length s}) (j:nat{j <= i}):
  Lemma (requires (True))
        (ensures (prefix (prefix s i) j == prefix s j))
        [SMTPat (prefix (prefix s i) j)]

val lemma_fullprefix_equal (#a:Type) (s:seq a):
  Lemma (requires (True))
        (ensures (prefix s (length s) == s))
        [SMTPat (prefix s (length s))]

val lemma_prefix_append (#a:Type) (s1 s2: seq a):
  Lemma (requires (True))
        (ensures (prefix (append s1 s2) (length s1) == s1))

let lemma_prefix1_append (#a:Type) (s: seq a) (x:a):
  Lemma (prefix (append1 s x) (length s) == s) =
  lemma_prefix_append s (create 1 x)

val lemma_hprefix_append_telem (#a:Type) (s: seq a{length s > 0}):
  Lemma (ensures (let s' = hprefix s in
                  let e = telem s in
                  s == append1 s' e))
        [SMTPat (hprefix s); SMTPat (prefix s (length s - 1))]

val lemma_prefix0_empty (#a:Type) (s: seq a):
Lemma (prefix s 0 == empty #a)

val lemma_prefix_create (#a:Type) (n:nat) (v:a) (i:nat{i <= n}) 
: Lemma (prefix (create n v) i == create i v)
/
prims.fst.checked FStar.Squash.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.SeqAux.fsti
s: FStar.Seq.Base.seq a -> ps: FStar.Seq.Base.seq a -> Type0
FStar.Seq.Base.seq Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.eq2 Zeta.SeqAux.prefix
let is_prefix (#a: Type) (s ps: seq a) : Type0 =
  
length ps <= length s /\ ps == prefix s (length ps)