Revision 4174a469
Added by Guillaume Davy over 8 years ago
tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.coq  

1 
Goal typed_AltitudeControl_step_post. 

2 
Proof. 

3 
intros. 

4 
eapply Q_inv_inv_AltitudeControl. 

5 
Focus 4. 

6 
eassumption. 

7 
eassumption. 

8 
eassumption. 

9 
eassumption. 

10 
Qed. 

1 
(* Generated by FramaC WP *) 

11  2  
12 
Goal typed_ref_AltitudeControl_step_post.


3 
Goal typed_AltitudeControl_step_post. 

13  4 
Proof. 
14  5 
intros. 
15  6 
eapply Q_inv_inv_AltitudeControl. 
...  ...  
206  197 
eassumption. 
207  198 
Qed. 
208  199  
200 
Goal typed_ref_AltitudeControl_step_post. 

201 
Proof. 

202 
intros. 

203 
eapply Q_inv_inv_AltitudeControl. 

204 
Focus 4. 

205 
eassumption. 

206 
eassumption. 

207 
eassumption. 

208 
eassumption. 

209 
Qed. 

210  
211 
Goal typed_ref_AltitudeControl_step_stmt_post_20. 

212 
Hint AltitudeControl_step,default,property. 

213 
Proof. 

214 
Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;try why3 "CVC4" timelimit 10. 

215 
why3 "altergo" timelimit 20. 

216 
Qed. 

217  
218 
Goal typed_ref_lemma_missing. 

219 
Hint missing,property. 

220 
Proof. 

221 
admit. 

222 
Qed. 

223  
224 
Also available in: Unified diff
Correct some problem related to new bool encoding