Library dirichlet_why

Require Export dirichlet_aux.
Require Export WhyFloatsStrictLegacy.
Local Coercion FtoRradix: Float.float >-> R.

Lemma forward_prop_ensures_default_po_3 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  
  
  (Rle
   (Rdiv
    (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (double_value
                                                             dx_8))
   (1 / 9007199254740992)%R).

Lemma forward_prop_ensures_default_po_4 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
   (Rle (0)%R (double_value a_1)).

Lemma forward_prop_ensures_default_po_5 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
   (Rle (double_value a_1) (1)%R).

Lemma forward_prop_ensures_default_po_6 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
   (Rlt (0)%R (double_exact a_1)).

Lemma forward_prop_ensures_default_po_7 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
   (Rle (double_exact a_1) (1)%R).

Lemma forward_prop_ensures_default_po_8 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  
   (Rle (double_round_error a_1) (1 / 562949953421312)%R).

Lemma forward_prop_ensures_default_po_11 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer doubleP)),
  forall (HW_26: result9 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_0: (memory doubleP double)),
  forall (HW_27: doubleP_doubleM_double_xM_18_0 =
                 (store doubleP_doubleM_double_xM_18 result9 result8)),
  forall (result10: int32),
  forall (HW_28: (integer_of_int32 result10) = 1),
  forall (i_6: int32),
  forall (HW_29: i_6 = result10),
  
  
  (analytic_error
   p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_0).

Lemma forward_prop_ensures_default_po_14 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer doubleP)),
  forall (HW_26: result9 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_0: (memory doubleP double)),
  forall (HW_27: doubleP_doubleM_double_xM_18_0 =
                 (store doubleP_doubleM_double_xM_18 result9 result8)),
  forall (result10: int32),
  forall (HW_28: (integer_of_int32 result10) = 1),
  forall (i_6: int32),
  forall (HW_29: i_6 = result10),
  forall (doubleP_doubleM_double_xM_18_1: (memory doubleP double)),
  forall (i_6_0: int32),
  forall (HW_30: ( 1 <= (integer_of_int32 i_6_0) /\
                  (integer_of_int32 i_6_0) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_0) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_1))),
  forall (HW_32: (integer_of_int32 i_6_0) < (integer_of_int32 ni_0)),
  forall (result11: double),
  forall (HW_33: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 i_6_0)) result11)),
  forall (result12: double),
  forall (HW_34: (mul_double_post nearest_even result11 dx_8 result12)),
  forall (result13: double),
  forall (HW_35:
                 (
                  (Rle (double_round_error result13)
                   (Rmult (14)%R (1 / 4503599627370496)%R)) /\
                 
                 (eq (double_exact result13) (p0 (double_exact result12))))),
  forall (result14: (pointer doubleP)),
  forall (HW_36: result14 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 i_6_0)))),
  forall (doubleP_doubleM_double_xM_18_2: (memory doubleP double)),
  forall (HW_37: doubleP_doubleM_double_xM_18_2 =
                 (store doubleP_doubleM_double_xM_18_1 result14 result13)),
  forall (result15: int32),
  forall (HW_38: (integer_of_int32 result15) = ((integer_of_int32 i_6_0) + 1)),
  forall (i_6_1: int32),
  forall (HW_39: i_6_1 = result15),
  
  
  (analytic_error
   p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_1) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_2).

