Commit efec0bde authored by MARCHE Claude's avatar MARCHE Claude

updated proofs

parent 25e8a869
......@@ -756,7 +756,6 @@ unfold valid_fmla ; simpl.
intros sigma' pi' (H5 & H6).
apply H1; auto; clear H1.
generalize (monotonicity s1 _ _ H).
why3 "alt-ergo" timelimit 5.
clear H; intro H.
unfold valid_fmla in H.
simpl in H.
......
......@@ -770,7 +770,7 @@ Axiom abstract_effects_writes : forall (sigma:(map mident value)) (pi:(list
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
Ltac ae := why3 "alt-ergo" timelimit 5.
(* Why3 goal *)
Theorem monotonicity : forall (s:expr),
......@@ -818,7 +818,7 @@ admit.
rewrite get_stack_neq; auto.
rewrite get_stack_eq; auto.
apply H.
ae.
(* todo *)
Qed.
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment