Skip to content

GitLab

Commit fd6e7889 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

example 2wp_gen: update sessions

parent 953a8309
Expand all Hide whitespace changes
Inline Side-by-side
examples/in_progress/2wp_gen/Makefile
View file @ fd6e7889
......@@ -4,4 +4,4 @@ MLW=base choice ho_set ho_rel fn pfn order transfinite game game_no_strat game_s
replay:
@exe() { echo "$$0 $$@"; "$$@"; };\
for f in $(MLW); do exe $(REPLAY) $$f.mlw; done
for f in $(MLW); do exe $(REPLAY) $$f; done
examples/in_progress/2wp_gen/base/why3session.xml
View file @ fd6e7889
......@@ -3,226 +3,226 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../base.mlw">
<theory name="Fun" sum="d41d8cd98f00b204e9800998ecf8427e">
<file name="../base.mlw" proved="true">
<theory name="Fun" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="FunExt" sum="8d44c32e8c71e269a74dd41007e7609b">
<goal name="VC extensional" expl="VC for extensional">
<theory name="FunExt" proved="true" sum="8d44c32e8c71e269a74dd41007e7609b">
<goal name="VC extensional" expl="VC for extensional" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</theory>
<theory name="FunCategory" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="FunCategory" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="FunProofs" sum="b9fbc35866125483c158259bb13c9cc4">
<goal name="ext">
<transf name="split_goal_wp">
<goal name="ext.1" expl="1.">
<transf name="introduce_premises">
<goal name="ext.1.1" expl="1.">
<transf name="inline_goal">
<goal name="ext.1.1.1" expl="1.">
<theory name="FunProofs" proved="true" sum="f70392d9b203295af7b3b37cb931e41e">
<goal name="ext" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="ext.0" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="ext.0.0" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="ext.0.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="ext.2" expl="2.">
<goal name="ext.1" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</transf>
</goal>
<goal name="assoc">
<goal name="assoc" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="neutral">
<goal name="neutral" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="44"/></proof>
</goal>
<goal name="FunExt.extensionality">
<goal name="FunExt.extensionality" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="FunCategory.assoc">
<goal name="FunCategory.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="FunCategory.neutral">
<goal name="FunCategory.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
</theory>
<theory name="Set" sum="3414482dcfbe683bc2c77737916e8e68">
<goal name="sext_is_ext">
<theory name="Set" proved="true" sum="3414482dcfbe683bc2c77737916e8e68">
<goal name="sext_is_ext" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
<theory name="SetBigOps" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="SetBigOps" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Rel" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Rel" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RelExt" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="RelExt" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RelCategory" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="RelCategory" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RelProduct" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="RelProduct" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RelSet" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="RelSet" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RelProofs" sum="47eaf58414de8e8f8ba045fd8039fea4">
<goal name="extensionality">
<theory name="RelProofs" proved="true" sum="4388396c90982f679b596fef0441fced">
<goal name="extensionality" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
<transf name="split_goal_wp">
<goal name="extensionality.1" expl="1.">
<transf name="split_goal_wp" proved="true" >
<goal name="extensionality.0" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="extensionality.2" expl="2.">
<goal name="extensionality.1" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="extensionality.3" expl="3.">
<goal name="extensionality.2" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</transf>
</goal>
<goal name="assoc">
<transf name="compute_specified">
<goal name="assoc.1" expl="1.">
<transf name="introduce_premises">
<goal name="assoc.1.1" expl="1.">
<goal name="assoc" proved="true">
<transf name="compute_specified" proved="true" >
<goal name="assoc.0" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="assoc.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="reverse_antimorphism">
<goal name="reverse_antimorphism" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="reverse_antimorphism_id">
<goal name="reverse_antimorphism_id" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="reverse_involution">
<goal name="reverse_involution" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="neutral">
<transf name="compute_specified">
<goal name="neutral.1" expl="1.">
<transf name="introduce_premises">
<goal name="neutral.1.1" expl="1.">
<goal name="neutral" proved="true">
<transf name="compute_specified" proved="true" >
<goal name="neutral.0" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="neutral.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="RelExt.extensionality">
<goal name="RelExt.extensionality" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="RelCategory.assoc">
<goal name="RelCategory.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="RelCategory.reverse_antimorphism">
<goal name="RelCategory.reverse_antimorphism" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="RelCategory.reverse_antimorphism_id">
<goal name="RelCategory.reverse_antimorphism_id" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="RelCategory.reverse_involution">
<goal name="RelCategory.reverse_involution" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="RelCategory.neutral">
<goal name="RelCategory.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
</theory>
<theory name="SubsetOrder" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="SubsetOrder" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SetProofs" sum="c22368c2c3a04e7c41543119617de769">
<goal name="anti_subset">
<theory name="SetProofs" proved="true" sum="c22368c2c3a04e7c41543119617de769">
<goal name="anti_subset" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="SubsetOrder.subset_order">
<goal name="SubsetOrder.subset_order" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="58"/></proof>
</goal>
</theory>
<theory name="Image" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Image" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="PartialFun" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="PartialFun" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="PartialFunInstance" sum="733ea4701f40b9ee22b7d22c463025a0">
<goal name="VC dummy" expl="VC for dummy">
<theory name="PartialFunInstance" proved="true" sum="fd48f8137216614f8c8c13b6d89d7e4f">
<goal name="VC dummy" expl="VC for dummy" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC of_fun" expl="VC for of_fun">
<goal name="VC of_fun" expl="VC for of_fun" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
<goal name="VC restrict" expl="VC for restrict">
<goal name="VC restrict" expl="VC for restrict" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC extends" expl="VC for extends">
<goal name="VC extends" expl="VC for extends" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.02" steps="92"/></proof>
</goal>
<goal name="VC psing" expl="VC for psing">
<goal name="VC psing" expl="VC for psing" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC padd" expl="VC for padd">
<goal name="VC padd" expl="VC for padd" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC premove" expl="VC for premove">
<goal name="VC premove" expl="VC for premove" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="extensional">
<transf name="split_goal_wp">
<goal name="extensional.1" expl="1.">
<goal name="extensional" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="extensional.0" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="extensional.2" expl="2.">
<goal name="extensional.1" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="extensional.3" expl="3.">
<goal name="extensional.2" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="extensional.4" expl="4.">
<goal name="extensional.3" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.07" steps="91"/></proof>
</goal>
<goal name="extensional.5" expl="5.">
<goal name="extensional.4" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="extensional.6" expl="6.">
<goal name="extensional.5" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</transf>
</goal>
<goal name="PartialFun.VC of_fun" expl="VC for of_fun">
<goal name="PartialFun.VC of_fun" expl="VC for of_fun" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="PartialFun.VC restrict" expl="VC for restrict">
<goal name="PartialFun.VC restrict" expl="VC for restrict" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="PartialFun.VC extends" expl="VC for extends">
<goal name="PartialFun.VC extends" expl="VC for extends" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.03" steps="126"/></proof>
</goal>
<goal name="PartialFun.VC join" expl="VC for join">
<goal name="PartialFun.VC join" expl="VC for join" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.03" steps="179"/></proof>
</goal>
<goal name="PartialFun.VC psing" expl="VC for psing">
<goal name="PartialFun.VC psing" expl="VC for psing" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.04" steps="179"/></proof>
</goal>
<goal name="PartialFun.VC padd" expl="VC for padd">
<proof prover="0" timelimit="1"><result status="valid" time="0.24" steps="1221"/></proof>
<goal name="PartialFun.VC padd" expl="VC for padd" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.24" steps="1269"/></proof>
</goal>
<goal name="PartialFun.VC premove" expl="VC for premove">
<goal name="PartialFun.VC premove" expl="VC for premove" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="47"/></proof>
</goal>
<goal name="PartialFun.extensional">
<goal name="PartialFun.extensional" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
<theory name="SubFunOrder" sum="43c3b6d10e75b8bfef291d48bac961ef">
<goal name="subfun_order">
<transf name="split_goal_wp">
<goal name="subfun_order.1" expl="1.">
<theory name="SubFunOrder" proved="true" sum="b5704a9dd6a083e2c68baaea448357f6">
<goal name="subfun_order" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="subfun_order.0" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="subfun_order.2" expl="2.">
<goal name="subfun_order.1" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="subfun_order.3" expl="3.">
<goal name="subfun_order.2" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.02" steps="137"/></proof>
</goal>
</transf>
......
examples/in_progress/2wp_gen/choice/why3session.xml
View file @ fd6e7889
......@@ -3,12 +3,12 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../choice.mlw">
<theory name="Choice" sum="ab969c547d54aa154c27370d65057999">
<goal name="VC choose" expl="VC for choose">
<file name="../choice.mlw" proved="true">
<theory name="Choice" proved="true" sum="ab969c547d54aa154c27370d65057999">
<goal name="VC choose" expl="VC for choose" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC choose_if" expl="VC for choose_if">
<goal name="VC choose_if" expl="VC for choose_if" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
</theory>
......
examples/in_progress/2wp_gen/fn/why3session.xml
View file @ fd6e7889
......@@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../fn.mlw" expanded="true">
<theory name="Fun" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<file name="../fn.mlw" proved="true">
<theory name="Fun" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Category" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Category" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Image" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Image" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
examples/in_progress/2wp_gen/ho_rel/why3session.xml
View file @ fd6e7889
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../ho_rel.mlw" expanded="true">
<theory name="Rel" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<file name="../ho_rel.mlw" proved="true">
<theory name="Rel" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Category" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Category" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Prod" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Prod" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RelSet" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="RelSet" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
examples/in_progress/2wp_gen/ho_set/why3session.xml
View file @ fd6e7889
......@@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../ho_set.mlw" expanded="true">
<theory name="Set" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<file name="../ho_set.mlw" proved="true">
<theory name="Set" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SubsetOrder" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="SubsetOrder" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SetBigOps" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="SetBigOps" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
examples/in_progress/2wp_gen/pfn/why3session.xml
View file @ fd6e7889
......@@ -2,10 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../pfn.mlw" expanded="true">
<theory name="Pfun" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<file name="../pfn.mlw" proved="true">
<theory name="Pfun" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SubFunOrder" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="SubFunOrder" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
examples/in_progress/2wp_gen/subgame/why3session.xml
View file @ fd6e7889
......@@ -4,24 +4,24 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../subgame.mlw">
<theory name="SubGameDef" sum="d41d8cd98f00b204e9800998ecf8427e">
<file name="../subgame.mlw" proved="true">
<theory name="SubGameDef" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SubGame" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="SubGame" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SubGameProof" sum="a87262aa57544f69f68ecf7ea4029bf7">
<goal name="L0" expl="">
<transf name="split_goal_wp">
<goal name="L0.1" expl="">
<transf name="introduce_premises">
<goal name="L0.1.1" expl="">
<transf name="inline_goal">
<goal name="L0.1.1.1" expl="">
<transf name="split_goal_wp">
<goal name="L0.1.1.1.1" expl="">
<theory name="SubGameProof" proved="true" sum="63c689d8c610e2ff0735f8a280be6ee9">
<goal name="L0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="L0.0" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="L0.0.0" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="L0.0.0.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="L0.0.0.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="L0.1.1.1.2" expl="">
<goal name="L0.0.0.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
......@@ -30,26 +30,26 @@
</goal>
</transf>
</goal>
<goal name="L0.2" expl="">
<goal name="L0.1" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="L1" expl="">
<transf name="split_goal_wp">
<goal name="L1.1" expl="">
<goal name="L1" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="L1.0" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="L1.2" expl="">
<transf name="introduce_premises">
<goal name="L1.2.1" expl="">
<transf name="inline_goal">
<goal name="L1.2.1.1" expl="">
<transf name="split_goal_wp">
<goal name="L1.2.1.1.1" expl="">
<proof prover="1"><result status="valid" time="0.29"/></proof>
<goal name="L1.1" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="L1.1.0" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="L1.1.0.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="L1.1.0.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="L1.2.1.1.2" expl="">
<goal name="L1.1.0.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
......@@ -58,37 +58,37 @@
</goal>
</transf>
</goal>
<goal name="L1.3" expl="">
<goal name="L1.2" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="113"/></proof>
</goal>
<goal name="L1.4" expl="">
<goal name="L1.3" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="9"/></proof>
</goal>
<goal name="L1.5" expl="">
<goal name="L1.4" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="40"/></proof>
</goal>
<goal name="L1.6" expl="">
<goal name="L1.5" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="7"/></proof>
</goal>
</transf>
</goal>
<goal name="SubGame.trivial_subgame_subgame" expl="">
<goal name="SubGame.trivial_subgame_subgame" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="SubGame.subgame_other" expl="">
<transf name="split_goal_wp">
<goal name="subgame_other.1" expl="">
<goal name="SubGame.subgame_other" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="subgame_other.0" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="3"/></proof>
</goal>
<goal name="subgame_other.2" expl="">
<proof prover="1" timelimit="20"><result status="valid" time="3.33"/></proof>
<goal name="subgame_other.1" proved="true">
<proof prover="1" timelimit="20"><result status="valid" time="2.35"/></proof>
</goal>
<goal name="subgame_other.3" expl="">
<goal name="subgame_other.2" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="15"/></proof>
</goal>
</transf>
</goal>
<goal name="SubGame.subgame_preorder" expl="">
<goal name="SubGame.subgame_preorder" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="129"/></proof>
</goal>
</theory>
......
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