Lemma forward_prop_ensures_default_po_15 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer doubleP)),
  forall (HW_26: result9 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_0: (memory doubleP double)),
  forall (HW_27: doubleP_doubleM_double_xM_18_0 =
                 (store doubleP_doubleM_double_xM_18 result9 result8)),
  forall (result10: int32),
  forall (HW_28: (integer_of_int32 result10) = 1),
  forall (i_6: int32),
  forall (HW_29: i_6 = result10),
  forall (doubleP_doubleM_double_xM_18_1: (memory doubleP double)),
  forall (i_6_0: int32),
  forall (HW_30: ( 1 <= (integer_of_int32 i_6_0) /\
                  (integer_of_int32 i_6_0) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_0) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_1))),
  forall (HW_40: (integer_of_int32 i_6_0) >= (integer_of_int32 ni_0)),
  forall (result11: double),
  forall (HW_41: (eq (double_value result11) (0)%R) /\
                 (eq (double_exact result11) (0)%R) /\
                 (eq (double_model result11) (0)%R)),
  forall (result12: (pointer doubleP)),
  forall (HW_42: result12 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_2: (memory doubleP double)),
  forall (HW_43: doubleP_doubleM_double_xM_18_2 =
                 (store doubleP_doubleM_double_xM_18_1 result12 result11)),
  
  (analytic_error
   p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_2).

Lemma forward_prop_ensures_default_po_18 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer doubleP)),
  forall (HW_26: result9 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_0: (memory doubleP double)),
  forall (HW_27: doubleP_doubleM_double_xM_18_0 =
                 (store doubleP_doubleM_double_xM_18 result9 result8)),
  forall (result10: int32),
  forall (HW_28: (integer_of_int32 result10) = 1),
  forall (i_6: int32),
  forall (HW_29: i_6 = result10),
  forall (doubleP_doubleM_double_xM_18_1: (memory doubleP double)),
  forall (i_6_0: int32),
  forall (HW_30: ( 1 <= (integer_of_int32 i_6_0) /\
                  (integer_of_int32 i_6_0) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_0) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_1))),
  forall (HW_40: (integer_of_int32 i_6_0) >= (integer_of_int32 ni_0)),
  forall (result11: double),
  forall (HW_41: (eq (double_value result11) (0)%R) /\
                 (eq (double_exact result11) (0)%R) /\
                 (eq (double_model result11) (0)%R)),
  forall (result12: (pointer doubleP)),
  forall (HW_42: result12 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_2: (memory doubleP double)),
  forall (HW_43: doubleP_doubleM_double_xM_18_2 =
                 (store doubleP_doubleM_double_xM_18_1 result12 result11)),
  forall (HW_44:
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_2)),
  forall (result13: double),
  forall (HW_45: (eq (double_value result13) (0)%R) /\
                 (eq (double_exact result13) (0)%R) /\
                 (eq (double_model result13) (0)%R)),
  forall (result14: (pointer doubleP)),
  forall (HW_46: result14 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_3: (memory doubleP double)),
  forall (HW_47: doubleP_doubleM_double_xM_18_3 =
                 (store
                  doubleP_doubleM_double_xM_18_2 (shift result14 1) result13)),
  forall (result15: int32),
  forall (HW_48: (integer_of_int32 result15) = 1),
  forall (i_6_1: int32),
  forall (HW_49: i_6_1 = result15),
  
  
  (analytic_error
   p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_1) - 1) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_3).

