diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v
index 2df150a..448952c 100755
--- a/projects/lib/gmp_goal.v
+++ b/projects/lib/gmp_goal.v
@@ -2651,6 +2651,2189 @@ forall (n_pre: Z) (rp_pre: Z) (cap2: Z) (l'': (@list Z)) (l': (@list Z)) (i: Z)
   **  (store_uint_array rp_pre (i + 1 ) (app (l') ((cons (a) (nil)))) )
 .
 
+(*----- Function mpn_add_n -----*)
+
+Definition mpn_add_n_safety_wit_1 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) ,
+  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array_rec rp_pre 0 cap_r l_r )
+  **  (store_uint_array rp_pre 0 nil )
+  **  ((( &( "cy" ) )) # UInt  |->_)
+  **  ((( &( "i" ) )) # Int  |->_)
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| (0 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 0) |]
+.
+
+Definition mpn_add_n_safety_wit_2 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) ,
+  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array_rec rp_pre 0 cap_r l_r )
+  **  (store_uint_array rp_pre 0 nil )
+  **  ((( &( "cy" ) )) # UInt  |->_)
+  **  ((( &( "i" ) )) # Int  |-> 0)
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| (0 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 0) |]
+.
+
+Definition mpn_add_n_safety_wit_3 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) ((app (l_r_prefix) ((cons (a) (nil)))))) )
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  ((( &( "r" ) )) # UInt  |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)))
+  **  ((( &( "b" ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  ((( &( "a" ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  ((( &( "cy" ) )) # UInt  |-> (0 + 1 ))
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| ((i + 1 ) <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= (i + 1 )) |]
+.
+
+Definition mpn_add_n_safety_wit_4 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) ((app (l_r_prefix) ((cons (a) (nil)))))) )
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  ((( &( "r" ) )) # UInt  |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)))
+  **  ((( &( "b" ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  ((( &( "a" ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  ((( &( "cy" ) )) # UInt  |-> (0 + 0 ))
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| ((i + 1 ) <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= (i + 1 )) |]
+.
+
+Definition mpn_add_n_safety_wit_5 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) ((app (l_r_prefix) ((cons (a) (nil)))))) )
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  ((( &( "r" ) )) # UInt  |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)))
+  **  ((( &( "b" ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  ((( &( "a" ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  ((( &( "cy" ) )) # UInt  |-> (1 + 1 ))
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| ((i + 1 ) <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= (i + 1 )) |]
+.
+
+Definition mpn_add_n_safety_wit_6 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) ((app (l_r_prefix) ((cons (a) (nil)))))) )
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  ((( &( "r" ) )) # UInt  |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)))
+  **  ((( &( "b" ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  ((( &( "a" ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  ((( &( "cy" ) )) # UInt  |-> (1 + 0 ))
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| ((i + 1 ) <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= (i + 1 )) |]
+.
+
+Definition mpn_add_n_entail_wit_1 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) ,
+  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array_rec rp_pre 0 cap_r l_r )
+  **  (store_uint_array rp_pre 0 nil )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+|--
+  EX (l_r_suffix: (@list Z))  (l_r_prefix: (@list Z))  (val_r_prefix: Z)  (val_b_prefix: Z)  (val_a_prefix: Z)  (l_b: (@list Z))  (l_a: (@list Z)) ,
+  [| (0 <= 0) |] 
+  &&  [| (0 <= 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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = 0) |] 
+  &&  [| ((val_r_prefix + (0 * (Z.pow (UINT_MOD) (0)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre 0 l_r_prefix )
+  **  (store_uint_array_rec rp_pre 0 cap_r l_r_suffix )
+.
+
+Definition mpn_add_n_entail_wit_2 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  ((( &( "i" ) )) # Int  |-> i)
+  **  ((( &( "cy" ) )) # UInt  |-> cy)
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  ((( &( "cy" ) )) # UInt  |-> cy)
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+.
+
+Definition mpn_add_n_entail_wit_3_1 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix_2: (@list Z)) (cy: Z) (l_r_prefix_2: (@list Z)) (val_r_prefix_2: Z) (val_b_prefix_2: Z) (val_a_prefix_2: Z) (l_b_3: (@list Z)) (l_a_3: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix_2 = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32)) >= (Znth i l_b_3 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix_2)) = i) |] 
+  &&  [| ((val_r_prefix_2 + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix_2 + val_b_prefix_2 )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32))) ((app (l_r_prefix_2) ((cons (a) (nil)))))) )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_3 )
+  **  (store_uint_array ap_pre n_pre l_a_3 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+|--
+  EX (l_r_suffix: (@list Z))  (l_r_prefix: (@list Z))  (val_r_prefix: Z)  (val_b_prefix: Z)  (val_a_prefix: Z)  (l_b: (@list Z))  (l_a: (@list Z)) ,
+  [| (0 <= (i + 1 )) |] 
+  &&  [| ((i + 1 ) <= 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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = (i + 1 )) |] 
+  &&  [| ((val_r_prefix + ((1 + 0 ) * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre (i + 1 ) l_r_prefix )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix )
+.
+
+Definition mpn_add_n_entail_wit_3_2 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix_2: (@list Z)) (cy: Z) (l_r_prefix_2: (@list Z)) (val_r_prefix_2: Z) (val_b_prefix_2: Z) (val_a_prefix_2: Z) (l_b_3: (@list Z)) (l_a_3: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix_2 = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32)) < (Znth i l_b_3 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix_2)) = i) |] 
+  &&  [| ((val_r_prefix_2 + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix_2 + val_b_prefix_2 )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32))) ((app (l_r_prefix_2) ((cons (a) (nil)))))) )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_3 )
+  **  (store_uint_array ap_pre n_pre l_a_3 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+|--
+  EX (l_r_suffix: (@list Z))  (l_r_prefix: (@list Z))  (val_r_prefix: Z)  (val_b_prefix: Z)  (val_a_prefix: Z)  (l_b: (@list Z))  (l_a: (@list Z)) ,
+  [| (0 <= (i + 1 )) |] 
+  &&  [| ((i + 1 ) <= 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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = (i + 1 )) |] 
+  &&  [| ((val_r_prefix + ((1 + 1 ) * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre (i + 1 ) l_r_prefix )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix )
+.
+
+Definition mpn_add_n_entail_wit_3_3 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix_2: (@list Z)) (cy: Z) (l_r_prefix_2: (@list Z)) (val_r_prefix_2: Z) (val_b_prefix_2: Z) (val_a_prefix_2: Z) (l_b_3: (@list Z)) (l_a_3: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix_2 = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32)) >= (Znth i l_b_3 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix_2)) = i) |] 
+  &&  [| ((val_r_prefix_2 + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix_2 + val_b_prefix_2 )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32))) ((app (l_r_prefix_2) ((cons (a) (nil)))))) )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_3 )
+  **  (store_uint_array ap_pre n_pre l_a_3 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+|--
+  EX (l_r_suffix: (@list Z))  (l_r_prefix: (@list Z))  (val_r_prefix: Z)  (val_b_prefix: Z)  (val_a_prefix: Z)  (l_b: (@list Z))  (l_a: (@list Z)) ,
+  [| (0 <= (i + 1 )) |] 
+  &&  [| ((i + 1 ) <= 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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = (i + 1 )) |] 
+  &&  [| ((val_r_prefix + ((0 + 0 ) * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre (i + 1 ) l_r_prefix )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix )
+.
+
+Definition mpn_add_n_entail_wit_3_4 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix_2: (@list Z)) (cy: Z) (l_r_prefix_2: (@list Z)) (val_r_prefix_2: Z) (val_b_prefix_2: Z) (val_a_prefix_2: Z) (l_b_3: (@list Z)) (l_a_3: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix_2 = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32)) < (Znth i l_b_3 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix_2)) = i) |] 
+  &&  [| ((val_r_prefix_2 + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix_2 + val_b_prefix_2 )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32))) ((app (l_r_prefix_2) ((cons (a) (nil)))))) )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_3 )
+  **  (store_uint_array ap_pre n_pre l_a_3 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+|--
+  EX (l_r_suffix: (@list Z))  (l_r_prefix: (@list Z))  (val_r_prefix: Z)  (val_b_prefix: Z)  (val_a_prefix: Z)  (l_b: (@list Z))  (l_a: (@list Z)) ,
+  [| (0 <= (i + 1 )) |] 
+  &&  [| ((i + 1 ) <= 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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = (i + 1 )) |] 
+  &&  [| ((val_r_prefix + ((0 + 1 ) * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre (i + 1 ) l_r_prefix )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix )
+.
+
+Definition mpn_add_n_return_wit_1 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b: (@list Z)) (l_a: (@list Z)) (i: Z) ,
+  [| (i >= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b_2)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact 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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+|--
+  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 rp_pre val_r_out n_pre cap_r )
+.
+
+Definition mpn_add_n_partial_solve_wit_1 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) ,
+  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (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 )
+  **  (store_uint_array rp_pre cap_r l_r )
+|--
+  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (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 )
+  **  (store_uint_array rp_pre cap_r l_r )
+.
+
+Definition mpn_add_n_partial_solve_wit_2 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) ,
+  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (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 )
+  **  (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 ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (mpd_store_Z_compact 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 )
+.
+
+Definition mpn_add_n_partial_solve_wit_3_pure := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) ,
+  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  ((( &( "cy" ) )) # UInt  |->_)
+  **  ((( &( "i" ) )) # Int  |->_)
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+  **  (store_uint_array rp_pre cap_r l_r )
+|--
+  [| ((Zlength (l_r)) = cap_r) |]
+.
+
+Definition mpn_add_n_partial_solve_wit_3_aux := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) ,
+  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre 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 )
+|--
+  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre cap_r l_r )
+  **  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array ap_pre n_pre l_a )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+.
+
+Definition mpn_add_n_partial_solve_wit_3 := mpn_add_n_partial_solve_wit_3_pure -> mpn_add_n_partial_solve_wit_3_aux.
+
+Definition mpn_add_n_partial_solve_wit_4 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+|--
+  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (((ap_pre + (i * sizeof(UINT) ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  (store_uint_array_missing_i_rec ap_pre i 0 n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+.
+
+Definition mpn_add_n_partial_solve_wit_5 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+|--
+  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (((bp_pre + (i * sizeof(UINT) ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  (store_uint_array_missing_i_rec bp_pre i 0 n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+.
+
+Definition mpn_add_n_partial_solve_wit_6_pure := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  ((( &( "r" ) )) # UInt  |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)))
+  **  ((( &( "b" ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  ((( &( "a" ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  ((( &( "cy" ) )) # UInt  |-> (0 + 1 ))
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |]
+.
+
+Definition mpn_add_n_partial_solve_wit_6_aux := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+|--
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+Definition mpn_add_n_partial_solve_wit_6 := mpn_add_n_partial_solve_wit_6_pure -> mpn_add_n_partial_solve_wit_6_aux.
+
+Definition mpn_add_n_partial_solve_wit_7_pure := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  ((( &( "r" ) )) # UInt  |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)))
+  **  ((( &( "b" ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  ((( &( "a" ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  ((( &( "cy" ) )) # UInt  |-> (0 + 0 ))
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |]
+.
+
+Definition mpn_add_n_partial_solve_wit_7_aux := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+|--
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+Definition mpn_add_n_partial_solve_wit_7 := mpn_add_n_partial_solve_wit_7_pure -> mpn_add_n_partial_solve_wit_7_aux.
+
+Definition mpn_add_n_partial_solve_wit_8_pure := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  ((( &( "r" ) )) # UInt  |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)))
+  **  ((( &( "b" ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  ((( &( "a" ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  ((( &( "cy" ) )) # UInt  |-> (1 + 1 ))
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |]
+.
+
+Definition mpn_add_n_partial_solve_wit_8_aux := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+|--
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+Definition mpn_add_n_partial_solve_wit_8 := mpn_add_n_partial_solve_wit_8_pure -> mpn_add_n_partial_solve_wit_8_aux.
+
+Definition mpn_add_n_partial_solve_wit_9_pure := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  ((( &( "r" ) )) # UInt  |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)))
+  **  ((( &( "b" ) )) # UInt  |-> (Znth i l_b_2 0))
+  **  ((( &( "a" ) )) # UInt  |-> (Znth i l_a_2 0))
+  **  ((( &( "cy" ) )) # UInt  |-> (1 + 0 ))
+  **  ((( &( "i" ) )) # Int  |-> i)
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  ((( &( "n" ) )) # Int  |-> n_pre)
+  **  ((( &( "bp" ) )) # Ptr  |-> bp_pre)
+  **  ((( &( "ap" ) )) # Ptr  |-> ap_pre)
+  **  ((( &( "rp" ) )) # Ptr  |-> rp_pre)
+|--
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |]
+.
+
+Definition mpn_add_n_partial_solve_wit_9_aux := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) ,
+  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+  **  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+|--
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+Definition mpn_add_n_partial_solve_wit_9 := mpn_add_n_partial_solve_wit_9_pure -> mpn_add_n_partial_solve_wit_9_aux.
+
+Definition mpn_add_n_partial_solve_wit_10 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+|--
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (((rp_pre + (i * sizeof(UINT) ) )) # UInt  |->_)
+  **  (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+Definition mpn_add_n_partial_solve_wit_11 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+|--
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (((rp_pre + (i * sizeof(UINT) ) )) # UInt  |->_)
+  **  (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+Definition mpn_add_n_partial_solve_wit_12 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+|--
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (((rp_pre + (i * sizeof(UINT) ) )) # UInt  |->_)
+  **  (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+Definition mpn_add_n_partial_solve_wit_13 := 
+forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+|--
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |] 
+  &&  [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] 
+  &&  [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] 
+  &&  [| (0 <= cy) |] 
+  &&  [| (cy <= UINT_MAX) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i <= n_pre) |] 
+  &&  [| (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 (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 ) |] 
+  &&  [| ((Zlength (l_r_prefix)) = i) |] 
+  &&  [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| ((Zlength (l_b)) = n_pre) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_b val_b ) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| ((Zlength (l_a)) = n_pre) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (list_store_Z_compact l_a val_a ) |] 
+  &&  [| ((Zlength (l_r)) = cap_r) |] 
+  &&  [| (cap_a <= 100000000) |] 
+  &&  [| (cap_b <= 100000000) |] 
+  &&  [| (cap_r <= 100000000) |] 
+  &&  [| (n_pre > 0) |] 
+  &&  [| (n_pre <= cap_a) |] 
+  &&  [| (n_pre <= cap_b) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (((rp_pre + (i * sizeof(UINT) ) )) # UInt  |->_)
+  **  (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+  **  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array bp_pre n_pre l_b_2 )
+  **  (store_uint_array ap_pre n_pre l_a_2 )
+  **  (store_undef_uint_array_rec ap_pre n_pre cap_a )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+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 )
+|--
+  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 ) |]
+  &&  (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 )
+|--
+  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 ) |]
+  &&  (store_uint_array bp_pre n_pre l_b )
+  **  (store_undef_uint_array_rec bp_pre n_pre cap_b )
+.
+
+Definition mpn_add_n_which_implies_wit_3 := 
+forall (rp_pre: Z) (l_r: (@list Z)) (cap_r: Z) ,
+  [| ((Zlength (l_r)) = cap_r) |]
+  &&  (store_uint_array rp_pre cap_r l_r )
+|--
+  [| ((Zlength (l_r)) = cap_r) |]
+  &&  (store_uint_array_rec rp_pre 0 cap_r l_r )
+  **  (store_uint_array rp_pre 0 nil )
+.
+
+Definition mpn_add_n_which_implies_wit_4 := 
+forall (n_pre: Z) (rp_pre: Z) (cap_r: Z) (l_r_suffix: (@list Z)) (l_r_prefix: (@list Z)) (i: Z) ,
+  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array rp_pre i l_r_prefix )
+  **  (store_uint_array_rec rp_pre i cap_r l_r_suffix )
+|--
+  EX (a: Z)  (l_r_suffix': (@list Z)) ,
+  [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] 
+  &&  [| (0 <= i) |] 
+  &&  [| (i < n_pre) |] 
+  &&  [| (n_pre <= cap_r) |]
+  &&  (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' )
+  **  (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) )
+.
+
 (*----- Function mpz_clear -----*)
 
 Definition mpz_clear_return_wit_1_1 := 
@@ -3770,6 +5953,41 @@ Axiom proof_of_mpn_add_1_partial_solve_wit_7 : mpn_add_1_partial_solve_wit_7.
 Axiom proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1.
 Axiom proof_of_mpn_add_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2.
 Axiom proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3.
+Axiom proof_of_mpn_add_n_safety_wit_1 : mpn_add_n_safety_wit_1.
+Axiom proof_of_mpn_add_n_safety_wit_2 : mpn_add_n_safety_wit_2.
+Axiom proof_of_mpn_add_n_safety_wit_3 : mpn_add_n_safety_wit_3.
+Axiom proof_of_mpn_add_n_safety_wit_4 : mpn_add_n_safety_wit_4.
+Axiom proof_of_mpn_add_n_safety_wit_5 : mpn_add_n_safety_wit_5.
+Axiom proof_of_mpn_add_n_safety_wit_6 : mpn_add_n_safety_wit_6.
+Axiom proof_of_mpn_add_n_entail_wit_1 : mpn_add_n_entail_wit_1.
+Axiom proof_of_mpn_add_n_entail_wit_2 : mpn_add_n_entail_wit_2.
+Axiom proof_of_mpn_add_n_entail_wit_3_1 : mpn_add_n_entail_wit_3_1.
+Axiom proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2.
+Axiom proof_of_mpn_add_n_entail_wit_3_3 : mpn_add_n_entail_wit_3_3.
+Axiom proof_of_mpn_add_n_entail_wit_3_4 : mpn_add_n_entail_wit_3_4.
+Axiom proof_of_mpn_add_n_return_wit_1 : mpn_add_n_return_wit_1.
+Axiom proof_of_mpn_add_n_partial_solve_wit_1 : mpn_add_n_partial_solve_wit_1.
+Axiom proof_of_mpn_add_n_partial_solve_wit_2 : mpn_add_n_partial_solve_wit_2.
+Axiom proof_of_mpn_add_n_partial_solve_wit_3_pure : mpn_add_n_partial_solve_wit_3_pure.
+Axiom proof_of_mpn_add_n_partial_solve_wit_3 : mpn_add_n_partial_solve_wit_3.
+Axiom proof_of_mpn_add_n_partial_solve_wit_4 : mpn_add_n_partial_solve_wit_4.
+Axiom proof_of_mpn_add_n_partial_solve_wit_5 : mpn_add_n_partial_solve_wit_5.
+Axiom proof_of_mpn_add_n_partial_solve_wit_6_pure : mpn_add_n_partial_solve_wit_6_pure.
+Axiom proof_of_mpn_add_n_partial_solve_wit_6 : mpn_add_n_partial_solve_wit_6.
+Axiom proof_of_mpn_add_n_partial_solve_wit_7_pure : mpn_add_n_partial_solve_wit_7_pure.
+Axiom proof_of_mpn_add_n_partial_solve_wit_7 : mpn_add_n_partial_solve_wit_7.
+Axiom proof_of_mpn_add_n_partial_solve_wit_8_pure : mpn_add_n_partial_solve_wit_8_pure.
+Axiom proof_of_mpn_add_n_partial_solve_wit_8 : mpn_add_n_partial_solve_wit_8.
+Axiom proof_of_mpn_add_n_partial_solve_wit_9_pure : mpn_add_n_partial_solve_wit_9_pure.
+Axiom proof_of_mpn_add_n_partial_solve_wit_9 : mpn_add_n_partial_solve_wit_9.
+Axiom proof_of_mpn_add_n_partial_solve_wit_10 : mpn_add_n_partial_solve_wit_10.
+Axiom proof_of_mpn_add_n_partial_solve_wit_11 : mpn_add_n_partial_solve_wit_11.
+Axiom proof_of_mpn_add_n_partial_solve_wit_12 : mpn_add_n_partial_solve_wit_12.
+Axiom proof_of_mpn_add_n_partial_solve_wit_13 : mpn_add_n_partial_solve_wit_13.
+Axiom proof_of_mpn_add_n_which_implies_wit_1 : mpn_add_n_which_implies_wit_1.
+Axiom proof_of_mpn_add_n_which_implies_wit_2 : mpn_add_n_which_implies_wit_2.
+Axiom proof_of_mpn_add_n_which_implies_wit_3 : mpn_add_n_which_implies_wit_3.
+Axiom proof_of_mpn_add_n_which_implies_wit_4 : mpn_add_n_which_implies_wit_4.
 Axiom proof_of_mpz_clear_return_wit_1_1 : mpz_clear_return_wit_1_1.
 Axiom proof_of_mpz_clear_return_wit_1_2 : mpz_clear_return_wit_1_2.
 Axiom proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3.
diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v
index dd60026..21ed069 100755
--- a/projects/lib/gmp_proof_auto.v
+++ b/projects/lib/gmp_proof_auto.v
@@ -180,6 +180,78 @@ Proof. Admitted.
 Lemma proof_of_mpn_add_1_partial_solve_wit_7 : mpn_add_1_partial_solve_wit_7.
 Proof. Admitted. 
 
+Lemma proof_of_mpn_add_n_safety_wit_1 : mpn_add_n_safety_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_safety_wit_2 : mpn_add_n_safety_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_safety_wit_3 : mpn_add_n_safety_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_safety_wit_4 : mpn_add_n_safety_wit_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_safety_wit_5 : mpn_add_n_safety_wit_5.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_safety_wit_6 : mpn_add_n_safety_wit_6.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_1 : mpn_add_n_partial_solve_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_2 : mpn_add_n_partial_solve_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_3_pure : mpn_add_n_partial_solve_wit_3_pure.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_3 : mpn_add_n_partial_solve_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_4 : mpn_add_n_partial_solve_wit_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_5 : mpn_add_n_partial_solve_wit_5.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_6_pure : mpn_add_n_partial_solve_wit_6_pure.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_6 : mpn_add_n_partial_solve_wit_6.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_7_pure : mpn_add_n_partial_solve_wit_7_pure.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_7 : mpn_add_n_partial_solve_wit_7.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_8_pure : mpn_add_n_partial_solve_wit_8_pure.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_8 : mpn_add_n_partial_solve_wit_8.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_9_pure : mpn_add_n_partial_solve_wit_9_pure.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_9 : mpn_add_n_partial_solve_wit_9.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_10 : mpn_add_n_partial_solve_wit_10.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_11 : mpn_add_n_partial_solve_wit_11.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_12 : mpn_add_n_partial_solve_wit_12.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_partial_solve_wit_13 : mpn_add_n_partial_solve_wit_13.
+Proof. Admitted. 
+
 Lemma proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3.
 Proof. Admitted. 
 
diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v
index 0580a17..fd3b8d4 100755
--- a/projects/lib/gmp_proof_manual.v
+++ b/projects/lib/gmp_proof_manual.v
@@ -807,6 +807,39 @@ Proof.
     lia.
 Qed.
 
+Lemma proof_of_mpn_add_n_entail_wit_1 : mpn_add_n_entail_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_entail_wit_2 : mpn_add_n_entail_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_entail_wit_3_1 : mpn_add_n_entail_wit_3_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_entail_wit_3_3 : mpn_add_n_entail_wit_3_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_entail_wit_3_4 : mpn_add_n_entail_wit_3_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_return_wit_1 : mpn_add_n_return_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_which_implies_wit_1 : mpn_add_n_which_implies_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_which_implies_wit_2 : mpn_add_n_which_implies_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_which_implies_wit_3 : mpn_add_n_which_implies_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_n_which_implies_wit_4 : mpn_add_n_which_implies_wit_4.
+Proof. Admitted. 
+
 Lemma proof_of_mpz_clear_return_wit_1_1 : mpz_clear_return_wit_1_1.
 Proof.
   pre_process.
diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c
index 43b2ab9..8c9f618 100755
--- a/projects/mini-gmp.c
+++ b/projects/mini-gmp.c
@@ -313,24 +313,104 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b)
 }
 
 /* 位数相同的多精度数ap 加上多精度数bp，返回最后产生的进位 */
-/*unsigned int
+unsigned int
 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) *
+   store_uint_array(rp, cap_r, l_r) &&
+   Zlength(l_r) == cap_r &&
+   cap_a <= 100000000 &&
+   cap_b <= 100000000 &&
+   cap_r <= 100000000 &&
+   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(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)
+    which implies
+    exists l_a,
+      n@pre <= cap_a &&
+      Zlength(l_a) == n@pre &&
+      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)
+  */
+  /*@
+    mpd_store_Z_compact(bp@pre, val_b, n@pre, cap_b)
+    which implies
+    exists l_b,
+      n@pre <= cap_b &&
+      Zlength(l_b) == n@pre &&
+      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)
+  */
   int i;
   unsigned int cy;
 
-  for (i = 0, cy = 0; i < n; i++)
+  /*@
+  store_uint_array(rp@pre, cap_r, l_r) && Zlength(l_r) == cap_r
+  which implies
+    store_uint_array_rec(rp@pre, 0, cap_r, l_r) * store_uint_array(rp@pre, 0, nil) &&
+    Zlength(l_r) == cap_r
+  */
+  i = 0;
+  cy = 0;
+  /*@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(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) &&
+      Zlength(l_r_prefix) == i &&
+      (val_r_prefix + cy * Z::pow(UINT_MOD, i) == val_a_prefix + val_b_prefix) &&
+      store_uint_array(ap@pre, n@pre, l_a) *
+      store_undef_uint_array_rec(ap@pre, n@pre, cap_a) *
+      store_uint_array(bp@pre, n@pre, l_b) *
+      store_undef_uint_array_rec(bp@pre, n@pre, cap_b) *
+      store_uint_array(rp@pre, i, l_r_prefix) *
+      store_uint_array_rec(rp@pre, i, cap_r, l_r_suffix)
+  */
+  while (i < n)
     {
+      /*@
+        Given l_a l_b l_r_prefix l_r_suffix val_a_prefix val_b_prefix val_r_prefix
+      */
+      /*@ 0 <= cy && cy <= UINT_MAX by local */
       unsigned int a, b, r;
       a = ap[i]; b = bp[i];
       r = a + cy;
       cy = (r < cy);
       r += b;
       cy += (r < b);
+      /*@
+        0 <= i && i < n@pre && n@pre <= cap_r &&
+        store_uint_array(rp@pre, i, l_r_prefix) *
+        store_uint_array_rec(rp@pre, i, cap_r, l_r_suffix)
+        which implies
+        exists a l_r_suffix',
+        l_r_suffix == cons(a, l_r_suffix') && 0 <= i && i < n@pre && n@pre <= cap_r &&
+        store_uint_array_rec(rp@pre, i+1, cap_r, l_r_suffix') *
+        store_uint_array(rp@pre, i+1, app(l_r_prefix, cons(a, nil)))
+      */
       rp[i] = r;
+      ++i;
     }
   return cy;
-}*/
+}
 
 /*不同位数的多精度数相加，返回最后的进位*/
 /*unsigned int
diff --git a/projects/mini-gmp.h b/projects/mini-gmp.h
index 08af83a..2c67d96 100755
--- a/projects/mini-gmp.h
+++ b/projects/mini-gmp.h
@@ -84,7 +84,7 @@ void mpn_copyi (unsigned int *d, unsigned int *s, int n);
 int mpn_cmp (unsigned int *ap, unsigned int *bp, int n);
 
 unsigned int mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b);
-unsigned int mpn_add_n (unsigned int *, unsigned int *, unsigned int *, int);
+unsigned int mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n);
 unsigned int mpn_add (unsigned int *, unsigned int *, int, unsigned int *, int);
 
 unsigned int mpn_sub_1 (unsigned int *, unsigned int *, int, unsigned int);