Commit d49323d1 authored by MARCHE Claude's avatar MARCHE Claude

update session

parent f181fd76
......@@ -25,7 +25,6 @@ topological_sorting.mlw
tortoise_and_hare.mlw
tree_height.mlw
vacid_0_sparse_array.mlw
verifythis_fm2012_LRS.mlw
verifythis_fm2012_treedel.mlw
verifythis_PrefixSumRec.mlw
vstte10_inverting.mlw
......
......@@ -2,7 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="11" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="1000"/>
......@@ -10,191 +11,101 @@
<prover id="14" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="15" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../verifythis_fm2012_LRS.mlw" expanded="true">
<theory name="LCP" sum="821c4c7b4eefc7603fd949478dc68000">
<theory name="LCP" sum="552016829cd88cd233ae59b88005b7b6">
<goal name="not_common_prefix_if_last_char_are_different">
<proof prover="12"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="longest_common_prefix_succ">
<proof prover="12"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="13"><result status="valid" time="0.06"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter lcp" expl="VC for lcp">
<goal name="VC lcp" expl="VC for lcp">
<transf name="split_goal_wp">
<goal name="WP_parameter lcp.1" expl="1. loop invariant init">
<goal name="VC lcp.1" expl="1. loop invariant init">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter lcp.2" expl="2. index in array bounds">
<goal name="VC lcp.2" expl="2. index in array bounds">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter lcp.3" expl="3. index in array bounds">
<goal name="VC lcp.3" expl="3. index in array bounds">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter lcp.4" expl="4. loop invariant preservation">
<proof prover="12"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter lcp.5" expl="5. loop variant decrease">
<goal name="VC lcp.4" expl="4. loop variant decrease">
<proof prover="3" timelimit="5" memlimit="4000"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="1.16"/></proof>
<proof prover="12" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="12"/></proof>
<proof prover="12" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="13" timelimit="5" memlimit="4000"><result status="valid" time="0.01"/></proof>
<proof prover="14" timelimit="5" memlimit="4000"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="WP_parameter lcp.6" expl="6. postcondition">
<proof prover="12" timelimit="20"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="WP_parameter lcp.7" expl="7. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="1.03"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.06"/></proof>
<goal name="VC lcp.5" expl="5. loop invariant preservation">
<proof prover="12"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="WP_parameter lcp.8" expl="8. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.95"/></proof>
<proof prover="12"><result status="valid" time="0.03" steps="15"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.11"/></proof>
<goal name="VC lcp.6" expl="6. postcondition">
<proof prover="12"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="LCP_test" sum="c72f281745bb5c07623e7c7b5db2aa2f">
<goal name="WP_parameter bench" expl="VC for bench">
<proof prover="12" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="14"/></proof>
<theory name="LCP_test" sum="e356df98e287e0b24a6456ac61581533">
<goal name="VC bench" expl="VC for bench">
<proof prover="12" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
</theory>
<theory name="SuffixSort" sum="f964e891d2b66f843c1077481bdba58f">
<goal name="WP_parameter compare" expl="VC for compare">
<theory name="SuffixSort" sum="ebb933bb70a5b9281d13c73fc8c99685">
<goal name="VC compare" expl="VC for compare">
<transf name="split_goal_wp">
<goal name="WP_parameter compare.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.4" expl="4. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.5" expl="5. precondition">
<goal name="VC compare.1" expl="1. precondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.6" expl="6. postcondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<goal name="VC compare.2" expl="2. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.7" expl="7. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="WP_parameter compare.8" expl="8. postcondition">
<goal name="VC compare.3" expl="3. index in array bounds">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.05"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter compare.9" expl="9. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.10" expl="10. postcondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter compare.11" expl="11. postcondition">
<proof prover="12"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter compare.12" expl="12. index in array bounds">
<goal name="VC compare.4" expl="4. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter compare.13" expl="13. index in array bounds">
<goal name="VC compare.5" expl="5. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="15"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compare.14" expl="14. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.15" expl="15. postcondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="25"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compare.16" expl="16. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter compare.17" expl="17. index in array bounds">
<goal name="VC compare.6" expl="6. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="14"/></proof>
......@@ -202,35 +113,24 @@
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.18" expl="18. index in array bounds">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
<goal name="VC compare.7" expl="7. unreachable point">
<proof prover="12"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter compare.19" expl="19. postcondition">
<goal name="VC compare.8" expl="8. postcondition">
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="11"><result status="valid" time="0.12"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
<proof prover="15"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compare.20" expl="20. postcondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="15"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter compare.21" expl="21. postcondition">
<proof prover="12"><result status="valid" time="0.02" steps="33"/></proof>
<goal name="VC compare.9" expl="9. postcondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="28"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compare.22" expl="22. unreachable point">
<proof prover="12"><result status="valid" time="0.02" steps="27"/></proof>
<goal name="VC compare.10" expl="10. postcondition">
<proof prover="12"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
</transf>
</goal>
......@@ -241,302 +141,232 @@
<proof prover="14"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="le_trans">
<proof prover="12"><result status="valid" time="0.10" steps="235"/></proof>
<proof prover="12"><result status="valid" time="0.10" steps="236"/></proof>
</goal>
<goal name="WP_parameter sort" expl="VC for sort">
<goal name="VC sort" expl="VC for sort">
<transf name="split_goal_wp">
<goal name="WP_parameter sort.1" expl="1. postcondition">
<goal name="VC sort.1" expl="1. loop bounds">
<proof prover="3"><result status="valid" time="0.13"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="14"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC sort.2" expl="2. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.37"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="7"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter sort.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.34"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<goal name="VC sort.3" expl="3. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="WP_parameter sort.3" expl="3. loop invariant init">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.34"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<goal name="VC sort.4" expl="4. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="13"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.46"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.4" expl="4. loop invariant init">
<goal name="VC sort.5" expl="5. loop invariant init">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.5" expl="5. loop invariant init">
<goal name="VC sort.6" expl="6. loop invariant init">
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.6" expl="6. loop invariant init">
<goal name="VC sort.7" expl="7. loop invariant init">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.7" expl="7. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="13"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter sort.8" expl="8. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.04"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="10"/></proof>
<goal name="VC sort.8" expl="8. loop invariant init">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter sort.9" expl="9. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.10" expl="10. loop invariant init">
<goal name="VC sort.9" expl="9. loop invariant init">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="WP_parameter sort.11" expl="11. loop invariant init">
<goal name="VC sort.10" expl="10. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.12"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="13"><result status="valid" time="0.05"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
<proof prover="15"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter sort.12" expl="12. type invariant">
<goal name="VC sort.11" expl="11. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.63"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.13" expl="13. index in array bounds">
<goal name="VC sort.12" expl="12. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="1.04"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="17"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="13"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sort.14" expl="14. index in array bounds">
<goal name="VC sort.13" expl="13. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="18"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="45"/></proof>
<proof prover="13"><result status="valid" time="0.05"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sort.15" expl="15. precondition">
<goal name="VC sort.14" expl="14. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.22"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="29"/></proof>
<proof prover="11"><result status="valid" time="0.57"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="45"/></proof>
<proof prover="13"><result status="valid" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter sort.16" expl="16. precondition">
<goal name="VC sort.15" expl="15. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.21"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="29"/></proof>
<proof prover="13"><result status="valid" time="0.05"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="16"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="WP_parameter sort.17" expl="17. index in array bounds">
<goal name="VC sort.16" expl="16. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="27"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.18" expl="18. index in array bounds">
<goal name="VC sort.17" expl="17. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="11"><result status="valid" time="0.42"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.19" expl="19. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="13"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sort.20" expl="20. index in array bounds">
<goal name="VC sort.18" expl="18. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sort.21" expl="21. assertion">
<proof prover="12"><result status="valid" time="0.04" steps="64"/></proof>
</goal>
<goal name="WP_parameter sort.22" expl="22. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.22"/></proof>
<proof prover="12"><result status="valid" time="0.02" steps="29"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="30"/></proof>
<proof prover="13"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter sort.23" expl="23. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="13"><result status="valid" time="0.81"/></proof>
<transf name="inline_goal">
<goal name="WP_parameter sort.23.1" expl="1. loop invariant preservation">
<proof prover="12"><result status="valid" time="0.42" steps="150"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sort.24" expl="24. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.13"/></proof>
<proof prover="12"><result status="valid" time="2.00" steps="401"/></proof>
<proof prover="14"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter sort.25" expl="25. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="14"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="WP_parameter sort.26" expl="26. loop invariant preservation">
<proof prover="13" timelimit="5"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="WP_parameter sort.27" expl="27. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.05"/></proof>
<goal name="VC sort.19" expl="19. assertion">
<proof prover="12"><result status="valid" time="0.04" steps="99"/></proof>
</goal>
<goal name="WP_parameter sort.28" expl="28. loop variant decrease">
<goal name="VC sort.20" expl="20. loop variant decrease">
<proof prover="11"><result status="valid" time="0.15"/></proof>
<proof prover="12" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="29"/></proof>
<proof prover="12" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="14" timelimit="5" memlimit="4000"><result status="valid" time="0.04"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter sort.29" expl="29. assertion">
<goal name="VC sort.21" expl="21. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.03"/></proof>