Lemma forward_prop_ensures_default_po_24 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer doubleP)),
  forall (HW_26: result9 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_0: (memory doubleP double)),
  forall (HW_27: doubleP_doubleM_double_xM_18_0 =
                 (store doubleP_doubleM_double_xM_18 result9 result8)),
  forall (result10: int32),
  forall (HW_28: (integer_of_int32 result10) = 1),
  forall (i_6: int32),
  forall (HW_29: i_6 = result10),
  forall (doubleP_doubleM_double_xM_18_1: (memory doubleP double)),
  forall (i_6_0: int32),
  forall (HW_30: ( 1 <= (integer_of_int32 i_6_0) /\
                  (integer_of_int32 i_6_0) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_0) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_1))),
  forall (HW_40: (integer_of_int32 i_6_0) >= (integer_of_int32 ni_0)),
  forall (result11: double),
  forall (HW_41: (eq (double_value result11) (0)%R) /\
                 (eq (double_exact result11) (0)%R) /\
                 (eq (double_model result11) (0)%R)),
  forall (result12: (pointer doubleP)),
  forall (HW_42: result12 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_2: (memory doubleP double)),
  forall (HW_43: doubleP_doubleM_double_xM_18_2 =
                 (store doubleP_doubleM_double_xM_18_1 result12 result11)),
  forall (HW_44:
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_2)),
  forall (result13: double),
  forall (HW_45: (eq (double_value result13) (0)%R) /\
                 (eq (double_exact result13) (0)%R) /\
                 (eq (double_model result13) (0)%R)),
  forall (result14: (pointer doubleP)),
  forall (HW_46: result14 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_3: (memory doubleP double)),
  forall (HW_47: doubleP_doubleM_double_xM_18_3 =
                 (store
                  doubleP_doubleM_double_xM_18_2 (shift result14 1) result13)),
  forall (result15: int32),
  forall (HW_48: (integer_of_int32 result15) = 1),
  forall (i_6_1: int32),
  forall (HW_49: i_6_1 = result15),
  forall (doubleP_doubleM_double_xM_18_4: (memory doubleP double)),
  forall (i_6_2: int32),
  forall (HW_50: ( 1 <= (integer_of_int32 i_6_2) /\
                  (integer_of_int32 i_6_2) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_2) - 1) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_4))),
  forall (HW_52: (integer_of_int32 i_6_2) < (integer_of_int32 ni_0)),
  forall (HW_53:
                 (Rle
                  (Rabs
                   (double_value
                    (select
                     doubleP_doubleM_double_xM_18_4 (shift
                                                     (select
                                                      double_xP_double_xM_result_7 (
                                                      shift
                                                      p_6 ((integer_of_int32
                                                            i_6_2) -
                                                          1))) 0))))
                  (2)%R)),
  forall (HW_54:
                 (Rle
                  (Rabs
                   (double_value
                    (select
                     doubleP_doubleM_double_xM_18_4 (shift
                                                     (select
                                                      double_xP_double_xM_result_7 (
                                                      shift
                                                      p_6 (integer_of_int32
                                                           i_6_2))) 0))))
                  (2)%R)),
  forall (HW_55:
                 (Rle
                  (Rabs
                   (double_value
                    (select
                     doubleP_doubleM_double_xM_18_4 (shift
                                                     (select
                                                      double_xP_double_xM_result_7 (
                                                      shift
                                                      p_6 ((integer_of_int32
                                                            i_6_2) +
                                                          1))) 0))))
                  (2)%R)),
  forall (result16: int32),
  forall (HW_56: (integer_of_int32 result16) = ((integer_of_int32 i_6_2) + 1)),
  forall (result17: (pointer doubleP)),
  forall (HW_57: result17 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32
                                                     result16)))),
  forall (result18: double),
  forall (HW_58: result18 =
                 (select doubleP_doubleM_double_xM_18_4 (shift result17 0))),
  forall (result19: double),
  forall (HW_59: (eq (double_value result19) (2)%R) /\
                 (eq (double_exact result19) (2)%R) /\
                 (eq (double_model result19) (2)%R)),
  forall (result20: (pointer doubleP)),
  forall (HW_60: result20 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 i_6_2)))),
  forall (result21: double),
  forall (HW_61: result21 =
                 (select doubleP_doubleM_double_xM_18_4 (shift result20 0))),
  forall (result22: double),
  forall (HW_62: (mul_double_post nearest_even result19 result21 result22)),
  forall (result23: double),
  forall (HW_63: (sub_double_post nearest_even result18 result22 result23)),
  forall (result24: int32),
  forall (HW_64: (integer_of_int32 result24) = ((integer_of_int32 i_6_2) - 1)),
  forall (result25: (pointer doubleP)),
  forall (HW_65: result25 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32
                                                     result24)))),
  forall (result26: double),
  forall (HW_66: result26 =
                 (select doubleP_doubleM_double_xM_18_4 (shift result25 0))),
  forall (result27: double),
  forall (HW_67: (add_double_post nearest_even result23 result26 result27)),
  forall (dp: double),
  forall (HW_68: dp = result27),
  forall (result28: (pointer doubleP)),
  forall (HW_69: result28 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 i_6_2)))),
  forall (result29: double),
  forall (HW_70: result29 =
                 (select doubleP_doubleM_double_xM_18_4 (shift result28 0))),
  forall (result30: double),
  forall (HW_71: (eq (double_value result30) (05 / 10)%R) /\
                 (eq (double_exact result30) (05 / 10)%R) /\
                 (eq (double_model result30) (05 / 10)%R)),
  forall (result31: double),
  forall (HW_72: (mul_double_post nearest_even result30 a_1 result31)),
  forall (result32: double),
  forall (HW_73: (mul_double_post nearest_even result31 dp result32)),
  forall (result33: double),
  forall (HW_74: (add_double_post nearest_even result29 result32 result33)),
  forall (result34: (pointer doubleP)),
  forall (HW_75: result34 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 i_6_2)))),
  forall (doubleP_doubleM_double_xM_18_5: (memory doubleP double)),
  forall (HW_76: doubleP_doubleM_double_xM_18_5 =
                 (store
                  doubleP_doubleM_double_xM_18_4 (shift result34 1) result33)),
  forall (result35: int32),
  forall (HW_77: (integer_of_int32 result35) = ((integer_of_int32 i_6_2) + 1)),
  forall (i_6_3: int32),
  forall (HW_78: i_6_3 = result35),
  
  
  (analytic_error
   p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_3) - 1) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_5).

