## lustrec/optim/oversampling/out/typed/f_step_post.coq @ 6a93d814

1 |
(* ---------------------------------------------------------- *) |
---|---|

2 |
(* --- Post-condition (file oversampling0_4.c, line 153) in 'f_step' --- *) |

3 |
(* ---------------------------------------------------------- *) |

4 |
Require Import ZArith. |

5 |
Require Import Reals. |

6 |
Require Import BuiltIn. |

7 |
Require Import bool.Bool. |

8 |
Require Import int.Int. |

9 |
Require Import int.Abs. |

10 |
Require Import int.ComputerDivision. |

11 |
Require Import real.Real. |

12 |
Require Import real.RealInfix. |

13 |
Require Import real.FromInt. |

14 |
Require Import map.Map. |

15 |
Require Import Qedlib. |

16 |
Require Import Qed. |

17 | |

18 |
Require Import S_f_mem_pack. |

19 |
Require Import Memory. |

20 |
Require Import Cint. |

21 |
Require Import Compound. |

22 |
Require Import Axiomatic. |

23 | |

24 |
Goal |

25 |
forall (i_1 i : Z), |

26 |
forall (t : array Z), |

27 |
forall (t_2 t_1 : farray addr Z), |

28 |
forall (t_3 : farray addr addr), |

29 |
forall (a_2 a_1 a : addr), |

30 |
forall (f_1 f : S_f_mem_pack), |

31 |
let a_3 := t_3.[ (shiftfield_F_f_mem_ni_2 a_2) ] in |

32 |
let x := (1%Z + i_1%Z)%Z in |

33 |
let m := t_2.[ a_1 <- x ] in |

34 |
let a_4 := (shiftfield_F__arrow_reg__first |

35 |
((shiftfield_F__arrow_mem__reg a_3))) in |

36 |
let x_1 := (m.[ a_4 ])%Z in |

37 |
let x_2 := (1%Z + i%Z)%Z in |

38 |
let m_1 := t_1.[ a <- x_2 ] in |

39 |
let a_5 := (shiftfield_F_f_reg___f_2 ((shiftfield_F_f_mem__reg a_2))) in |

40 |
let m_2 := m_1.[ a_5 <- x_2 ] in |

41 |
let x_3 := (t_1.[ a_1 ])%Z in |

42 |
let x_4 := (m_2.[ a_1 ])%Z in |

43 |
let x_5 := (m_2.[ a ])%Z in |

44 |
(a <> a_1) -> |

45 |
((IsS_f_mem_pack f)) -> |

46 |
((IsS_f_mem_pack f_1)) -> |

47 |
((framed t_3)) -> |

48 |
((linked t)) -> |

49 |
((is_sint32 i%Z)) -> |

50 |
((is_sint32 i_1%Z)) -> |

51 |
(a <> a_3) -> |

52 |
(a_1 <> a_3) -> |

53 |
((valid_rw t a 1%Z)) -> |

54 |
((valid_rw t a_1 1%Z)) -> |

55 |
((P_valid_f t t_3 a_2)) -> |

56 |
((((region ((base a))%Z)) <= 0)%Z) -> |

57 |
((((region ((base a_1))%Z)) <= 0)%Z) -> |

58 |
((((region ((base a_2))%Z)) <= 0)%Z) -> |

59 |
((separated a_2 2%Z a 1%Z)) -> |

60 |
((separated a_2 2%Z a_1 1%Z)) -> |

61 |
((P_f_pack2 t_3 t_2 f_1 a_2)) -> |

62 |
((separated a_2 2%Z a_3 1%Z)) -> |

63 |
((is_uint32 x_1)) -> |

64 |
((P_f_pack2 t_3 m_2 f a_2)) -> |

65 |
(itep ((0 = x_1)%Z) (t_1 = m) (t_1 = (m.[ a_4 <- (0)%Z ]))) -> |

66 |
(itep ((0 = x_1)%Z) ((i = (t_1.[ a_5 ]))%Z) ((0 = i)%Z)) -> |

67 |
(forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |

68 |
(forall (f_3 : S_f_mem_pack), (P_f_pack0) -> ((IsS_f_mem_pack f_3)) -> |

69 |
((P_f_pack2 t_3 t_2 f_2 a_2)) -> (P_trans_fA))) -> |

70 |
(forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |

71 |
(forall (f_3 : S_f_mem_pack), (P_f_pack0) -> ((IsS_f_mem_pack f_3)) -> |

72 |
((P_f_pack2 t_3 t_2 f_2 a_2)) -> ((P_trans_fB i_1%Z x)))) -> |

73 |
(forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |

74 |
(forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) -> |

75 |
((P_f_pack1 t_3 t_1 f_3 a_2)) -> ((P_f_pack2 t_3 t_2 f_2 a_2)) -> |

76 |
((P_trans_fD i_1%Z f_2 f_3 x_3 i%Z)))) -> |

77 |
(forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |

78 |
(forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) -> |

79 |
((P_f_pack2 t_3 t_2 f_2 a_2)) -> ((P_f_pack1 t_3 m_1 f_3 a_2)) -> |

80 |
((P_trans_fE i_1%Z f_2 f_3 (m_1.[ a_1 ])%Z x_2)))) -> |

81 |
(forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |

82 |
(forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) -> |

83 |
((P_f_pack2 t_3 t_2 f_2 a_2)) -> ((P_f_pack2 t_3 m_2 f_3 a_2)) -> |

84 |
((P_trans_fF i_1%Z f_2 f_3 x_4 x_5)))) -> |

85 |
(forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |

86 |
(forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) -> |

87 |
((P_f_pack1 t_3 t_1 f_3 a_2)) -> ((P_f_pack2 t_3 t_2 f_2 a_2)) -> |

88 |
((P_trans_fC i_1%Z f_2 f_3 x_3 x_1)))) -> |

89 |
((P_trans_fF i_1%Z f_1 f x_4 x_5)). |

90 |