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