Lemma forward_prop_ensures_default_po_25 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer doubleP)),
  forall (HW_26: result9 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_0: (memory doubleP double)),
  forall (HW_27: doubleP_doubleM_double_xM_18_0 =
                 (store doubleP_doubleM_double_xM_18 result9 result8)),
  forall (result10: int32),
  forall (HW_28: (integer_of_int32 result10) = 1),
  forall (i_6: int32),
  forall (HW_29: i_6 = result10),
  forall (doubleP_doubleM_double_xM_18_1: (memory doubleP double)),
  forall (i_6_0: int32),
  forall (HW_30: ( 1 <= (integer_of_int32 i_6_0) /\
                  (integer_of_int32 i_6_0) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_0) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_1))),
  forall (HW_40: (integer_of_int32 i_6_0) >= (integer_of_int32 ni_0)),
  forall (result11: double),
  forall (HW_41: (eq (double_value result11) (0)%R) /\
                 (eq (double_exact result11) (0)%R) /\
                 (eq (double_model result11) (0)%R)),
  forall (result12: (pointer doubleP)),
  forall (HW_42: result12 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_2: (memory doubleP double)),
  forall (HW_43: doubleP_doubleM_double_xM_18_2 =
                 (store doubleP_doubleM_double_xM_18_1 result12 result11)),
  forall (HW_44:
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_2)),
  forall (result13: double),
  forall (HW_45: (eq (double_value result13) (0)%R) /\
                 (eq (double_exact result13) (0)%R) /\
                 (eq (double_model result13) (0)%R)),
  forall (result14: (pointer doubleP)),
  forall (HW_46: result14 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_3: (memory doubleP double)),
  forall (HW_47: doubleP_doubleM_double_xM_18_3 =
                 (store
                  doubleP_doubleM_double_xM_18_2 (shift result14 1) result13)),
  forall (result15: int32),
  forall (HW_48: (integer_of_int32 result15) = 1),
  forall (i_6_1: int32),
  forall (HW_49: i_6_1 = result15),
  forall (doubleP_doubleM_double_xM_18_4: (memory doubleP double)),
  forall (i_6_2: int32),
  forall (HW_50: ( 1 <= (integer_of_int32 i_6_2) /\
                  (integer_of_int32 i_6_2) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_2) - 1) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_4))),
  forall (HW_79: (integer_of_int32 i_6_2) >= (integer_of_int32 ni_0)),
  forall (result16: double),
  forall (HW_80: (eq (double_value result16) (0)%R) /\
                 (eq (double_exact result16) (0)%R) /\
                 (eq (double_model result16) (0)%R)),
  forall (result17: (pointer doubleP)),
  forall (HW_81: result17 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_5: (memory doubleP double)),
  forall (HW_82: doubleP_doubleM_double_xM_18_5 =
                 (store
                  doubleP_doubleM_double_xM_18_4 (shift result17 1) result16)),
  
  (analytic_error
   p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_5).

