Commit 035ba52e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean some session files.

parent c07c22a6
...@@ -77,8 +77,6 @@ ...@@ -77,8 +77,6 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="Typing" proved="true">
</theory>
<theory name="TypingAndSemantics" proved="true"> <theory name="TypingAndSemantics" proved="true">
<goal name="type_inversion" proved="true"> <goal name="type_inversion" proved="true">
<transf name="induction_ty_lex" proved="true" > <transf name="induction_ty_lex" proved="true" >
......
...@@ -5,11 +5,9 @@ ...@@ -5,11 +5,9 @@
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/> <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="2" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/> <prover id="2" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/> <prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../formula.why" expanded="true"> <file name="../formula.why" proved="true">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="PropositionalCalculus" proved="true">
</theory> <goal name="Test1" proved="true">
<theory name="PropositionalCalculus" sum="7f2804c705a099e7f5ba415139b5ad50" expanded="true">
<goal name="Test1" expl="" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof> <proof prover="2"><result status="valid" time="0.19"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="46"/></proof> <proof prover="3"><result status="valid" time="0.05" steps="46"/></proof>
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
<prover id="1" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/> <prover id="1" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../imp_n.why" proved="true"> <file name="../imp_n.why" proved="true">
<theory name="Imp" proved="true" sum="3ef09115e35536df0c4a509815956237"> <theory name="Imp" proved="true">
<goal name="ident_eq_dec" proved="true"> <goal name="ident_eq_dec" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
......
...@@ -4,22 +4,20 @@ ...@@ -4,22 +4,20 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="4" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../add_list.mlw"> <file name="../add_list.mlw" proved="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="AddListRec" proved="true">
</theory> <goal name="VC sum" expl="VC for sum" proved="true">
<theory name="AddListRec" sum="191e311078f6223c9af44eece1bb2a47">
<goal name="VC sum" expl="VC for sum">
<proof prover="1"><result status="valid" time="0.02" steps="93"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="93"/></proof>
</goal> </goal>
<goal name="VC main" expl="VC for main"> <goal name="VC main" expl="VC for main" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof> <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="AddListImp" sum="25869898cb7ed98962558d9845b87089"> <theory name="AddListImp" proved="true">
<goal name="VC sum" expl="VC for sum"> <goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof> <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC main" expl="VC for main"> <goal name="VC main" expl="VC for main" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof> <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</theory> </theory>
......
...@@ -4,9 +4,7 @@ ...@@ -4,9 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../add_list_vc_sp.mlw" proved="true"> <file name="../add_list_vc_sp.mlw" proved="true">
<theory name="SumList" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="AddListRec" proved="true">
</theory>
<theory name="AddListRec" proved="true" sum="191e311078f6223c9af44eece1bb2a47">
<goal name="VC sum" expl="VC for sum" proved="true"> <goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal> </goal>
...@@ -14,7 +12,7 @@ ...@@ -14,7 +12,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="AddListImp" proved="true" sum="8e8899af132298f23d25fda654d93382"> <theory name="AddListImp" proved="true">
<goal name="VC sum" expl="VC for sum" proved="true"> <goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof> <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal> </goal>
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw" proved="true"> <file name="../all_distinct.mlw" proved="true">
<theory name="AllDistinct" proved="true" sum="ffbeb873677b943d48c32a50ca55f83a"> <theory name="AllDistinct" proved="true">
<goal name="VC all_distinct" expl="VC for all_distinct" proved="true"> <goal name="VC all_distinct" expl="VC for all_distinct" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="270"/></proof> <proof prover="0"><result status="valid" time="0.06" steps="270"/></proof>
</goal> </goal>
......
...@@ -4,14 +4,12 @@ ...@@ -4,14 +4,12 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../arm.mlw" proved="true"> <file name="../arm.mlw" proved="true">
<theory name="M" proved="true" sum="eade0a495f21f73e713558097e8dc30a"> <theory name="M" proved="true">
<goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true"> <goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="135"/></proof> <proof prover="0"><result status="valid" time="0.11" steps="135"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="ARM" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="InsertionSortExample" proved="true">
</theory>
<theory name="InsertionSortExample" proved="true" sum="b0bf33c0b21cb5adba7e72e6f7e3acfd">
<goal name="VC path_init_l2" expl="VC for path_init_l2" proved="true"> <goal name="VC path_init_l2" expl="VC for path_init_l2" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="22"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="22"/></proof>
</goal> </goal>
......
...@@ -4,12 +4,12 @@ ...@@ -4,12 +4,12 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../assigning_meanings_to_programs.mlw" proved="true"> <file name="../assigning_meanings_to_programs.mlw" proved="true">
<theory name="Sum" proved="true" sum="f8b6d21736575c9d96e33f6e4488d7f8"> <theory name="Sum" proved="true">
<goal name="VC sum" expl="VC for sum" proved="true"> <goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="39"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="Division" proved="true" sum="ce38e3995afc25e5981ed2086f16a1aa"> <theory name="Division" proved="true">
<goal name="VC division" expl="VC for division" proved="true"> <goal name="VC division" expl="VC for division" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal> </goal>
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../avl.mlw" proved="true"> <file name="../avl.mlw" proved="true">
<theory name="SelectionTypes" proved="true" sum="abd7a22ecdfcca31609e6de139c95c74"> <theory name="SelectionTypes" proved="true">
<goal name="VC option_to_seq" expl="VC for option_to_seq" proved="true"> <goal name="VC option_to_seq" expl="VC for option_to_seq" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
...@@ -18,7 +18,7 @@ ...@@ -18,7 +18,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="AVL" proved="true" sum="e4dba19b9b74ca489a76700d2e721781"> <theory name="AVL" proved="true">
<goal name="M.M.assoc" proved="true"> <goal name="M.M.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal> </goal>
......
...@@ -2,8 +2,6 @@ ...@@ -2,8 +2,6 @@
<!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="4"> <why3session shape_version="4">
<file name="../key_type.mlw"> <file name="../key_type.mlw" proved="true">
<theory name="KeyType" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file> </file>
</why3session> </why3session>
...@@ -5,11 +5,7 @@ ...@@ -5,11 +5,7 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../monoid.mlw" proved="true"> <file name="../monoid.mlw" proved="true">
<theory name="Monoid" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="MonoidSumDef" proved="true">
</theory>
<theory name="MonoidSum" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="MonoidSumDef" proved="true" sum="fe9dcfe1f224ce795e38a9e5cae32134">
<goal name="VC agg" expl="VC for agg" proved="true"> <goal name="VC agg" expl="VC for agg" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal> </goal>
...@@ -35,7 +31,5 @@ ...@@ -35,7 +31,5 @@
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="ComputableMonoid" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file> </file>
</why3session> </why3session>
...@@ -3,33 +3,31 @@ ...@@ -3,33 +3,31 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../preorder.mlw"> <file name="../preorder.mlw" proved="true">
<theory name="Full" sum="94f46ba82591cea76a95ccb2f4fdbacf"> <theory name="Full" proved="true">
<goal name="Eq.Refl"> <goal name="Eq.Refl" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal> </goal>
<goal name="Eq.Trans"> <goal name="Eq.Trans" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
</goal> </goal>
<goal name="Eq.Symm"> <goal name="Eq.Symm" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal> </goal>
<goal name="Lt.Trans"> <goal name="Lt.Trans" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
</goal> </goal>
<goal name="Lt.Asymm"> <goal name="Lt.Asymm" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="TotalFull" sum="a2011a71493dc687fc1408c6840d5529"> <theory name="TotalFull" proved="true">
<goal name="Lt.Total"> <goal name="Lt.Total" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal> </goal>
<goal name="lt_def2"> <goal name="lt_def2" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="Computable" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file> </file>
</why3session> </why3session>
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
<prover id="2" name="Eprover" version="1.8-001" timelimit="20" steplimit="0" memlimit="1000"/> <prover id="2" name="Eprover" version="1.8-001" timelimit="20" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../priority_queue.mlw" proved="true"> <file name="../priority_queue.mlw" proved="true">
<theory name="PQueue" proved="true" sum="2dc2e3d764d5c161d843c474061d1d51"> <theory name="PQueue" proved="true">
<goal name="VC balancing" expl="VC for balancing" proved="true"> <goal name="VC balancing" expl="VC for balancing" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal> </goal>
......
...@@ -3,157 +3,157 @@ ...@@ -3,157 +3,157 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../ral.mlw"> <file name="../ral.mlw" proved="true">
<theory name="RAL" sum="71a1e47f9906cbd919ad5a85c23b1173"> <theory name="RAL" proved="true">
<goal name="VC balancing" expl="VC for balancing"> <goal name="VC balancing" expl="VC for balancing" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal> </goal>
<goal name="M.assoc" expl=""> <goal name="M.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="M.neutral" expl=""> <goal name="M.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="M.M.assoc" expl=""> <goal name="M.M.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="M.M.neutral" expl=""> <goal name="M.M.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="M.VC zero" expl="VC for zero"> <goal name="M.VC zero" expl="VC for zero" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="M.VC op" expl="VC for op"> <goal name="M.VC op" expl="VC for op" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="D.VC measure" expl="VC for measure"> <goal name="D.VC measure" expl="VC for measure" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="VC agg_measure_is_length" expl="VC for agg_measure_is_length"> <goal name="VC agg_measure_is_length" expl="VC for agg_measure_is_length" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="50"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="50"/></proof>
</goal> </goal>
<goal name="VC selected_part" expl="VC for selected_part"> <goal name="VC selected_part" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.26" steps="762"/></proof> <proof prover="0"><result status="valid" time="0.26" steps="762"/></proof>
</goal> </goal>
<goal name="Sel.M.assoc" expl=""> <goal name="Sel.M.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="Sel.M.neutral" expl=""> <goal name="Sel.M.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="Sel.M.VC zero" expl="VC for zero"> <goal name="Sel.M.VC zero" expl="VC for zero" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="Sel.M.VC op" expl="VC for op"> <goal name="Sel.M.VC op" expl="VC for op" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="Sel.M.agg_empty" expl=""> <goal name="Sel.M.agg_empty" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal> </goal>
<goal name="Sel.M.agg_sing" expl=""> <goal name="Sel.M.agg_sing" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal> </goal>
<goal name="Sel.M.agg_cat" expl=""> <goal name="Sel.M.agg_cat" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal> </goal>
<goal name="Sel.D.VC measure" expl="VC for measure"> <goal name="Sel.D.VC measure" expl="VC for measure" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="Sel.VC balancing" expl="VC for balancing"> <goal name="Sel.VC balancing" expl="VC for balancing" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="Sel.selection_empty" expl=""> <goal name="Sel.selection_empty" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
</goal> </goal>
<goal name="Sel.VC selected_part" expl="VC for selected_part"> <goal name="Sel.VC selected_part" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.28" steps="655"/></proof> <proof prover="0"><result status="valid" time="0.28" steps="655"/></proof>
</goal> </goal>
<goal name="VC empty" expl="VC for empty"> <goal name="VC empty" expl="VC for empty" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal> </goal>
<goal name="VC singleton" expl="VC for singleton"> <goal name="VC singleton" expl="VC for singleton" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal> </goal>
<goal name="VC is_empty" expl="VC for is_empty"> <goal name="VC is_empty" expl="VC for is_empty" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="VC decompose_front" expl="VC for decompose_front"> <goal name="VC decompose_front" expl="VC for decompose_front" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="59"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="59"/></proof>
</goal> </goal>
<goal name="VC decompose_back" expl="VC for decompose_back"> <goal name="VC decompose_back" expl="VC for decompose_back" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="59"/></proof> <proof prover="0"><result status="valid" time="0.04" steps="59"/></proof>
</goal> </goal>
<goal name="VC front" expl="VC for front"> <goal name="VC front" expl="VC for front" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="VC back" expl="VC for back"> <goal name="VC back" expl="VC for back" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="4"/></proof>
</goal> </goal>
<goal name="VC cons" expl="VC for cons"> <goal name="VC cons" expl="VC for cons" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal> </goal>
<goal name="VC snoc" expl="VC for snoc"> <goal name="VC snoc" expl="VC for snoc" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal> </goal>
<goal name="VC concat" expl="VC for concat"> <goal name="VC concat" expl="VC for concat" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="4"/></proof>
</goal> </goal>
<goal name="VC length" expl="VC for length"> <goal name="VC length" expl="VC for length" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal> </goal>
<goal name="VC set" expl="VC for set"> <goal name="VC set" expl="VC for set" proved="true">
<proof prover="0"><result status="valid" time="0.20" steps="488"/></proof> <proof prover="0"><result status="valid" time="0.20" steps="488"/></proof>
</goal> </goal>
<goal name="VC get" expl="VC for get"> <goal name="VC get" expl="VC for get" proved="true">
<proof prover="0"><result status="valid" time="0.07" steps="106"/></proof> <proof prover="0"><result status="valid" time="0.07" steps="106"/></proof>
</goal> </goal>
<goal name="VC insert" expl="VC for insert"> <goal name="VC insert" expl="VC for insert" proved="true">
<proof prover="0"><result status="valid" time="0.47" steps="498"/></proof> <proof prover="0"><result status="valid" time="0.47" steps="498"/></proof>
</goal> </goal>
<goal name="VC remove" expl="VC for remove"> <goal name="VC remove" expl="VC for remove" proved="true">
<proof prover="0"><result status="valid" time="0.38" steps="360"/></proof> <proof prover="0"><result status="valid" time="0.38" steps="360"/></proof>
</goal> </goal>
<goal name="VC cut" expl="VC for cut"> <goal name="VC cut" expl="VC for cut" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="177"/></proof> <proof prover="0"><result status="valid" time="0.09" steps="177"/></proof>
</goal> </goal>
<goal name="VC split" expl="VC for split"> <goal name="VC split" expl="VC for split" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="353"/></proof> <proof prover="0"><result status="valid" time="0.15" steps="353"/></proof>
</goal> </goal>
<goal name="VC harness" expl="VC for harness"> <goal name="VC harness" expl="VC for harness" proved="true">
<transf name="split_goal_wp"> <transf name="split_goal_wp" proved="true" >
<goal name="VC harness.1" expl="precondition"> <goal name="VC harness.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="6"/></proof>
</goal> </goal>
<goal name="VC harness.2" expl="precondition"> <goal name="VC harness.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="9"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="9"/></proof>
</goal> </goal>
<goal name="VC harness.3" expl="precondition"> <goal name="VC harness.2" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="VC harness.4" expl="precondition"> <goal name="VC harness.3" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="15"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="15"/></proof>
</goal> </goal>
<goal name="VC harness.5" expl="check"> <goal name="VC harness.4" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="143"/></proof> <proof prover="0"><result status="valid" time="0.06" steps="143"/></proof>
</goal> </goal>
<goal name="VC harness.6" expl="check"> <goal name="VC harness.5" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.07" steps="143"/></proof> <proof prover="0"><result status="valid" time="0.07" steps="143"/></proof>
</goal> </goal>
<goal name="VC harness.7" expl="precondition"> <goal name="VC harness.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="18"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="18"/></proof>
</goal> </goal>
<goal name="VC harness.8" expl="precondition"> <goal name="VC harness.7" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
</goal>