diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index 248978b..4a4a115 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -89,9 +89,9 @@ Proof. reflexivity. Qed. -Lemma list_store_Z_compact_reverse_injection: forall l1 l2 n1 n2, - list_store_Z_compact l1 n1 -> - list_store_Z_compact l2 n2 -> +Lemma list_store_Z_reverse_injection: forall l1 l2 n1 n2, + list_store_Z l1 n1 -> + list_store_Z l2 n2 -> n1 = n2 -> l1 = l2. Proof. Admitted. @@ -284,7 +284,7 @@ Qed. Lemma list_store_Z_list_append: forall (l: list Z) (i: Z) (val_prefix: Z) (val_full: Z), 0 <= i < Zlength l -> - list_store_Z_compact l val_full -> + list_store_Z l val_full -> list_store_Z (sublist 0 i l) val_prefix -> list_store_Z (sublist 0 (i+1) l) (val_prefix + Znth i l 0 * UINT_MOD ^ i). Proof. @@ -313,7 +313,7 @@ Proof. split; try tauto. apply list_within_bound_Znth. lia. - unfold list_store_Z_compact in H0. + unfold list_store_Z in H0. tauto. Qed. diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 448952c..a0488a4 100755 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -1760,7 +1760,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -1792,7 +1792,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -1802,7 +1802,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -1836,7 +1836,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -1846,7 +1846,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -1874,7 +1874,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -1889,7 +1889,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= 0) |] && [| (0 <= n_pre) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (0) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -1899,7 +1899,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -1917,7 +1917,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -1927,7 +1927,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -1950,7 +1950,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -1960,7 +1960,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -1991,7 +1991,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_3 val ) |] + && [| (list_store_Z l_3 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] && [| (list_store_Z l'_2 val2_2 ) |] @@ -2001,7 +2001,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2016,7 +2016,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= (i + 1 )) |] && [| ((i + 1 ) <= n_pre) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2026,7 +2026,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2051,7 +2051,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_3 val ) |] + && [| (list_store_Z l_3 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] && [| (list_store_Z l'_2 val2_2 ) |] @@ -2061,7 +2061,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2076,7 +2076,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= (i + 1 )) |] && [| ((i + 1 ) <= n_pre) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2086,7 +2086,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2104,7 +2104,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ [| (i >= n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2114,7 +2114,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2128,7 +2128,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ |-- EX (val': Z) , [| ((val' + (b * (Z.pow (UINT_MOD) (n_pre)) ) ) = (val + b_pre )) |] - && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + && (mpd_store_Z ap_pre val n_pre cap1 ) ** (mpd_store_Z rp_pre val' n_pre cap2 ) . @@ -2140,7 +2140,7 @@ forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (v && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + && (mpd_store_Z ap_pre val n_pre cap1 ) ** (store_uint_array rp_pre cap2 l2 ) |-- [| ((Zlength (l2)) = cap2) |] @@ -2149,7 +2149,7 @@ forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (v && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + && (mpd_store_Z ap_pre val n_pre cap1 ) ** (store_uint_array rp_pre cap2 l2 ) . @@ -2158,7 +2158,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2182,7 +2182,7 @@ forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (v [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2197,7 +2197,7 @@ forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (v && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2216,7 +2216,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2226,7 +2226,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2241,7 +2241,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2251,7 +2251,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2273,7 +2273,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2283,7 +2283,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2314,7 +2314,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2324,7 +2324,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2345,7 +2345,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2355,7 +2355,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2378,7 +2378,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2388,7 +2388,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2419,7 +2419,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2429,7 +2429,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2450,7 +2450,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2460,7 +2460,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2487,7 +2487,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2497,7 +2497,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2519,7 +2519,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2529,7 +2529,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2555,7 +2555,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2565,7 +2565,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2587,7 +2587,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] + && [| (list_store_Z l_2 val ) |] && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] @@ -2597,7 +2597,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && [| (cap1 <= 100000000) |] @@ -2613,13 +2613,13 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ Definition mpn_add_1_which_implies_wit_1 := forall (n_pre: Z) (ap_pre: Z) (cap1: Z) (val: Z) , - (mpd_store_Z_compact ap_pre val n_pre cap1 ) + (mpd_store_Z ap_pre val n_pre cap1 ) |-- EX (l: (@list Z)) , [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] + && [| (list_store_Z l val ) |] && (store_uint_array ap_pre n_pre l ) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) . @@ -2659,11 +2659,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -2695,11 +2695,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -2741,8 +2741,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -2752,11 +2752,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -2801,8 +2801,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -2812,11 +2812,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -2861,8 +2861,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -2872,11 +2872,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -2921,8 +2921,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -2932,11 +2932,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -2971,11 +2971,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -2997,8 +2997,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a val_a ) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_a val_a ) |] + && [| (list_store_Z l_b val_b ) |] && [| (list_store_Z (sublist (0) (0) (l_a)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (0) (l_b)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3008,11 +3008,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3037,8 +3037,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3048,11 +3048,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3082,8 +3082,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3093,11 +3093,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3136,8 +3136,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_3 val_a ) |] - && [| (list_store_Z_compact l_b_3 val_b ) |] + && [| (list_store_Z l_a_3 val_a ) |] + && [| (list_store_Z l_b_3 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_3)) val_a_prefix_2 ) |] && [| (list_store_Z (sublist (0) (i) (l_b_3)) val_b_prefix_2 ) |] && [| (list_store_Z l_r_prefix_2 val_r_prefix_2 ) |] @@ -3147,11 +3147,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3173,8 +3173,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a val_a ) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_a val_a ) |] + && [| (list_store_Z l_b val_b ) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l_a)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l_b)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3184,11 +3184,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3221,8 +3221,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_3 val_a ) |] - && [| (list_store_Z_compact l_b_3 val_b ) |] + && [| (list_store_Z l_a_3 val_a ) |] + && [| (list_store_Z l_b_3 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_3)) val_a_prefix_2 ) |] && [| (list_store_Z (sublist (0) (i) (l_b_3)) val_b_prefix_2 ) |] && [| (list_store_Z l_r_prefix_2 val_r_prefix_2 ) |] @@ -3232,11 +3232,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3258,8 +3258,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a val_a ) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_a val_a ) |] + && [| (list_store_Z l_b val_b ) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l_a)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l_b)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3269,11 +3269,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3306,8 +3306,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_3 val_a ) |] - && [| (list_store_Z_compact l_b_3 val_b ) |] + && [| (list_store_Z l_a_3 val_a ) |] + && [| (list_store_Z l_b_3 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_3)) val_a_prefix_2 ) |] && [| (list_store_Z (sublist (0) (i) (l_b_3)) val_b_prefix_2 ) |] && [| (list_store_Z l_r_prefix_2 val_r_prefix_2 ) |] @@ -3317,11 +3317,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3343,8 +3343,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a val_a ) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_a val_a ) |] + && [| (list_store_Z l_b val_b ) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l_a)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l_b)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3354,11 +3354,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3391,8 +3391,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_3 val_a ) |] - && [| (list_store_Z_compact l_b_3 val_b ) |] + && [| (list_store_Z l_a_3 val_a ) |] + && [| (list_store_Z l_b_3 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_3)) val_a_prefix_2 ) |] && [| (list_store_Z (sublist (0) (i) (l_b_3)) val_b_prefix_2 ) |] && [| (list_store_Z l_r_prefix_2 val_r_prefix_2 ) |] @@ -3402,11 +3402,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3428,8 +3428,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a val_a ) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_a val_a ) |] + && [| (list_store_Z l_b val_b ) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l_a)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l_b)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3439,11 +3439,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3468,8 +3468,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a val_a ) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_a val_a ) |] + && [| (list_store_Z l_b val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3479,11 +3479,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b_2)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a_2)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z l_a_2 val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3501,8 +3501,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z |-- EX (val_r_out: Z) , [| ((val_r_out + (cy * (Z.pow (UINT_MOD) (n_pre)) ) ) = (val_a + val_b )) |] - && (mpd_store_Z_compact ap_pre val_a n_pre cap_a ) - ** (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + && (mpd_store_Z ap_pre val_a n_pre cap_a ) + ** (mpd_store_Z bp_pre val_b n_pre cap_b ) ** (mpd_store_Z rp_pre val_r_out n_pre cap_r ) . @@ -3516,8 +3516,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && (mpd_store_Z_compact ap_pre val_a n_pre cap_a ) - ** (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + && (mpd_store_Z ap_pre val_a n_pre cap_a ) + ** (mpd_store_Z bp_pre val_b n_pre cap_b ) ** (store_uint_array rp_pre cap_r l_r ) |-- [| ((Zlength (l_r)) = cap_r) |] @@ -3528,8 +3528,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && (mpd_store_Z_compact ap_pre val_a n_pre cap_a ) - ** (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + && (mpd_store_Z ap_pre val_a n_pre cap_a ) + ** (mpd_store_Z bp_pre val_b n_pre cap_b ) ** (store_uint_array rp_pre cap_r l_r ) . @@ -3538,7 +3538,7 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3549,13 +3549,13 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_r) |] && (store_uint_array ap_pre n_pre l_a ) ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) - ** (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + ** (mpd_store_Z bp_pre val_b n_pre cap_b ) ** (store_uint_array rp_pre cap_r l_r ) |-- [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3564,7 +3564,7 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + && (mpd_store_Z bp_pre val_b n_pre cap_b ) ** (store_uint_array ap_pre n_pre l_a ) ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) ** (store_uint_array rp_pre cap_r l_r ) @@ -3575,11 +3575,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3608,11 +3608,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3631,11 +3631,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3663,8 +3663,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3674,11 +3674,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3702,8 +3702,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3713,11 +3713,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3745,8 +3745,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3756,11 +3756,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3784,8 +3784,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3795,11 +3795,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3829,8 +3829,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3840,11 +3840,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3886,8 +3886,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3897,11 +3897,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3930,8 +3930,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3941,11 +3941,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -3976,8 +3976,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -3987,11 +3987,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4033,8 +4033,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4044,11 +4044,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4077,8 +4077,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4088,11 +4088,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4123,8 +4123,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4134,11 +4134,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4180,8 +4180,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4191,11 +4191,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4224,8 +4224,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4235,11 +4235,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4270,8 +4270,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4281,11 +4281,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4327,8 +4327,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4338,11 +4338,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4371,8 +4371,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4382,11 +4382,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4421,8 +4421,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4432,11 +4432,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4466,8 +4466,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4477,11 +4477,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4515,8 +4515,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4526,11 +4526,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4560,8 +4560,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4571,11 +4571,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4609,8 +4609,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4620,11 +4620,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4654,8 +4654,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4665,11 +4665,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4703,8 +4703,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4714,11 +4714,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4748,8 +4748,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_a) |] && [| (n_pre <= cap_b) |] && [| (n_pre <= cap_r) |] - && [| (list_store_Z_compact l_a_2 val_a ) |] - && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z l_a_2 val_a ) |] + && [| (list_store_Z l_b_2 val_b ) |] && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] && [| (list_store_Z l_r_prefix val_r_prefix ) |] @@ -4759,11 +4759,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z && [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && [| ((Zlength (l_r)) = cap_r) |] && [| (cap_a <= 100000000) |] && [| (cap_b <= 100000000) |] @@ -4783,26 +4783,26 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z Definition mpn_add_n_which_implies_wit_1 := forall (n_pre: Z) (ap_pre: Z) (val_a: Z) (cap_a: Z) , - (mpd_store_Z_compact ap_pre val_a n_pre cap_a ) + (mpd_store_Z ap_pre val_a n_pre cap_a ) |-- EX (l_a: (@list Z)) , [| (n_pre <= cap_a) |] && [| ((Zlength (l_a)) = n_pre) |] && [| (cap_a <= 100000000) |] - && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z l_a val_a ) |] && (store_uint_array ap_pre n_pre l_a ) ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) . Definition mpn_add_n_which_implies_wit_2 := forall (n_pre: Z) (bp_pre: Z) (val_b: Z) (cap_b: Z) , - (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + (mpd_store_Z bp_pre val_b n_pre cap_b ) |-- EX (l_b: (@list Z)) , [| (n_pre <= cap_b) |] && [| ((Zlength (l_b)) = n_pre) |] && [| (cap_b <= 100000000) |] - && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z l_b val_b ) |] && (store_uint_array bp_pre n_pre l_b ) ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) . diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 0977238..821eb73 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -469,7 +469,7 @@ Proof. assert (0 <= Znth i l_3 0 < 4294967296). { assert (l_2=l_3). { - pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + pose proof (list_store_Z_reverse_injection l_2 l_3 val val). apply H30 in H9; try tauto. } assert (i < Zlength l_3). { @@ -477,7 +477,7 @@ Proof. rewrite H17. tauto. } - unfold list_store_Z_compact in H9. + unfold list_store_Z in H9. apply list_within_bound_Znth. lia. tauto. @@ -505,7 +505,7 @@ Proof. lia. + assert (l_2=l_3). { - pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + pose proof (list_store_Z_reverse_injection l_2 l_3 val val). apply H28 in H9; try tauto. } @@ -539,7 +539,7 @@ Proof. lia. apply list_within_bound_Znth. lia. - unfold list_store_Z_compact in H9. + unfold list_store_Z in H9. tauto. - pose proof (Zlength_sublist0 i l'_2). lia. @@ -585,7 +585,7 @@ Proof. assert (0 <= Znth i l_3 0 < 4294967296). { assert (l_2=l_3). { - pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + pose proof (list_store_Z_reverse_injection l_2 l_3 val val). apply H30 in H9; try tauto. } assert (i < Zlength l_3). { @@ -593,7 +593,7 @@ Proof. rewrite H17. tauto. } - unfold list_store_Z_compact in H9. + unfold list_store_Z in H9. apply list_within_bound_Znth. lia. tauto. @@ -621,7 +621,7 @@ Proof. lia. + assert (l_2=l_3). { - pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + pose proof (list_store_Z_reverse_injection l_2 l_3 val val). apply H28 in H9; try tauto. } @@ -655,7 +655,7 @@ Proof. lia. apply list_within_bound_Znth. lia. - unfold list_store_Z_compact in H9. + unfold list_store_Z in H9. tauto. - pose proof (Zlength_sublist0 i l'_2). lia. @@ -664,10 +664,10 @@ Qed. Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. Proof. pre_process. - unfold mpd_store_Z_compact. + unfold mpd_store_Z. unfold mpd_store_list. Exists val2. - pose proof (list_store_Z_compact_reverse_injection l l_2 val val). + pose proof (list_store_Z_reverse_injection l l_2 val val). apply H19 in H2; try tauto. rewrite <-H2 in H10. assert (i = n_pre) by lia. @@ -675,32 +675,33 @@ Proof. rewrite <- H10 in H4. rewrite (sublist_self l (Zlength l)) in H4; try tauto. rewrite <-H2 in H12. - assert (list_store_Z l val). { apply list_store_Z_compact_to_normal. tauto. } pose proof (list_store_Z_injection l l val1 val). - apply H22 in H4; try tauto. + apply H21 in H4; try tauto. rewrite H4 in H6. entailer!. Exists l. entailer!. entailer!; try rewrite H20; try tauto. - - rewrite H10. - entailer!. - unfold mpd_store_Z. - unfold mpd_store_list. - Exists l'. - rewrite H7. - subst i. - entailer!. - rewrite H20. - entailer!. - apply store_uint_array_rec_def2undef. - - rewrite <- H20. tauto. + rewrite H10. + entailer!. + unfold mpd_store_Z. + unfold mpd_store_list. + Exists l'. + rewrite H7. + subst i. + entailer!. + rewrite H20. + entailer!. + apply store_uint_array_rec_def2undef. + assert (Zlength l' = n_pre) by lia. + rewrite <- H7. + tauto. Qed. Lemma proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1. Proof. pre_process. - unfold mpd_store_Z_compact. + unfold mpd_store_Z. Intros l. Exists l. unfold mpd_store_list. @@ -838,14 +839,14 @@ Proof. pre_process. rewrite replace_Znth_app_r. assert (l_a_3 = l_a_2). { - pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + pose proof (list_store_Z_reverse_injection l_a_3 l_a_2 val_a val_a). specialize (H37 H13 H28). apply H37. reflexivity. } subst l_a_3. assert (l_b_3 = l_b_2). { - pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + pose proof (list_store_Z_reverse_injection l_b_3 l_b_2 val_b val_b). specialize (H37 H14 H24). apply H37. reflexivity. @@ -882,7 +883,7 @@ Proof. assert (2 ^ 32 = 4294967296). { nia. } rewrite H37 in H4, H3; clear H37. apply Z_mod_3add_carry10; try lia; try tauto; - try unfold list_store_Z_compact in H13, H14; + try unfold list_store_Z in H13, H14; try apply list_within_bound_Znth; try lia; try tauto. @@ -936,14 +937,14 @@ Proof. pre_process. rewrite replace_Znth_app_r. assert (l_a_3 = l_a_2). { - pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + pose proof (list_store_Z_reverse_injection l_a_3 l_a_2 val_a val_a). specialize (H37 H13 H28). apply H37. reflexivity. } subst l_a_3. assert (l_b_3 = l_b_2). { - pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + pose proof (list_store_Z_reverse_injection l_b_3 l_b_2 val_b val_b). specialize (H37 H14 H24). apply H37. reflexivity. @@ -980,7 +981,7 @@ Proof. assert (2 ^ 32 = 4294967296). { nia. } rewrite H37 in H4, H3; clear H37. apply Z_mod_3add_carry11; try lia; try tauto; - try unfold list_store_Z_compact in H13, H14; + try unfold list_store_Z in H13, H14; try apply list_within_bound_Znth; try lia; try tauto. @@ -1034,14 +1035,14 @@ Proof. pre_process. rewrite replace_Znth_app_r. assert (l_a_3 = l_a_2). { - pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + pose proof (list_store_Z_reverse_injection l_a_3 l_a_2 val_a val_a). specialize (H37 H13 H28). apply H37. reflexivity. } subst l_a_3. assert (l_b_3 = l_b_2). { - pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + pose proof (list_store_Z_reverse_injection l_b_3 l_b_2 val_b val_b). specialize (H37 H14 H24). apply H37. reflexivity. @@ -1078,7 +1079,7 @@ Proof. assert (2 ^ 32 = 4294967296). { nia. } rewrite H37 in H4, H3; clear H37. apply Z_mod_3add_carry00; try lia; try tauto; - try unfold list_store_Z_compact in H13, H14; + try unfold list_store_Z in H13, H14; try apply list_within_bound_Znth; try lia; try tauto. @@ -1132,14 +1133,14 @@ Proof. pre_process. rewrite replace_Znth_app_r. assert (l_a_3 = l_a_2). { - pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + pose proof (list_store_Z_reverse_injection l_a_3 l_a_2 val_a val_a). specialize (H37 H13 H28). apply H37. reflexivity. } subst l_a_3. assert (l_b_3 = l_b_2). { - pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + pose proof (list_store_Z_reverse_injection l_b_3 l_b_2 val_b val_b). specialize (H37 H14 H24). apply H37. reflexivity. @@ -1176,7 +1177,7 @@ Proof. assert (2 ^ 32 = 4294967296). { nia. } rewrite H37 in H4, H3; clear H37. apply Z_mod_3add_carry01; try lia; try tauto; - try unfold list_store_Z_compact in H13, H14; + try unfold list_store_Z in H13, H14; try apply list_within_bound_Znth; try lia; try tauto. @@ -1229,14 +1230,14 @@ Lemma proof_of_mpn_add_n_return_wit_1 : mpn_add_n_return_wit_1. Proof. pre_process. assert (l_a_2 = l_a). { - pose proof (list_store_Z_compact_reverse_injection l_a_2 l_a val_a val_a). + pose proof (list_store_Z_reverse_injection l_a_2 l_a val_a val_a). specialize (H29 H20 H5). apply H29. reflexivity. } subst l_a_2. assert (l_b_2 = l_b). { - pose proof (list_store_Z_compact_reverse_injection l_b_2 l_b val_b val_b). + pose proof (list_store_Z_reverse_injection l_b_2 l_b val_b val_b). specialize (H29 H16 H6). apply H29. reflexivity. @@ -1244,55 +1245,50 @@ Proof. subst l_b_2. assert (i = n_pre) by lia. Exists val_r_prefix. - unfold mpd_store_Z_compact. + unfold mpd_store_Z. unfold mpd_store_list. Exists l_a. Exists l_b. entailer!. - + rewrite H14. - rewrite H18. - entailer!. - unfold mpd_store_Z. - Exists l_r_prefix. - rewrite H29 in *. - entailer!. - unfold mpd_store_list. - entailer!. - rewrite H10. - entailer!. - apply store_uint_array_rec_def2undef. - + rewrite <- H29. - assert (val_a_prefix = val_a). { - assert (i = Zlength l_a). { - lia. - } - rewrite H30 in H7. - rewrite sublist_self in H7. - unfold list_store_Z_compact in H5. - unfold list_store_Z in H7. - lia. - reflexivity. - } - rewrite <- H30; clear H30. - assert (val_b_prefix = val_b). { - assert (i = Zlength l_b). { - lia. - } - rewrite H30 in H8. - rewrite sublist_self in H8. - unfold list_store_Z_compact in H6. - unfold list_store_Z in H8. - lia. - reflexivity. - } - rewrite <- H30; clear H30. - tauto. + rewrite H14. + rewrite H18. + entailer!. + unfold mpd_store_Z. + Exists l_r_prefix. + rewrite H29 in *. + entailer!. + unfold mpd_store_list. + entailer!. + rewrite H10. + entailer!. + apply store_uint_array_rec_def2undef. + rewrite <- H29. + assert (val_a_prefix = val_a). { + rewrite <-H18 in H7. + rewrite sublist_self in H7. + unfold list_store_Z in H5. + unfold list_store_Z in H7. + lia. + reflexivity. + } + rewrite <- H30; clear H30. + assert (val_b_prefix = val_b). { + rewrite <-H14 in H8. + rewrite sublist_self in H8. + unfold list_store_Z in H6. + unfold list_store_Z in H8. + lia. + reflexivity. + } + rewrite <- H30; clear H30. + rewrite H29. + tauto. Qed. Lemma proof_of_mpn_add_n_which_implies_wit_1 : mpn_add_n_which_implies_wit_1. Proof. pre_process. - unfold mpd_store_Z_compact. + unfold mpd_store_Z. Intros l. Exists l. unfold mpd_store_list. @@ -1304,7 +1300,7 @@ Qed. Lemma proof_of_mpn_add_n_which_implies_wit_2 : mpn_add_n_which_implies_wit_2. Proof. pre_process. - unfold mpd_store_Z_compact. + unfold mpd_store_Z. Intros l. Exists l. unfold mpd_store_list. diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 8c9f618..a24fc1a 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -228,7 +228,7 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) /*@ With val l2 cap1 cap2 Require - mpd_store_Z_compact(ap, val, n, cap1) * + mpd_store_Z(ap, val, n, cap1) * store_uint_array(rp, cap2, l2) && Zlength(l2) == cap2 && cap2 >= n && @@ -237,13 +237,13 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) n > 0 && n <= cap1 Ensure exists val', - mpd_store_Z_compact(ap@pre, val, n@pre, cap1) * + mpd_store_Z(ap@pre, val, n@pre, cap1) * mpd_store_Z(rp@pre, val', n@pre, cap2) && (val' + __return * Z::pow(UINT_MOD, n@pre) == val + b@pre) */ { /*@ - mpd_store_Z_compact(ap@pre, val, n@pre, cap1) + mpd_store_Z(ap@pre, val, n@pre, cap1) which implies exists l, n@pre <= cap1 && @@ -251,7 +251,7 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) cap1 <= 100000000 && store_uint_array(ap@pre, n@pre, l) * store_undef_uint_array_rec(ap@pre, n@pre, cap1) && - list_store_Z_compact(l, val) + list_store_Z(l, val) */ int i; //assert (n > 0); @@ -278,7 +278,7 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) /*@Inv exists l l' l'' val1 val2, 0 <= i && i <= n@pre && - list_store_Z_compact(l, val) && n@pre <= cap1 && + list_store_Z(l, val) && n@pre <= cap1 && store_uint_array(ap@pre, n@pre, l) * store_undef_uint_array_rec(ap@pre, n@pre, cap1) && list_store_Z(sublist(0, i, l), val1) && @@ -318,8 +318,8 @@ mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) /*@ With cap_a cap_b cap_r val_a val_b l_r Require - mpd_store_Z_compact(ap, val_a, n, cap_a) * - mpd_store_Z_compact(bp, val_b, n, cap_b) * + mpd_store_Z(ap, val_a, n, cap_a) * + mpd_store_Z(bp, val_b, n, cap_b) * store_uint_array(rp, cap_r, l_r) && Zlength(l_r) == cap_r && cap_a <= 100000000 && @@ -328,14 +328,14 @@ mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) n > 0 && n <= cap_a && n <= cap_b && n <= cap_r Ensure exists val_r_out, - mpd_store_Z_compact(ap@pre, val_a, n@pre, cap_a) * - mpd_store_Z_compact(bp@pre, val_b, n@pre, cap_b) * + mpd_store_Z(ap@pre, val_a, n@pre, cap_a) * + mpd_store_Z(bp@pre, val_b, n@pre, cap_b) * mpd_store_Z(rp@pre, val_r_out, n@pre, cap_r) && (val_r_out + __return * Z::pow(UINT_MOD, n@pre) == val_a + val_b) */ { /*@ - mpd_store_Z_compact(ap@pre, val_a, n@pre, cap_a) + mpd_store_Z(ap@pre, val_a, n@pre, cap_a) which implies exists l_a, n@pre <= cap_a && @@ -343,10 +343,10 @@ mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) cap_a <= 100000000 && store_uint_array(ap@pre, n@pre, l_a) * store_undef_uint_array_rec(ap@pre, n@pre, cap_a) && - list_store_Z_compact(l_a, val_a) + list_store_Z(l_a, val_a) */ /*@ - mpd_store_Z_compact(bp@pre, val_b, n@pre, cap_b) + mpd_store_Z(bp@pre, val_b, n@pre, cap_b) which implies exists l_b, n@pre <= cap_b && @@ -354,7 +354,7 @@ mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) cap_b <= 100000000 && store_uint_array(bp@pre, n@pre, l_b) * store_undef_uint_array_rec(bp@pre, n@pre, cap_b) && - list_store_Z_compact(l_b, val_b) + list_store_Z(l_b, val_b) */ int i; unsigned int cy; @@ -370,8 +370,8 @@ mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) /*@Inv exists l_a l_b l_r_prefix l_r_suffix val_a_prefix val_b_prefix val_r_prefix, 0 <= i && i <= n@pre && n@pre <= cap_a && n@pre <= cap_b && n@pre <= cap_r && - list_store_Z_compact(l_a, val_a) && - list_store_Z_compact(l_b, val_b) && + list_store_Z(l_a, val_a) && + list_store_Z(l_b, val_b) && list_store_Z(sublist(0, i, l_a), val_a_prefix) && list_store_Z(sublist(0, i, l_b), val_b_prefix) && list_store_Z(l_r_prefix, val_r_prefix) &&