## lustrec / optim / oversampling / out / typed / g_reset_call_f_reset_pre_Coq.v @ 6a93d814

History | View | Annotate | Download (1.26 KB)

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

2 |
(* --- Instance of 'Pre-condition (file oversampling0_4.c, line 138) in 'f_reset'' in 'g_reset' at call 'f_reset' (file oversampling0_4.c, line 321) |

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 | |

20 |
Require Import Axiomatic. |

21 |
Require Import Compound. |

22 | |

23 |
Goal |

24 |
forall (t : array Z), |

25 |
forall (t_1 : farray addr addr), |

26 |
forall (a : addr), |

27 |
let a_1 := t_1.[ (shiftfield_F_g_mem_ni_1 a) ] in |

28 |
let a_2 := t_1.[ (shiftfield_F_g_mem_ni_0 a) ] in |

29 |
let a_3 := t_1.[ (shiftfield_F_f_mem_ni_2 a_2) ] in |

30 |
((framed t_1)) -> |

31 |
((linked t)) -> |

32 |
((P_valid_g t t_1 a)) -> |

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

34 |
(a_1 <> a_3) -> |

35 |
((separated a 3%Z a_2 2%Z)) -> |

36 |
((separated a 3%Z a_1 1%Z)) -> |

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

38 |
((separated a 3%Z a_3 1%Z)) -> |

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

40 |
((P_valid_f t t_1 a_2)). |

41 | |

42 |
Proof. |

43 |
auto with zarith. |

44 |
Qed. |

45 |