Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / clocks7 / wp4.script @ 6a93d814

History | View | Annotate | Download (173 Bytes)

1
(* Generated by Frama-C WP *)
2

    
3
Goal typed_toto_step_assert_21.
4
Hint property,toto_step.
5
Proof.
6
Require Import Why3.
7
intuition.
8
repeat (split || exists 0); why3 "Z3".
9
Qed.
10

    
11