Lemma forward_prop_ensures_default_po_31 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer doubleP)),
  forall (HW_26: result9 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_0: (memory doubleP double)),
  forall (HW_27: doubleP_doubleM_double_xM_18_0 =
                 (store doubleP_doubleM_double_xM_18 result9 result8)),
  forall (result10: int32),
  forall (HW_28: (integer_of_int32 result10) = 1),
  forall (i_6: int32),
  forall (HW_29: i_6 = result10),
  forall (doubleP_doubleM_double_xM_18_1: (memory doubleP double)),
  forall (i_6_0: int32),
  forall (HW_30: ( 1 <= (integer_of_int32 i_6_0) /\
                  (integer_of_int32 i_6_0) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_0) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_1))),
  forall (HW_40: (integer_of_int32 i_6_0) >= (integer_of_int32 ni_0)),
  forall (result11: double),
  forall (HW_41: (eq (double_value result11) (0)%R) /\
                 (eq (double_exact result11) (0)%R) /\
                 (eq (double_model result11) (0)%R)),
  forall (result12: (pointer doubleP)),
  forall (HW_42: result12 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_2: (memory doubleP double)),
  forall (HW_43: doubleP_doubleM_double_xM_18_2 =
                 (store doubleP_doubleM_double_xM_18_1 result12 result11)),
  forall (HW_44:
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_2)),
  forall (result13: double),
  forall (HW_45: (eq (double_value result13) (0)%R) /\
                 (eq (double_exact result13) (0)%R) /\
                 (eq (double_model result13) (0)%R)),
  forall (result14: (pointer doubleP)),
  forall (HW_46: result14 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_3: (memory doubleP double)),
  forall (HW_47: doubleP_doubleM_double_xM_18_3 =
                 (store
                  doubleP_doubleM_double_xM_18_2 (shift result14 1) result13)),
  forall (result15: int32),
  forall (HW_48: (integer_of_int32 result15) = 1),
  forall (i_6_1: int32),
  forall (HW_49: i_6_1 = result15),
  forall (doubleP_doubleM_double_xM_18_4: (memory doubleP double)),
  forall (i_6_2: int32),
  forall (HW_50: ( 1 <= (integer_of_int32 i_6_2) /\
                  (integer_of_int32 i_6_2) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_2) - 1) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_4))),
  forall (HW_79: (integer_of_int32 i_6_2) >= (integer_of_int32 ni_0)),
  forall (result16: double),
  forall (HW_80: (eq (double_value result16) (0)%R) /\
                 (eq (double_exact result16) (0)%R) /\
                 (eq (double_model result16) (0)%R)),
  forall (result17: (pointer doubleP)),
  forall (HW_81: result17 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_5: (memory doubleP double)),
  forall (HW_82: doubleP_doubleM_double_xM_18_5 =
                 (store
                  doubleP_doubleM_double_xM_18_4 (shift result17 1) result16)),
  forall (HW_83:
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_5)),
  forall (result18: int32),
  forall (HW_84: (integer_of_int32 result18) = 1),
  forall (k_7: int32),
  forall (HW_85: k_7 = result18),
  forall (doubleP_doubleM_double_xM_18_6: (memory doubleP double)),
  forall (k_7_0: int32),
  forall (HW_86: ( 1 <= (integer_of_int32 k_7_0) /\
                  (integer_of_int32 k_7_0) <=
                 (integer_of_int32 nk) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) (
                  integer_of_int32 k_7_0) a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_6))),
  forall (HW_88: (integer_of_int32 k_7_0) < (integer_of_int32 nk)),
  forall (result19: double),
  forall (HW_89: (eq (double_value result19) (0)%R) /\
                 (eq (double_exact result19) (0)%R) /\
                 (eq (double_model result19) (0)%R)),
  forall (result20: (pointer doubleP)),
  forall (HW_90: result20 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (result21: int32),
  forall (HW_91: (integer_of_int32 result21) = ((integer_of_int32 k_7_0) + 1)),
  forall (doubleP_doubleM_double_xM_18_7: (memory doubleP double)),
  forall (HW_92: doubleP_doubleM_double_xM_18_7 =
                 (store
                  doubleP_doubleM_double_xM_18_6 (shift
                                                  result20 (integer_of_int32
                                                            result21)) result19)),
  forall (result22: int32),
  forall (HW_93: (integer_of_int32 result22) = 1),
  forall (i_6_3: int32),
  forall (HW_94: i_6_3 = result22),
  
  
  (analytic_error
   p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_3) - 1) ((integer_of_int32
                                                                k_7_0) +
                                                              1) a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_7).

