val for_all_array : f: (_: ty -> Prims.GTot Prims.bool) -> a: Util.ImmutableArray.array_t ty -> Prims.GTot Prims.bool
let for_all_array (#ty: Type) (f: ty -> GTot bool) (a: array_t ty) =
  for_all_range (array_len a) (fun i -> f (array_index a i))
module Util.ImmutableArray

open FStar.ImmutableArray
open Spec.List
open Spec.Ubool
open Util.List
open Util.Nth
open Util.Range

let array_t = FStar.ImmutableArray.t
let array_len = FStar.ImmutableArray.length
let array_index = FStar.ImmutableArray.index
let list_to_array = FStar.ImmutableArray.of_list
let array_to_list = FStar.ImmutableArray.to_list

let array_nth (#ty: Type) (a: array_t ty) (i: nat) : option ty =
  if i >= array_len a then
    None
  else
    Some (array_index a i)

let rec array_offset_matches_list
  (#ty: Type)
  (a: array_t ty)
  (len: nat{len = array_len a})
  (offset: nat)
  (l: list ty)
  : GTot bool (decreases l) =
  match l with
  | [] -> len = offset
  | hd :: tl -> len > offset && eqb hd (array_index a offset) && array_offset_matches_list a len (offset + 1) tl

let array_matches_list (#ty: Type) (a: array_t ty) (l: list ty) : GTot bool =
  array_offset_matches_list a (array_len a) 0 l

val array_matches_list_implies_length_equivalent (#ty: Type) (a: array_t ty) (l: list ty)
  : Lemma (requires array_matches_list a l)
          (ensures  array_len a = list_len l)

val array_matches_list_implies_nth_equivalent (#ty: Type) (a: array_t ty) (l: list ty) (n: nat)
  : Lemma (requires array_matches_list a l)
          (ensures  array_nth a n == list_nth l n)

val array_matches_list_implies_index_equivalent
  (#ty: Type)
  (a: array_t ty)
  (l: list ty)
  (n: nat{n < array_len a})
  : Lemma (requires array_matches_list a l)
          (ensures  n < list_len l /\ array_index a n == list_index l n)

val list_to_array_implies_array_matches_list
  (#ty: Type)
  (a: array_t ty)
  (l: list ty)
  : Lemma (requires a == list_to_array l)
          (ensures  array_matches_list a l)

val array_to_list_implies_array_matches_list
  (#ty: Type)
  (a: array_t ty)
  (l: list ty)
  : Lemma (requires l == array_to_list a)
          (ensures  array_matches_list a l)

val list_to_array_implies_length_equivalent
  (#ty: Type)
  (a: array_t ty)
  (l: list ty)
  : Lemma (requires a == list_to_array l)
          (ensures  array_len a = list_len l)

val list_to_array_implies_nth_equivalent
  (#ty: Type)
  (a: array_t ty)
  (l: list ty)
  (n: nat)
  : Lemma (requires a == list_to_array l)
          (ensures  array_nth a n == list_nth l n)

val list_to_array_implies_index_equivalent
  (#ty: Type)
  (a: array_t ty)
  (l: list ty)
  (n: nat{n < array_len a})
  : Lemma (requires a == list_to_array l)
          (ensures  n < list_len l /\ array_index a n == list_index l n)
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.ImmutableArray.fsti.checked
Util.ImmutableArray.fsti
f: (_: ty -> Prims.GTot Prims.bool) -> a: Util.ImmutableArray.array_t ty -> Prims.GTot Prims.bool
Prims.bool Util.ImmutableArray.array_t Util.Range.for_all_range Util.ImmutableArray.array_len Prims.nat Prims.b2t Prims.op_LessThan Util.ImmutableArray.array_index
let for_all_array (#ty: Type) (f: (ty -> GTot bool)) (a: array_t ty) =
  
for_all_range (array_len a) (fun i -> f (array_index a i))