Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/misc/durationThm_2.lus
regression_tests/lustre_files/success/kind_fmcad08/misc/durationThm_2.lus  

18  18 
 (p k> q and r k> t) => (p and r) k> (q and t) 
19  19  
20  20 
 Not provable in luke* 
21 
@ ensures OK; 

22  21 
node top (k0: int; p, q, r, t : bool) returns (OK: bool); 
22 
@ contract guarantees OK; 

23  23 
var k: int; 
24  24 
env : bool; 
25  25 
let 
Also available in: Unified diff