Lemma forward_prop_ensures_default_po_32 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer doubleP)),
  forall (HW_26: result9 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_0: (memory doubleP double)),
  forall (HW_27: doubleP_doubleM_double_xM_18_0 =
                 (store doubleP_doubleM_double_xM_18 result9 result8)),
  forall (result10: int32),
  forall (HW_28: (integer_of_int32 result10) = 1),
  forall (i_6: int32),
  forall (HW_29: i_6 = result10),
  forall (doubleP_doubleM_double_xM_18_1: (memory doubleP double)),
  forall (i_6_0: int32),
  forall (HW_30: ( 1 <= (integer_of_int32 i_6_0) /\
                  (integer_of_int32 i_6_0) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_0) - 1) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_1))),
  forall (HW_40: (integer_of_int32 i_6_0) >= (integer_of_int32 ni_0)),
  forall (result11: double),
  forall (HW_41: (eq (double_value result11) (0)%R) /\
                 (eq (double_exact result11) (0)%R) /\
                 (eq (double_model result11) (0)%R)),
  forall (result12: (pointer doubleP)),
  forall (HW_42: result12 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_2: (memory doubleP double)),
  forall (HW_43: doubleP_doubleM_double_xM_18_2 =
                 (store doubleP_doubleM_double_xM_18_1 result12 result11)),
  forall (HW_44:
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 0 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_2)),
  forall (result13: double),
  forall (HW_45: (eq (double_value result13) (0)%R) /\
                 (eq (double_exact result13) (0)%R) /\
                 (eq (double_model result13) (0)%R)),
  forall (result14: (pointer doubleP)),
  forall (HW_46: result14 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (doubleP_doubleM_double_xM_18_3: (memory doubleP double)),
  forall (HW_47: doubleP_doubleM_double_xM_18_3 =
                 (store
                  doubleP_doubleM_double_xM_18_2 (shift result14 1) result13)),
  forall (result15: int32),
  forall (HW_48: (integer_of_int32 result15) = 1),
  forall (i_6_1: int32),
  forall (HW_49: i_6_1 = result15),
  forall (doubleP_doubleM_double_xM_18_4: (memory doubleP double)),
  forall (i_6_2: int32),
  forall (HW_50: ( 1 <= (integer_of_int32 i_6_2) /\
                  (integer_of_int32 i_6_2) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_2) - 1) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_4))),
  forall (HW_79: (integer_of_int32 i_6_2) >= (integer_of_int32 ni_0)),
  forall (result16: double),
  forall (HW_80: (eq (double_value result16) (0)%R) /\
                 (eq (double_exact result16) (0)%R) /\
                 (eq (double_model result16) (0)%R)),
  forall (result17: (pointer doubleP)),
  forall (HW_81: result17 =
                 (select
                  double_xP_double_xM_result_7 (shift
                                                p_6 (integer_of_int32 ni_0)))),
  forall (doubleP_doubleM_double_xM_18_5: (memory doubleP double)),
  forall (HW_82: doubleP_doubleM_double_xM_18_5 =
                 (store
                  doubleP_doubleM_double_xM_18_4 (shift result17 1) result16)),
  forall (HW_83:
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) 1 a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_5)),
  forall (result18: int32),
  forall (HW_84: (integer_of_int32 result18) = 1),
  forall (k_7: int32),
  forall (HW_85: k_7 = result18),
  forall (doubleP_doubleM_double_xM_18_6: (memory doubleP double)),
  forall (k_7_0: int32),
  forall (HW_86: ( 1 <= (integer_of_int32 k_7_0) /\
                  (integer_of_int32 k_7_0) <=
                 (integer_of_int32 nk) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) (integer_of_int32 ni_0) (
                  integer_of_int32 k_7_0) a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_6))),
  forall (HW_88: (integer_of_int32 k_7_0) < (integer_of_int32 nk)),
  forall (result19: double),
  forall (HW_89: (eq (double_value result19) (0)%R) /\
                 (eq (double_exact result19) (0)%R) /\
                 (eq (double_model result19) (0)%R)),
  forall (result20: (pointer doubleP)),
  forall (HW_90: result20 =
                 (select double_xP_double_xM_result_7 (shift p_6 0))),
  forall (result21: int32),
  forall (HW_91: (integer_of_int32 result21) = ((integer_of_int32 k_7_0) + 1)),
  forall (doubleP_doubleM_double_xM_18_7: (memory doubleP double)),
  forall (HW_92: doubleP_doubleM_double_xM_18_7 =
                 (store
                  doubleP_doubleM_double_xM_18_6 (shift
                                                  result20 (integer_of_int32
                                                            result21)) result19)),
  forall (result22: int32),
  forall (HW_93: (integer_of_int32 result22) = 1),
  forall (i_6_3: int32),
  forall (HW_94: i_6_3 = result22),
  forall (doubleP_doubleM_double_xM_18_8: (memory doubleP double)),
  forall (i_6_4: int32),
  forall (HW_95: ( 1 <= (integer_of_int32 i_6_4) /\
                  (integer_of_int32 i_6_4) <=
                 (integer_of_int32 ni_0) /\
                 
                 (analytic_error
                  p_6 (integer_of_int32 ni_0) ((integer_of_int32 i_6_4) - 1)
                  ((integer_of_int32 k_7_0) + 1) a_1 dt double_xP_double_xM_result_7 doubleP_doubleM_double_xM_18_8))),
  forall (HW_97: (integer_of_int32 i_6_4) < (integer_of_int32 ni_0)),
  
  (Rle
   (Rabs
    (double_value
     (select
      doubleP_doubleM_double_xM_18_8 (shift
                                      (select
                                       double_xP_double_xM_result_7 (
                                       shift
                                       p_6 ((integer_of_int32 i_6_4) - 1))) (
                                      integer_of_int32 k_7_0)))))
   (2)%R).

