Commit 456880e9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update sessions for Prover example

parent 609cfacf
......@@ -2,15 +2,15 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Firstorder_formula_list_spec.mlw" expanded="true">
<theory name="Spec" sum="95246be42438773cb85bab6d78509d88">
<theory name="Spec" sum="789ed05fcbb07ac7a6877ebd8dfb88e1">
<goal name="WP_parameter size_positive_lemma_fo_formula_list" expl="VC for size_positive_lemma_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.10" steps="63"/></proof>
</goal>
<goal name="WP_parameter renaming_composition_lemma_fo_formula_list" expl="VC for renaming_composition_lemma_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.07" steps="70"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.07" steps="71"/></proof>
</goal>
<goal name="WP_parameter renaming_identity_lemma_fo_formula_list" expl="VC for renaming_identity_lemma_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.07" steps="52"/></proof>
......@@ -23,13 +23,13 @@
</goal>
<goal name="WP_parameter subst_composition_lemma_fo_formula_list" expl="VC for subst_composition_lemma_fo_formula_list">
<transf name="split_goal_wp">
<goal name="WP_parameter subst_composition_lemma_fo_formula_list.1" expl="1. postcondition">
<goal name="WP_parameter subst_composition_lemma_fo_formula_list.1" expl="postcondition">
<proof prover="2"><result status="valid" time="0.06" steps="7"/></proof>
</goal>
<goal name="WP_parameter subst_composition_lemma_fo_formula_list.2" expl="2. variant decrease">
<goal name="WP_parameter subst_composition_lemma_fo_formula_list.2" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.06" steps="10"/></proof>
</goal>
<goal name="WP_parameter subst_composition_lemma_fo_formula_list.3" expl="3. postcondition">
<goal name="WP_parameter subst_composition_lemma_fo_formula_list.3" expl="postcondition">
<proof prover="2"><result status="valid" time="0.07" steps="43"/></proof>
</goal>
</transf>
......@@ -41,13 +41,13 @@
<proof prover="2" timelimit="1"><result status="valid" time="0.07" steps="52"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_constructive_inversion_symbol_fo_formula_list" expl="VC for rename_free_var_constructive_inversion_symbol_fo_formula_list">
<proof prover="2"><result status="valid" time="0.12" steps="135"/></proof>
<proof prover="2"><result status="valid" time="0.12" steps="134"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_inversion_symbol_fo_formula_list" expl="VC for rename_free_var_inversion_symbol_fo_formula_list">
<proof prover="2"><result status="valid" time="0.08" steps="9"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_constructive_inversion_fo_term_fo_formula_list" expl="VC for rename_free_var_constructive_inversion_fo_term_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.09" steps="135"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.09" steps="134"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_inversion_fo_term_fo_formula_list" expl="VC for rename_free_var_inversion_fo_term_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.06" steps="9"/></proof>
......@@ -59,100 +59,100 @@
<proof prover="2" timelimit="1"><result status="valid" time="0.11" steps="160"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_constructive_inversion_symbol_fo_formula_list" expl="VC for subst_free_var_constructive_inversion_symbol_fo_formula_list">
<proof prover="2"><result status="valid" time="0.36" steps="679"/></proof>
<proof prover="2"><result status="valid" time="0.20" steps="665"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_inversion_symbol_fo_formula_list" expl="VC for subst_free_var_inversion_symbol_fo_formula_list">
<proof prover="2"><result status="valid" time="0.09" steps="57"/></proof>
<proof prover="2"><result status="valid" time="0.09" steps="50"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_constructive_inversion_fo_term_fo_formula_list" expl="VC for subst_free_var_constructive_inversion_fo_term_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.14" steps="386"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.14" steps="382"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_inversion_fo_term_fo_formula_list" expl="VC for subst_free_var_inversion_fo_term_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.07" steps="9"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_symbol_symbol_fo_formula_list" expl="VC for subst_free_var_propagation_symbol_symbol_fo_formula_list">
<proof prover="2"><result status="valid" time="0.51" steps="1036"/></proof>
<proof prover="2"><result status="valid" time="0.35" steps="1080"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_fo_term_symbol_fo_formula_list" expl="VC for subst_free_var_propagation_fo_term_symbol_fo_formula_list">
<proof prover="2"><result status="valid" time="0.76" steps="652"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list" expl="VC for subst_free_var_propagation_fo_term_fo_term_fo_formula_list">
<transf name="split_goal_wp">
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.1" expl="1. postcondition">
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.1" expl="postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.05" steps="12"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.2" expl="2. assertion">
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.2" expl="assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.04" steps="7"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.3" expl="3. variant decrease">
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.3" expl="variant decrease">
<proof prover="2" timelimit="1"><result status="valid" time="0.05" steps="11"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.4" expl="4. assertion">
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.4" expl="assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.05" steps="7"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.5" expl="5. postcondition">
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list.5" expl="postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.06" steps="134"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter free_var_equivalence_of_subst_fo_formula_list" expl="VC for free_var_equivalence_of_subst_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.24" steps="411"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.11" steps="411"/></proof>
</goal>
<goal name="WP_parameter free_var_equivalence_of_rename_fo_formula_list" expl="VC for free_var_equivalence_of_rename_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.08" steps="231"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list" expl="VC for free_var_derive_equivalence_of_subst_fo_formula_list">
<transf name="split_goal_wp">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.1" expl="1. postcondition">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.1" expl="postcondition">
<proof prover="2"><result status="valid" time="0.09" steps="7"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.2" expl="2. postcondition">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.2" expl="postcondition">
<proof prover="2"><result status="valid" time="0.10" steps="7"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.3" expl="3. precondition">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.3" expl="precondition">
<proof prover="2"><result status="valid" time="0.46" steps="132"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.4" expl="4. assertion">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.4" expl="assertion">
<proof prover="2"><result status="valid" time="0.18" steps="154"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.5" expl="5. assertion">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.5" expl="assertion">
<proof prover="2"><result status="valid" time="0.17" steps="135"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.6" expl="6. variant decrease">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.6" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.08" steps="11"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.7" expl="7. precondition">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.7" expl="precondition">
<proof prover="2"><result status="valid" time="0.15" steps="71"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.8" expl="8. assertion">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.8" expl="assertion">
<proof prover="2"><result status="valid" time="0.20" steps="159"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.9" expl="9. assertion">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.9" expl="assertion">
<proof prover="2"><result status="valid" time="0.18" steps="138"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.10" expl="10. postcondition">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.10" expl="postcondition">
<proof prover="2"><result status="valid" time="0.09" steps="37"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.11" expl="11. postcondition">
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.11" expl="postcondition">
<proof prover="2"><result status="valid" time="0.10" steps="37"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list" expl="VC for free_var_derive_equivalence_of_rename_fo_formula_list">
<transf name="split_goal_wp">
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.1" expl="1. precondition">
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.08" steps="6"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.2" expl="2. assertion">
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.2" expl="assertion">
<proof prover="2"><result status="valid" time="0.09" steps="25"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.3" expl="3. assertion">
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.3" expl="assertion">
<proof prover="2"><result status="valid" time="0.10" steps="45"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.4" expl="4. postcondition">
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.4" expl="postcondition">
<proof prover="1"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.5" expl="5. postcondition">
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.5" expl="postcondition">
<proof prover="1"><result status="valid" time="0.74"/></proof>
</goal>
</transf>
......
......@@ -2,17 +2,17 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Firstorder_symbol_impl.mlw">
<theory name="Types" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Logic" sum="8942ac6e2361c16c38459a751e0dbd63">
<theory name="Logic" sum="4d4d8a1b000bd89a62cf255395502f23">
<goal name="WP_parameter nlsize_positive_lemma_symbol" expl="VC for nlsize_positive_lemma_symbol">
<proof prover="7"><result status="valid" time="0.03" steps="5"/></proof>
</goal>
<goal name="WP_parameter shiftb_compose_lemma_symbol" expl="VC for shiftb_compose_lemma_symbol">
<proof prover="7"><result status="valid" time="0.08" steps="146"/></proof>
<proof prover="7"><result status="valid" time="0.08" steps="133"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_symbol" expl="VC for nlmodel_subst_commutation_lemma_symbol">
<proof prover="7"><result status="valid" time="0.02" steps="25"/></proof>
......@@ -21,49 +21,49 @@
<proof prover="7"><result status="valid" time="0.04" steps="39"/></proof>
</goal>
<goal name="WP_parameter bound_depth_of_symbol_in_symbol_nonnegative" expl="VC for bound_depth_of_symbol_in_symbol_nonnegative">
<proof prover="7"><result status="valid" time="0.04" steps="34"/></proof>
<proof prover="7"><result status="valid" time="0.04" steps="30"/></proof>
</goal>
<goal name="WP_parameter model_equal_symbol" expl="VC for model_equal_symbol">
<proof prover="7"><result status="valid" time="0.04" steps="65"/></proof>
<proof prover="7"><result status="valid" time="0.04" steps="64"/></proof>
</goal>
</theory>
<theory name="Impl" sum="68dce20711cd1fde227ae722087cc947">
<theory name="Impl" sum="7cf2267692e6b261fae23742258ab4ff">
<goal name="WP_parameter bind_var_symbol_in_symbol" expl="VC for bind_var_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.10" steps="210"/></proof>
<proof prover="7"><result status="valid" time="0.10" steps="216"/></proof>
</goal>
<goal name="WP_parameter unbind_var_symbol_in_symbol" expl="VC for unbind_var_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.16" steps="280"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol" expl="VC for subst_base_symbol_in_symbol">
<transf name="split_goal_wp">
<goal name="WP_parameter subst_base_symbol_in_symbol.1" expl="1. precondition">
<goal name="WP_parameter subst_base_symbol_in_symbol.1" expl="precondition">
<proof prover="7"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.2" expl="2. precondition">
<proof prover="7"><result status="valid" time="0.04" steps="40"/></proof>
<goal name="WP_parameter subst_base_symbol_in_symbol.2" expl="precondition">
<proof prover="7"><result status="valid" time="0.04" steps="35"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.3" expl="3. postcondition">
<goal name="WP_parameter subst_base_symbol_in_symbol.3" expl="postcondition">
<proof prover="7"><result status="valid" time="0.04" steps="56"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.4" expl="4. postcondition">
<goal name="WP_parameter subst_base_symbol_in_symbol.4" expl="postcondition">
<proof prover="7"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.5" expl="5. postcondition">
<goal name="WP_parameter subst_base_symbol_in_symbol.5" expl="postcondition">
<proof prover="7"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.6" expl="6. postcondition">
<goal name="WP_parameter subst_base_symbol_in_symbol.6" expl="postcondition">
<proof prover="7"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.7" expl="7. postcondition">
<goal name="WP_parameter subst_base_symbol_in_symbol.7" expl="postcondition">
<proof prover="7"><result status="valid" time="0.03" steps="12"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.8" expl="8. postcondition">
<proof prover="7"><result status="valid" time="0.03" steps="31"/></proof>
<goal name="WP_parameter subst_base_symbol_in_symbol.8" expl="postcondition">
<proof prover="7"><result status="valid" time="0.03" steps="36"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.9" expl="9. postcondition">
<goal name="WP_parameter subst_base_symbol_in_symbol.9" expl="postcondition">
<proof prover="7"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_symbol.10" expl="10. postcondition">
<goal name="WP_parameter subst_base_symbol_in_symbol.10" expl="postcondition">
<proof prover="7"><result status="valid" time="0.03" steps="9"/></proof>
</goal>
</transf>
......@@ -76,69 +76,69 @@
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol" expl="VC for nlsubst_symbol_in_symbol">
<transf name="split_goal_wp">
<goal name="WP_parameter nlsubst_symbol_in_symbol.1" expl="1. precondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.1" expl="precondition">
<transf name="inline_goal">
<goal name="WP_parameter nlsubst_symbol_in_symbol.1.1" expl="1. precondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.1.1" expl="precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter nlsubst_symbol_in_symbol.1.1.1" expl="1. precondition">
<proof prover="7"><result status="valid" time="0.12" steps="21"/></proof>
<goal name="WP_parameter nlsubst_symbol_in_symbol.1.1.1" expl="precondition">
<proof prover="7"><result status="valid" time="0.12" steps="23"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.2" expl="2. precondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.2" expl="precondition">
<proof prover="7"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.3" expl="3. precondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.3" expl="precondition">
<proof prover="7"><result status="valid" time="0.03" steps="38"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.4" expl="4. postcondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.4" expl="postcondition">
<proof prover="7"><result status="valid" time="0.03" steps="18"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.5" expl="5. precondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.5" expl="precondition">
<proof prover="7"><result status="valid" time="0.04" steps="51"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.6" expl="6. precondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.6" expl="precondition">
<proof prover="7"><result status="valid" time="0.06" steps="59"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.7" expl="7. precondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.7" expl="precondition">
<proof prover="7"><result status="valid" time="0.05" steps="16"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8" expl="8. assertion">
<goal name="WP_parameter nlsubst_symbol_in_symbol.8" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="1.61"/></proof>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.1" expl="assertion">
<proof prover="1"><result status="valid" time="0.96"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.2" expl="2. assertion">
<proof prover="7"><result status="valid" time="0.08" steps="103"/></proof>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.2" expl="assertion">
<proof prover="7"><result status="valid" time="0.08" steps="105"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="0.78"/></proof>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.3" expl="assertion">
<proof prover="1"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.4" expl="4. assertion">
<proof prover="7"><result status="valid" time="0.03" steps="17"/></proof>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.4" expl="assertion">
<proof prover="7"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.5" expl="5. assertion">
<proof prover="7"><result status="valid" time="0.08" steps="101"/></proof>
<goal name="WP_parameter nlsubst_symbol_in_symbol.8.5" expl="assertion">
<proof prover="7"><result status="valid" time="0.08" steps="102"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.9" expl="9. postcondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.9" expl="postcondition">
<transf name="inline_goal">
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1" expl="1. postcondition">
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1" expl="postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1.1" expl="1. VC for nlsubst_symbol_in_symbol">
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1.1" expl="VC for nlsubst_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.27" steps="613"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1.2" expl="2. VC for nlsubst_symbol_in_symbol">
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1.2" expl="VC for nlsubst_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1.3" expl="3. VC for nlsubst_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.11" steps="140"/></proof>
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1.3" expl="VC for nlsubst_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.11" steps="174"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1.4" expl="4. VC for nlsubst_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.86" steps="502"/></proof>
<goal name="WP_parameter nlsubst_symbol_in_symbol.9.1.4" expl="VC for nlsubst_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.86" steps="492"/></proof>
</goal>
</transf>
</goal>
......
......@@ -2,13 +2,13 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="Spass" version="3.7" timelimit="5" memlimit="1000"/>
<prover id="7" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Firstorder_symbol_spec.mlw" expanded="true">
<theory name="Spec" sum="54ebee0ba44c4d15184f0e0c09def333" expanded="true">
<theory name="Spec" sum="6a7a9c8faa1d9fef0625ce2a32ca8c9d" expanded="true">
<goal name="WP_parameter size_positive_lemma_symbol" expl="VC for size_positive_lemma_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -31,15 +31,15 @@
<proof prover="5"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter right_rename_subst_by_identity_lemma_symbol" expl="VC for right_rename_subst_by_identity_lemma_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.40"/></proof>
<proof prover="0"><result status="valid" time="0.23"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter olifts_composition_lemma_rename_subst_symbol" expl="VC for olifts_composition_lemma_rename_subst_symbol" expanded="true">
<proof prover="5"><result status="valid" time="0.06" steps="257"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="256"/></proof>
</goal>
<goal name="WP_parameter olifts_composition_lemma_subst_rename_symbol" expl="VC for olifts_composition_lemma_subst_rename_symbol" expanded="true">
<proof prover="5"><result status="valid" time="0.14" steps="210"/></proof>
<proof prover="5"><result status="valid" time="0.14" steps="209"/></proof>
</goal>
<goal name="WP_parameter rename_then_subst_composition_lemma_symbol" expl="VC for rename_then_subst_composition_lemma_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
......@@ -80,15 +80,15 @@
<goal name="WP_parameter subst_identity_lemma_symbol" expl="VC for subst_identity_lemma_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter left_subst_subst_identity_lemma_symbol" expl="VC for left_subst_subst_identity_lemma_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.88"/></proof>
<proof prover="0"><result status="valid" time="0.51"/></proof>
<proof prover="1"><result status="valid" time="0.14"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="WP_parameter right_subst_subst_by_identity_lemma_symbol" expl="VC for right_subst_subst_by_identity_lemma_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.93"/></proof>
<proof prover="0"><result status="valid" time="0.56"/></proof>
<proof prover="1"><result status="valid" time="0.14"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
......@@ -105,7 +105,7 @@
<goal name="WP_parameter rename_free_var_inversion_symbol_symbol" expl="VC for rename_free_var_inversion_symbol_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_propagation_symbol_symbol" expl="VC for rename_free_var_propagation_symbol_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
......@@ -114,20 +114,20 @@
</goal>
<goal name="WP_parameter subst_free_var_constructive_inversion_symbol_symbol" expl="VC for subst_free_var_constructive_inversion_symbol_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.07"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_inversion_symbol_symbol" expl="VC for subst_free_var_inversion_symbol_symbol" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter subst_free_var_inversion_symbol_symbol.1" expl="1. variant decrease" expanded="true">
<goal name="WP_parameter subst_free_var_inversion_symbol_symbol.1" expl="variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.07"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_inversion_symbol_symbol.2" expl="2. precondition" expanded="true">
<goal name="WP_parameter subst_free_var_inversion_symbol_symbol.2" expl="precondition" expanded="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_inversion_symbol_symbol.3" expl="3. postcondition" expanded="true">
<goal name="WP_parameter subst_free_var_inversion_symbol_symbol.3" expl="postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.09"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
......@@ -136,7 +136,7 @@
</goal>
<goal name="WP_parameter subst_free_var_propagation_symbol_symbol_symbol" expl="VC for subst_free_var_propagation_symbol_symbol_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter free_var_equivalence_of_subst_symbol" expl="VC for free_var_equivalence_of_subst_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
......@@ -153,7 +153,7 @@
<proof prover="5"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_symbol" expl="VC for free_var_derive_equivalence_of_rename_symbol" expanded="true">
<proof prover="0"><result status="valid" time="0.55"/></proof>
<proof prover="0"><result status="valid" time="0.36"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="40"/></proof>
</goal>
</theory>
......
......@@ -2,10 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Firstorder_tableau_spec.mlw" expanded="true">
<theory name="Spec" sum="04ae47ccff643d8e6498166eda7f9b58">
<theory name="Spec" sum="3acaae3c60dcdf729526d2b71f6ebad5">
<goal name="WP_parameter size_positive_lemma_tableau" expl="VC for size_positive_lemma_tableau">
<proof prover="2"><result status="valid" time="0.16" steps="70"/></proof>
</goal>
......@@ -23,31 +23,31 @@
</goal>
<goal name="WP_parameter subst_composition_lemma_tableau" expl="VC for subst_composition_lemma_tableau">
<transf name="split_goal_wp">
<goal name="WP_parameter subst_composition_lemma_tableau.1" expl="1. postcondition">
<goal name="WP_parameter subst_composition_lemma_tableau.1" expl="postcondition">
<proof prover="2"><result status="valid" time="0.09" steps="7"/></proof>
</goal>
<goal name="WP_parameter subst_composition_lemma_tableau.2" expl="2. variant decrease">
<goal name="WP_parameter subst_composition_lemma_tableau.2" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.10" steps="10"/></proof>
</goal>
<goal name="WP_parameter subst_composition_lemma_tableau.3" expl="3. postcondition">
<goal name="WP_parameter subst_composition_lemma_tableau.3" expl="postcondition">
<proof prover="2"><result status="valid" time="0.11" steps="50"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter subst_identity_lemma_tableau" expl="VC for subst_identity_lemma_tableau">
<proof prover="2"><result status="valid" time="0.20" steps="96"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="96"/></proof>
</goal>
<goal name="WP_parameter renaming_preserve_size_tableau" expl="VC for renaming_preserve_size_tableau">
<proof prover="2"><result status="valid" time="0.14" steps="65"/></proof>
<proof prover="2"><result status="valid" time="0.14" steps="64"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_constructive_inversion_symbol_tableau" expl="VC for rename_free_var_constructive_inversion_symbol_tableau">
<proof prover="2"><result status="valid" time="0.19" steps="171"/></proof>
<proof prover="2"><result status="valid" time="0.19" steps="170"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_inversion_symbol_tableau" expl="VC for rename_free_var_inversion_symbol_tableau">
<proof prover="2"><result status="valid" time="0.10" steps="9"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_constructive_inversion_fo_term_tableau" expl="VC for rename_free_var_constructive_inversion_fo_term_tableau">
<proof prover="2"><result status="valid" time="0.17" steps="171"/></proof>
<proof prover="2"><result status="valid" time="0.17" steps="170"/></proof>
</goal>
<goal name="WP_parameter rename_free_var_inversion_fo_term_tableau" expl="VC for rename_free_var_inversion_fo_term_tableau">
<proof prover="2"><result status="valid" time="0.10" steps="9"/></proof>
......@@ -59,79 +59,79 @@