1

(*  *)

2

(*  Instance of 'Precondition (file oversampling0_4.c, line 149) in 'f_step'' in 'g_step' at call 'f_step' (file oversampling0_4.c, line 357)

3

 *)

4

(*  *)

5

Require Import ZArith.

6

Require Import Reals.

7

Require Import BuiltIn.

8

Require Import bool.Bool.

9

Require Import int.Int.

10

Require Import int.Abs.

11

Require Import int.ComputerDivision.

12

Require Import real.Real.

13

Require Import real.RealInfix.

14

Require Import real.FromInt.

15

Require Import map.Map.

16

Require Import Qedlib.

17

Require Import Qed.

18

Require Import Memory.

19

Require Import Cint.

20


21

Require Import Compound.

22

Require Import Axiomatic.

23

Require Import Globals.

24

Require Import S_g_mem_pack.

25


26

Goal

27

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

28

forall (i_1 i : Z),

29

forall (t : array Z),

30

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

31

forall (t_8 : farray addr addr),

32

forall (a_2 a_1 : addr),

33

let a_3 := t_8.[ (shiftfield_F_g_mem_ni_1 a_2) ] in

34

let a_4 := t_8.[ (shiftfield_F_g_mem_ni_0 a_2) ] in

35

let a_5 := t_8.[ (shiftfield_F_f_mem_ni_2 a_4) ] in

36

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

37

let a_6 := (shiftfield_F__arrow_reg__first

38

((shiftfield_F__arrow_mem__reg a_3))) in

39

let x_1 := (t_7.[ a_6 ])%Z in

40

((framed t_8)) >

41

((linked t)) >

42

((is_uint32 i%Z)) >

43

(a_1 <> a_3) >

44

((valid_rw t a_1 1%Z)) >

45

((P_valid_g t t_8 a_2)) >

46

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

47

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

48

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

49

(a_1 <> a_5) >

50

(a_3 <> a_5) >

51

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

52

((separated a_2 3%Z a_4 2%Z)) >

53

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

54

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

55

((is_sint32 x)) >

56

((is_uint32 x_1)) >

57

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

58

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

59

(itep ((0 = x_1)%Z) (t_1 = t_7) (t_1 = (t_7.[ a_6 < (0)%Z ]))) >

60

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

61

((t_4 = t_5) /\ (t_6 = (t_5.[ a < (i_1)%Z ])))) >

62

(itep ((0 = x_1)%Z)

63

((t_1 = t_2) /\

64

(t_4 =

65

(t_2.[ a < (t_2.[ (shiftfield_F_g_reg___g_2

66

((shiftfield_F_g_mem__reg a_2))) ])%Z ])))

67

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

68

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

69

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

70

((P_g_pack3 t_8 t_7 g a_2)) > (P_trans_gA))) >

71

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

72

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

73

((P_g_pack1 t_8 t_4 g_1 a_2)) > ((P_g_pack3 t_8 t_7 g a_2)) >

74

((P_trans_gC g g_1 (t_4.[ a ])%Z)))) >

75

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

76

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

77

((P_g_pack1 t_8 t_1 g_1 a_2)) > ((P_g_pack3 t_8 t_7 g a_2)) >

78

((P_trans_gB g g_1 x_1)))) >

79

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

80

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

81

((P_g_pack1 t_8 t_6 g_1 a_2)) > ((P_g_pack3 t_8 t_7 g a_2)) >

82

((P_trans_gD i%Z i_1%Z g g_1 x)))) >

83

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

84

t_8 a_4)).

85


86

Proof.

87

auto with zarith.

88

Qed.

89

