lustrec/optim/clocks7/wp1.script @ 6a93d814
| 1 |
(* 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 |
|
| 46 |
|