1

(*  *)

2

(*  Postcondition (file oversampling0_4.c, line 329) in 'g_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_g_mem_pack.

19

Require Import Memory.

20

Require Import Cint.

21

Require Import Compound.

22

Require Import Axiomatic.

23

Require Import Globals.

24

Require Import S_f_mem_pack.

25


26

Goal

27

let a := (shift_sint32 ((global (L_cpt_458)%Z)) 0%Z) in

28

let a_1 := (shift_sint32 ((global (L_last_y_459)%Z)) 0%Z) in

29

forall (i_5 i_4 i_3 i_2 i_1 i : Z),

30

forall (t : array Z),

31

forall (t_8 t_7 t_6 t_5 t_4 t_3 t_2 t_1 : farray addr Z),

32

forall (t_9 : farray addr addr),

33

forall (a_3 a_2 : addr),

34

forall (g_1 g : S_g_mem_pack),

35

let a_4 := t_9.[ (shiftfield_F_g_mem_ni_1 a_3) ] in

36

let a_5 := t_9.[ (shiftfield_F_g_mem_ni_0 a_3) ] in

37

let a_6 := t_9.[ (shiftfield_F_f_mem_ni_2 a_5) ] in

38

let x := (t_6.[ a_1 ])%Z in

39

let a_7 := (shiftfield_F__arrow_reg__first

40

((shiftfield_F__arrow_mem__reg a_4))) in

41

let x_1 := (t_8.[ a_7 ])%Z in

42

let a_8 := (shiftfield_F_g_reg___g_2 ((shiftfield_F_g_mem__reg a_3))) in

43

let x_2 := (t_7.[ a_1 ])%Z in

44

let m := t_7.[ a_8 < x_2 ] in

45

let m_1 := (((t_6.[ a < (i)%Z ]).[ a_1 < (i_1)%Z ]).[ (shiftfield_F_f_reg___f_2

46

((shiftfield_F_f_mem__reg

47

a_5))) <

48

(i_3)%Z ]).[ (shiftfield_F__arrow_reg__first

49

((shiftfield_F__arrow_mem__reg a_6))) <

50

(i_4)%Z ] in

51

let x_3 := (m_1.[ a_1 ])%Z in

52

let x_4 := (m.[ a_2 ])%Z in

53

((IsS_g_mem_pack g)) >

54

((IsS_g_mem_pack g_1)) >

55

((framed t_9)) >

56

((linked t)) >

57

((is_uint32 i_2%Z)) >

58

(a_2 <> a_4) >

59

((valid_rw t a_2 1%Z)) >

60

((P_valid_g t t_9 a_3)) >

61

((((region ((base a_2))%Z)) <= 0)%Z) >

62

((((region ((base a_3))%Z)) <= 0)%Z) >

63

((separated a_3 3%Z a_2 1%Z)) >

64

((P_g_pack3 t_9 t_8 g_1 a_3)) >

65

(a_2 <> a_6) >

66

(a_4 <> a_6) >

67

(a <> a_6) >

68

(a_1 <> a_6) >

69

((P_valid_f ((t.[ (L_cpt_458)%Z < (1)%Z ]).[ (L_last_y_459)%Z < (1)%Z ])

70

t_9 a_5)) >

71

((separated a_2 1%Z a_5 2%Z)) >

72

((separated a_3 3%Z a_5 2%Z)) >

73

((separated a_3 3%Z a_4 1%Z)) >

74

((separated a_5 2%Z a_4 1%Z)) >

75

((is_sint32 x)) >

76

((separated a_5 2%Z a 1%Z)) >

77

((separated a_5 2%Z a_1 1%Z)) >

78

((is_uint32 x_1)) >

79

((separated a_3 3%Z a_6 1%Z)) >

80

((separated a_5 2%Z a_6 1%Z)) >

81

(itep ((0 = x_1)%Z) (t_1 = t_8) (t_1 = (t_8.[ a_7 < (0)%Z ]))) >

82

((P_g_pack3 t_9 m g a_3)) >

83

(itep ((0 = i_2)%Z) (t_4 = t_6)

84

((t_4 = t_5) /\ (t_6 = (t_5.[ a_1 < (i_5)%Z ])))) >

85

(itep ((0 = x_1)%Z)

86

((t_1 = t_2) /\ (t_4 = (t_2.[ a_1 < (t_2.[ a_8 ])%Z ])))

87

((t_1 = t_3) /\ (t_4 = (t_3.[ a_1 < (0)%Z ])))) >

88

(itep ((0 = i_2)%Z) (t_7 = (m_1.[ a_2 < x_3 ])) (t_7 = m_1)) >

89

(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) >

90

(forall (g_3 : S_g_mem_pack), (P_g_pack0) > ((IsS_g_mem_pack g_3)) >

91

((P_g_pack3 t_9 t_8 g_2 a_3)) > (P_trans_gA))) >

92

(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) >

93

(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) >

94

((P_g_pack1 t_9 t_4 g_3 a_3)) > ((P_g_pack3 t_9 t_8 g_2 a_3)) >

95

((P_trans_gC g_2 g_3 (t_4.[ a_1 ])%Z)))) >

96

(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) >

97

(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) >

98

((P_g_pack1 t_9 t_1 g_3 a_3)) > ((P_g_pack3 t_9 t_8 g_2 a_3)) >

99

((P_trans_gB g_2 g_3 x_1)))) >

100

(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) >

101

(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) >

102

((P_g_pack1 t_9 t_6 g_3 a_3)) > ((P_g_pack3 t_9 t_8 g_2 a_3)) >

103

((P_trans_gD i_2%Z i_5%Z g_2 g_3 x)))) >

104

(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) >

105

(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) >

106

((P_g_pack2 t_9 t_7 g_3 a_3)) > ((P_g_pack3 t_9 t_8 g_2 a_3)) >

107

((P_trans_gF i_2%Z i_5%Z g_2 g_3 (t_7.[ a_2 ])%Z x_2)))) >

108

(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) >

109

(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) >

110

((P_g_pack3 t_9 t_8 g_2 a_3)) > ((P_g_pack3 t_9 m g_3 a_3)) >

111

((P_trans_gG i_2%Z i_5%Z g_2 g_3 x_4)))) >

112

(forall (f : S_f_mem_pack), ((IsS_f_mem_pack f)) >

113

(forall (f_1 : S_f_mem_pack), ((IsS_f_mem_pack f_1)) >

114

((P_f_pack2 t_9 t_6 f a_5)) > ((P_f_pack2 t_9 m_1 f_1 a_5)) >

115

((P_trans_fF x f f_1 x_3 (m_1.[ a ])%Z)))) >

116

(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) >

117

(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) >

118

((P_g_pack3 t_9 t_8 g_2 a_3)) > ((P_g_pack2 t_9 m_1 g_3 a_3)) >

119

((P_trans_gE i_2%Z i_5%Z g_2 g_3 x_3)))) >

120

((P_trans_gG i_2%Z i_5%Z g_1 g x_4)).

121


122

Proof.

123

auto with zarith.

124

Qed.

125

