arrays

source/casestudies/2024-casestudy-lists/lists_case.mmt

@@ -57,6 +57,8 @@ theory ArrayLists =
 
     // equational theory???❙
     grow_update_eq : {m,l:array m, a,b,c} (grow l by a) update b as c ≐ grow (l update b as c) by a ❙
+    array_same : {a,x :a, l : array a, b,y:b, m : array b} x ≐ y ⟶ l ≐ m ❙
+    array_same_grow : {a, l: array a, m: array b,k :nat} l ≐ m ⟶ grow l by k ≐ grow m by k ❙
     
     length : {a} array a ⟶ nat❘# | 2 |❙
     length_make : {a,n,x:a} |make n x| ≐ n❙
@@ -71,6 +73,8 @@ theory ArrayLists =
     get_grow_def : {a,l:array a,m,n} |l| < m ⟶ m < |l|+n ⟶ (grow l by n) get m ≐ some (default l)❙
     get_set_eq: {a,x:a,l,n} (l update n as x) get n ≐ some x❙
     get_set_neq: {a,x:a,l,m,n} m ≠ n ⟶ (l update n as x) get m ≐ l get m ❙
+    // some thing new from here❙
+    get_set_noteq : {a, x: a, l: array a, m, n} (l update m as x) get n ≠ x ⟶ m ≠ n ❙
 ❚
 
 theory SparseLists =