Commit a5ca2974 authored by Quentin Garchery's avatar Quentin Garchery

update test and big_big test for blast

parent 85faa980
...@@ -53,7 +53,8 @@ goal blast_and : (a /\ b) /\ (a /\ a /\ a /\ b) ...@@ -53,7 +53,8 @@ goal blast_and : (a /\ b) /\ (a /\ a /\ a /\ b)
goal blast_and_hole : (b /\ a) /\ ( (a /\ a) /\ c) goal blast_and_hole : (b /\ a) /\ ( (a /\ a) /\ c)
goal blast_or : (a \/ c) /\ (d \/ b) goal blast_or : (a \/ c) /\ (d \/ b)
goal blast_or_hole : a /\ (c \/ d) goal blast_or_hole : a /\ (c \/ d)
goal blast_big : ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ goal blast_big : (a /\ (d \/ c) ) \/ (((a /\ b) /\ ((b /\ (d \/ e \/ a)) \/d)) \/ (a /\ c))
goal blast_big_big : ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\
(((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a)))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a)))) /\
((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\
(((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a)))) (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))))
...@@ -69,3 +70,4 @@ goal drinker : exists x : bool. p x -> (forall y. p y) ...@@ -69,3 +70,4 @@ goal drinker : exists x : bool. p x -> (forall y. p y)
goal contra_hyps : (c /\ (not c \/ d) /\ (not d \/ e) /\ (not e \/ f) /\ not f) -> false goal contra_hyps : (c /\ (not c \/ d) /\ (not d \/ e) /\ (not e \/ f) /\ not f) -> false
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="8"> <why3session shape_version="8">
<file> <file format="whyml">
<path name=".."/><path name="test.mlw"/> <path name=".."/><path name="test.mlw"/>
<theory name="Top"> <theory name="Top">
<goal name="assumption" proved="true"> <goal name="assumption" proved="true">
...@@ -747,6 +747,12 @@ ...@@ -747,6 +747,12 @@
<transf name="blast_dcert" proved="true" > <transf name="blast_dcert" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="blast_big_big" proved="true">
<transf name="blast_ccert" proved="true" >
</transf>
<transf name="blast_dcert" proved="true" >
</transf>
</goal>
<goal name="rew_goal" proved="true"> <goal name="rew_goal" proved="true">
<transf name="intro_ccert" proved="true" > <transf name="intro_ccert" proved="true" >
<goal name="rew_goal.0" proved="true"> <goal name="rew_goal.0" proved="true">
......
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