lustrec/optim/clocks7/wp1.script @ 6a93d814
| 1 | 6a93d814 | xthirioux | (* Generated by Frama-C WP *) |
|---|---|---|---|
| 2 | |||
| 3 | Goal typed_toto_step_assert_6. |
||
| 4 | Hint property,toto_step. |
||
| 5 | Proof. |
||
| 6 | intros. |
||
| 7 | unfold P_trans_totoH. |
||
| 8 | intuition. |
||
| 9 | unfold P_trans_totoG. |
||
| 10 | exists Z0. |
||
| 11 | exists Z0. |
||
| 12 | exists Z0. |
||
| 13 | intuition. |
||
| 14 | unfold is_sint32. |
||
| 15 | auto with zarith. |
||
| 16 | unfold is_sint32. |
||
| 17 | auto with zarith. |
||
| 18 | unfold is_uint32. |
||
| 19 | auto with zarith. |
||
| 20 | unfold P_trans_totoF. |
||
| 21 | unfold P_trans_totoE. |
||
| 22 | unfold P_trans_totoD. |
||
| 23 | intuition. |
||
| 24 | exists Z0. |
||
| 25 | unfold is_uint32. |
||
| 26 | intuition. |
||
| 27 | |||
| 28 | unfold P_trans_totoC. |
||
| 29 | unfold P_trans_totoB. |
||
| 30 | unfold P_clock_toto_2. |
||
| 31 | intuition. |
||
| 32 | discriminate. |
||
| 33 | unfold P_clock_c in H7. |
||
| 34 | discriminate. |
||
| 35 | unfold P_clock_b2 in H7. |
||
| 36 | intuition. |
||
| 37 | unfold P_clock_c in H10. |
||
| 38 | discriminate. |
||
| 39 | unfold P_clock_b1 in H7. |
||
| 40 | intuition. |
||
| 41 | unfold P_clock_z in H7. |
||
| 42 | unfold P_clock_c in H7. |
||
| 43 | discriminate. |
||
| 44 | Qed. |
||
| 45 |