val seq_of_list_append_lemma: #a:Type -> x:list a -> y:list a ->
  Lemma (let xy_lseq = Seq.seq_of_list FL.(x @ y) in
    Seq.slice xy_lseq 0 (FL.length x) == Seq.seq_of_list x /\
    Seq.slice xy_lseq (FL.length x) (FL.length x + FL.length y) == Seq.seq_of_list y)
let seq_of_list_append_lemma #a x y =
  let xy = FL.(x @ y) in
  let x_lseq = Seq.seq_of_list x in
  let y_lseq = Seq.seq_of_list y in
  let xy_lseq = Seq.seq_of_list xy in
  let x_len = FL.length x in
  let y_len = FL.length y in

  let lemma_x_lseq (i:nat{i < x_len}) : Lemma (Seq.index xy_lseq i == Seq.index x_lseq i) =
    list_append_index x y i in

  FStar.Classical.forall_intro lemma_x_lseq;
  Seq.lemma_eq_intro (Seq.slice xy_lseq 0 x_len) x_lseq;
  assert (Seq.slice xy_lseq 0 x_len == x_lseq);

  let lemma_y_lseq (i:nat{i < y_len}) :
    Lemma (Seq.index xy_lseq (x_len + i) == Seq.index y_lseq i) =
    list_append_index x y (x_len + i) in

  FStar.Classical.forall_intro lemma_y_lseq;
  Seq.lemma_eq_intro (Seq.slice xy_lseq x_len (x_len + y_len)) y_lseq;
  assert (Seq.slice xy_lseq x_len (x_len + y_len) == y_lseq)
val seq_of_list_append_lemma: #a:Type -> x:list a -> y:list a ->
  Lemma (let xy_lseq = Seq.seq_of_list FL.(x @ y) in
    Seq.slice xy_lseq 0 (FL.length x) == Seq.seq_of_list x /\
    Seq.slice xy_lseq (FL.length x) (FL.length x + FL.length y) == Seq.seq_of_list y)
let seq_of_list_append_lemma #a x y =
let xy = let open FL in x @ y in
let x_lseq = Seq.seq_of_list x in
let y_lseq = Seq.seq_of_list y in
let xy_lseq = Seq.seq_of_list xy in
let x_len = FL.length x in
let y_len = FL.length y in
let lemma_x_lseq (i: nat{i < x_len}) : Lemma (Seq.index xy_lseq i == Seq.index x_lseq i) =
  list_append_index x y i
in
FStar.Classical.forall_intro lemma_x_lseq;
Seq.lemma_eq_intro (Seq.slice xy_lseq 0 x_len) x_lseq;
assert (Seq.slice xy_lseq 0 x_len == x_lseq);
let lemma_y_lseq (i: nat{i < y_len}) : Lemma (Seq.index xy_lseq (x_len + i) == Seq.index y_lseq i) =
  list_append_index x y (x_len + i)
in
FStar.Classical.forall_intro lemma_y_lseq;
Seq.lemma_eq_intro (Seq.slice xy_lseq x_len (x_len + y_len)) y_lseq;
assert (Seq.slice xy_lseq x_len (x_len + y_len) == y_lseq)
Hacl.Spec.PrecompBaseTable.fst.checked
Spec.Exponentiation.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.Definition.fsti.checked Hacl.Impl.Exponentiation.Definitions.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.PrecompBaseTable.fst
Prims.list Prims._assert Prims.eq2 FStar.Seq.Base.seq FStar.Seq.Base.slice Prims.op_Addition Prims.unit FStar.Seq.Base.lemma_eq_intro FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Hacl.Spec.PrecompBaseTable.list_append_index FStar.List.Tot.Base.length Prims.op_Equality FStar.Seq.Base.length FStar.Seq.Properties.seq_of_list FStar.List.Tot.Base.op_At
module Hacl.Spec.PrecompBaseTable

open FStar.Mul
open Lib.IntTypes

module FL = FStar.List.Tot
module LSeq = Lib.Sequence

module LE = Lib.Exponentiation.Definition
module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation.Definitions

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

#push-options "--fuel 2"
val list_append_index1: #a:Type -> x:list a -> y:list a -> i:nat{i < FL.length x} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index x i)) (decreases (FL.length x))

let rec list_append_index1 #a x y i =
  match x with
  | [] -> ()
  | hd::tl -> if i = 0 then () else list_append_index1 tl y (i - 1)


val list_append_index2: #a:Type -> x:list a -> y:list a -> i:nat{FL.length x <= i /\ i < FL.length x + FL.length y} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index y (i - FL.length x))) (decreases (FL.length x))

let rec list_append_index2 #a x y i =
  match x with
  | [] -> ()
  | hd::tl -> list_append_index2 tl y (i - 1)
#pop-options


val list_append_index: #a:Type -> x:list a -> y:list a -> i:nat{i < FL.length x + FL.length y} ->
  Lemma (FL.(index (x @ y)) i ==
    (if i < FL.length x then FL.index x i else FL.index y (i - FL.length x)))

let list_append_index #a x y i =
  if i < FL.length x then list_append_index1 x y i else list_append_index2 x y i
val seq_of_list_append_lemma: #a:Type -> x:list a -> y:list a ->
  Lemma (let xy_lseq = Seq.seq_of_list FL.(x @ y) in
    Seq.slice xy_lseq 0 (FL.length x) == Seq.seq_of_list x /\
    Seq.slice xy_lseq (FL.length x) (FL.length x + FL.length y) == Seq.seq_of_list y)
x: Prims.list a -> y: Prims.list a
  -> FStar.Pervasives.Lemma
    (ensures
      (let xy_lseq = FStar.Seq.Properties.seq_of_list (x @ y) in
        FStar.Seq.Base.slice xy_lseq 0 (FStar.List.Tot.Base.length x) ==
        FStar.Seq.Properties.seq_of_list x /\
        FStar.Seq.Base.slice xy_lseq
          (FStar.List.Tot.Base.length x)
          (FStar.List.Tot.Base.length x + FStar.List.Tot.Base.length y) ==
        FStar.Seq.Properties.seq_of_list y))