Commit 317e511a authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fill: one goal now using the induction tactic

parent ba364cfc
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
<file <file
name="../fill.mlw" name="../fill.mlw"
verified="true" verified="true"
expanded="false"> expanded="true">
<theory <theory
name="Fill" name="Fill"
locfile="../fill.mlw" locfile="../fill.mlw"
...@@ -36,6 +36,29 @@ ...@@ -36,6 +36,29 @@
archived="false"> archived="false">
<result status="valid" time="0.46"/> <result status="valid" time="0.46"/>
</proof> </proof>
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
<goal
name="size_nonneg.1"
locfile="../fill.mlw"
loclnum="23" loccnumb="8" loccnume="19"
expl="1."
sum="019465be7b57b5a20e93609d8ace4fed"
proved="true"
expanded="false"
shape="CV0aNullainfix &gt;=asizeV0c0aNodeVVVainfix &gt;=asizeV0c0Iainfix &gt;=asizeV1c0Iainfix &gt;=asizeV3c0F">
<proof
prover="0"
timelimit="8"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal> </goal>
<goal <goal
name="WP_parameter fill" name="WP_parameter fill"
......
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