Lemma forward_prop_ensures_default_po_33 :
  forall (ni_0: int32),
  forall (nk: int32),
  forall (dt: double),
  forall (v: double),
  forall (l: double),
  forall (doubleP_double_xM_18_alloc_table: (alloc_table doubleP)),
  forall (double_xP_result_7_alloc_table: (alloc_table double_xP)),
  forall (double_xP_double_xM_result_7: (memory double_xP (pointer doubleP))),
  forall (doubleP_doubleM_double_xM_18: (memory doubleP double)),
  forall (HW_1: ( (integer_of_int32 ni_0) >= 2 /\
                 (integer_of_int32 nk) >= 2 /\
                 ~(eq (double_value l) (0)%R) /\
                 (Rgt (double_value dt) (0)%R) /\
                 (Rgt (double_exact dt) (0)%R) /\
                 (eq (double_exact v) c) /\
                 (eq (double_exact v) (double_value v)) /\
                
                (Rle
                 (1 / 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)%R
                 (double_exact dt)) /\
                 (integer_of_int32 ni_0) <= 2147483646 /\
                 (integer_of_int32 nk) <= 7598581 /\
                
                (Rle (Rmult (IZR (integer_of_int32 nk)) (double_exact dt))
                 T_max) /\
                
                (Rle
                 (Rdiv
                  (Rabs (Rminus (double_exact dt) (double_value dt))) (
                  double_value dt))
                 (1 / 2251799813685248)%R) /\
                
                (Rle
                 (1 / 3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376)%R
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)) /\
                
                (Rle
                 (Rmult
                  (Rmult (double_exact dt) (IZR (integer_of_int32 ni_0))) c)
                 (Rminus (1)%R (1 / 1125899906842624)%R)) /\
                
                (Rlt
                 (sqrt
                  (Rplus
                   (Rdiv
                    (1)%R (IZR
                           ((integer_of_int32 ni_0) *
                           (integer_of_int32 ni_0)))) (Rmult
                                                       (double_exact dt) (
                                                       double_exact dt))))
                 alpha_conv))),
  forall (result: double),
  forall (HW_10: (eq (double_value result) (1)%R) /\
                 (eq (double_exact result) (1)%R) /\
                 (eq (double_model result) (1)%R)),
  forall (result0: double),
  forall (HW_11: (double_of_real_post
                  nearest_even (IZR (integer_of_int32 ni_0)) result0)),
  forall (result1: double),
  forall (HW_12: ~(eq (double_value result0) (0)%R) /\
                 (div_double_post nearest_even result result0 result1)),
  forall (dx_8: double),
  forall (HW_13: dx_8 = result1),
  forall (HW_14:
                 ( (Rgt (double_value dx_8) (0)%R) /\
                  (Rle (double_value dx_8) (05 / 10)%R) /\
                 
                 (Rle
                  (Rdiv
                   (Rabs (Rminus (double_exact dx_8) (double_value dx_8))) (
                   double_value dx_8))
                  (1 / 9007199254740992)%R))),
  forall (result2: double),
  forall (HW_15: ~(eq (double_value dx_8) (0)%R) /\
                 (div_double_post nearest_even dt dx_8 result2)),
  forall (result3: double),
  forall (HW_16: (mul_double_post nearest_even result2 v result3)),
  forall (a1: double),
  forall (HW_17: a1 = result3),
  forall (result4: double),
  forall (HW_18: (mul_double_post nearest_even a1 a1 result4)),
  forall (a_1: double),
  forall (HW_19: a_1 = result4),
  forall (HW_20: ( (Rle (0)%R (double_value a_1)) /\
                  (Rle (double_value a_1) (1)%R) /\
                  (Rlt (0)%R (double_exact a_1)) /\
                  (Rle (double_exact a_1) (1)%R) /\
                 
                 (Rle (double_round_error a_1) (1 / 562949953421312)%R))),
  forall (result5: int32),
  forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 ni_0) + 1)),
  forall (result6: int32),
  forall (HW_22: (integer_of_int32 result6) = ((integer_of_int32 nk) + 1)),
  forall (result7: (pointer double_xP)),
  forall (HW_23:
                 (
                  (offset_min double_xP_result_7_alloc_table result7) <= 0 /\
                 
                 (offset_max double_xP_result_7_alloc_table result7) >=
                 ((integer_of_int32 result5) - 1) /\
                 
                 (forall (i_4:Z),
                  (0 <= i_4 /\ i_4 < (integer_of_int32 result5) ->
                   (offset_min
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) <=
                   0 /\
                   (offset_max
                    doubleP_double_xM_18_alloc_table (select
                                                      double_xP_double_xM_result_7 (
                                                      shift result7 i_4))) >=
                   ((integer_of_int32 result6) - 1))) /\
                 
                 (separated_matrix
                  result7 (integer_of_int32 result5) double_xP_double_xM_result_7))),
  forall (p_6: (pointer double_xP)),
  forall (HW_24: p_6 = result7),
  forall (result8: double),
  forall (HW_25: (eq (double_value result8) (0)%R) /\
                 (eq (double_exact result8) (0)%R) /\
                 (eq (double_model result8) (0)%R)),
  forall (result9: (pointer