Commit 3af28b7a authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

update unchanged sessions, cont.

parent b3e30629
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="3">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
......@@ -34,7 +34,7 @@
name="Test1"
locfile="../formula.why"
loclnum="47" loccnumb="7" loccnume="12"
sum="bb895b30ba659fcab00d3a6bc4a96a4a"
sum="6c87c2af38a2791504726f9df017b072"
proved="true"
expanded="true"
shape="ainfix =aevalaForaFnotaFatomV0aFfalseV1aFalseLasetaconstaFalseV0aTrueLamk_identc0">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="3">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
......@@ -39,7 +39,7 @@
name="ident_eq_dec"
locfile="../imp_n.why"
loclnum="8" loccnumb="6" loccnume="18"
sum="d8b3349496884adeacfffaa63643f166"
sum="3675af500a069c66a22b4d644e748b6d"
proved="true"
expanded="false"
shape="Nainfix =V0V1Oainfix =V0V1F">
......@@ -56,7 +56,7 @@
name="check_skip"
locfile="../imp_n.why"
loclnum="32" loccnumb="6" loccnume="16"
sum="c35750e90768e99a7e470a4dbc3b1298"
sum="bd2df32bc63e96f186f34241083f0b6d"
proved="true"
expanded="false"
shape="Nainfix =V0aSskipOainfix =V0aSskipF">
......@@ -73,7 +73,7 @@
name="Test13"
locfile="../imp_n.why"
loclnum="59" loccnumb="7" loccnume="13"
sum="4312b5666c7692b0606faeaea4055be7"
sum="135ff0374858bfc2bcdc00245700858c"
proved="true"
expanded="false"
shape="ainfix =aeval_exprV0aEconstc13c13Laconstc0">
......@@ -90,7 +90,7 @@
name="Test42"
locfile="../imp_n.why"
loclnum="63" loccnumb="7" loccnume="13"
sum="efd7e564b6940ff29140e3fea0390012"
sum="dedf593e9119ad8aa918944509ccca3e"
proved="true"
expanded="false"
shape="ainfix =aeval_exprV1aEvarV0c42Lasetaconstc0V0c42Lamk_identc0">
......@@ -107,7 +107,7 @@
name="Test55"
locfile="../imp_n.why"
loclnum="68" loccnumb="7" loccnume="13"
sum="8de923382fb4d4e271c576030da077d1"
sum="4221bb40dfa5683a460026752186af78"
proved="true"
expanded="false"
shape="ainfix =aeval_exprV1aEbinaEvarV0aOplusaEconstc13c55Lasetaconstc0V0c42Lamk_identc0">
......@@ -124,7 +124,7 @@
name="Ass42"
locfile="../imp_n.why"
loclnum="112" loccnumb="7" loccnume="12"
sum="8f2f166e8dc44ca0be1a2c3510b368c7"
sum="51d613fd039be7bbb0c9724106a40e52"
proved="true"
expanded="false"
shape="ainfix =agetV2V0c42Iaone_stepV1aSassignV0aEconstc42V2aSskipFLaconstc0Lamk_identc0">
......@@ -141,7 +141,7 @@
name="If42"
locfile="../imp_n.why"
loclnum="119" loccnumb="7" loccnume="11"
sum="6acb1d5e60ce4206b0bc086fce883bdf"
sum="e4612157984e9b07ec1bdec65dffc1a1"
proved="true"
expanded="false"
shape="ainfix =agetV3V0c42Iaone_stepV2V4V3aSskipIaone_stepV1aSifaEvarV0aSassignV0aEconstc13aSassignV0aEconstc42V2V4FLaconstc0Lamk_identc0">
......@@ -174,7 +174,7 @@
name="progress"
locfile="../imp_n.why"
loclnum="131" loccnumb="8" loccnume="16"
sum="95dcf2d0cacebb80eac8815aa1240958"
sum="124b793e26b8260e9f06485a9c36f230"
proved="true"
expanded="false"
shape="aone_stepV0V1V2V3EINainfix =V1aSskipF">
......@@ -192,7 +192,7 @@
name="steps_non_neg"
locfile="../imp_n.why"
loclnum="148" loccnumb="6" loccnume="19"
sum="2e21f47991349d8d42919e56f0308d64"
sum="8b26e0832d9762a00f19c43bcf5cbc79"
proved="true"
expanded="false"
shape="ainfix &gt;=V4c0Iamany_stepsV0V2V1V3V4F">
......@@ -210,7 +210,7 @@
name="many_steps_seq"
locfile="../imp_n.why"
loclnum="152" loccnumb="6" loccnume="20"
sum="753b9d62a6fd037888ac32860317e4e9"
sum="03ac5bdad6cf20adf8c5bfc5c76f004f"
proved="true"
expanded="false"
shape="ainfix =V4ainfix +ainfix +c1V6V7Aamany_stepsV5V3V1aSskipV7Aamany_stepsV0V2V5aSskipV6EIamany_stepsV0aSseqV2V3V1aSskipV4F">
......@@ -228,7 +228,7 @@
name="eval_subst_expr"
locfile="../imp_n.why"
loclnum="186" loccnumb="6" loccnume="21"
sum="afab08b3d0114ce023767fdf954895d8"
sum="c780f943c0c39c7d098683c1e3f2ca5e"
proved="true"
expanded="false"
shape="ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F">
......@@ -246,7 +246,7 @@
name="eval_subst"
locfile="../imp_n.why"
loclnum="199" loccnumb="6" loccnume="16"
sum="73a9fcd288ef3ce8e0f1e7ef3ea52d29"
sum="dec078cfda368a18aebbec9544070181"
proved="true"
expanded="false"
shape="aeval_fmlaasetV0V2aeval_exprV0V3V1qaeval_fmlaV0asubstV1V2V3F">
......@@ -264,7 +264,7 @@
name="skip_rule"
locfile="../imp_n.why"
loclnum="214" loccnumb="6" loccnume="15"
sum="b7e2d5d49bd3f184c7cfc8cec8f06686"
sum="8afa9331e7a2ac192dbf870a525991e2"
proved="true"
expanded="false"
shape="avalid_tripleV0aSskipV0F">
......@@ -281,7 +281,7 @@
name="assign_rule"
locfile="../imp_n.why"
loclnum="217" loccnumb="6" loccnume="17"
sum="fa7246dc84574651c4918cadd45cbb90"
sum="84c026d4365da03d1d42701df97c46eb"
proved="true"
expanded="false"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
......@@ -299,7 +299,7 @@
name="seq_rule"
locfile="../imp_n.why"
loclnum="221" loccnumb="6" loccnume="14"
sum="464d28512d7ba27f59a0ce429768bddb"
sum="67e820ed6b096f7153b2c040c96ac7d0"
proved="true"
expanded="false"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
......@@ -317,7 +317,7 @@
name="if_rule"
locfile="../imp_n.why"
loclnum="226" loccnumb="6" loccnume="13"
sum="f07c333e87afb40999af74eccc40fdd4"
sum="6f3382e6acc68e7c6b3cf60fd64362a2"
proved="true"
expanded="false"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
......@@ -335,7 +335,7 @@
name="while_rule"
locfile="../imp_n.why"
loclnum="232" loccnumb="6" loccnume="16"
sum="7d44b3d3273b9b5b385582c56206be90"
sum="e7e84bcc9159a13ea5fe12d4aa040b43"
proved="true"
expanded="false"
shape="avalid_tripleV1aSwhileV0V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
......@@ -353,7 +353,7 @@
name="consequence_rule"
locfile="../imp_n.why"
loclnum="237" loccnumb="6" loccnume="22"
sum="0c935c99185ac468b9c4ccd481d2d9f0"
sum="530e2058ba35620f46993c6545f2eaba"
proved="true"
expanded="false"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="3">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
......@@ -39,7 +39,7 @@
name="eval_subst_term"
locfile="../wp2.mlw"
loclnum="99" loccnumb="6" loccnume="21"
sum="291d9138ec663a31cfb7dd532ae32f95"
sum="2e4c037afbd266a08f7ae24de97f317a"
proved="true"
expanded="false"
shape="ainfix =aeval_termV0V1asubst_termV2V3V4aeval_termasetV0V3agetV1V4V1V2Iafresh_in_termV4V2F">
......@@ -57,7 +57,7 @@
name="eval_term_change_free"
locfile="../wp2.mlw"
loclnum="105" loccnumb="6" loccnume="27"
sum="ca67cf34867d434b30531f77f742d66a"
sum="a30ddd6ad8fca6e2f1a446da2a61b13d"
proved="true"
expanded="false"
shape="ainfix =aeval_termV1asetV2V3V4V0aeval_termV1V2V0Iafresh_in_termV3V0F">
......@@ -75,7 +75,7 @@
name="eval_subst"
locfile="../wp2.mlw"
loclnum="131" loccnumb="6" loccnume="16"
sum="735f6d5c4ff9a5027667324609319031"
sum="d03ffba9c7e539a42633a71a528a3179"
proved="true"
expanded="false"
shape="aeval_fmlaasetV1V3agetV2V4V2V0qaeval_fmlaV1V2asubstV0V3V4Iafresh_in_fmlaV4V0F">
......@@ -93,7 +93,7 @@
name="eval_swap"
locfile="../wp2.mlw"
loclnum="137" loccnumb="6" loccnume="15"
sum="3d3e8d7a47e96ec0084eb0cece4c30ba"
sum="d338fa2264560ab2bf1c92c6b6fb8f2a"
proved="true"
expanded="false"
shape="aeval_fmlaV1asetasetV2V4V6V3V5V0qaeval_fmlaV1asetasetV2V3V5V4V6V0INainfix =V3V4F">
......@@ -118,7 +118,7 @@
name="eval_change_free"
locfile="../wp2.mlw"
loclnum="143" loccnumb="6" loccnume="22"
sum="8c02f93e41f9ff0ae0bbb58433d18bd7"
sum="c2f71dda154524507d9d5892ae3a95b4"
proved="true"
expanded="false"
shape="aeval_fmlaV1V2V0qaeval_fmlaV1asetV2V3V4V0Iafresh_in_fmlaV3V0F">
......@@ -136,7 +136,7 @@
name="check_skip"
locfile="../wp2.mlw"
loclnum="158" loccnumb="6" loccnume="16"
sum="4cb33c7fcf193e306777c152abd0052a"
sum="6c5144e6f38fb62a405839d017c2b2d3"
proved="true"
expanded="false"
shape="Nainfix =V0aSskipOainfix =V0aSskipF">
......@@ -185,7 +185,7 @@
name="steps_non_neg"
locfile="../wp2.mlw"
loclnum="227" loccnumb="6" loccnume="19"
sum="2b2e6eebd1f04bc6fa1686016e2a719c"
sum="7842350a2b92583cd45a725d5f60ca1f"
proved="true"
expanded="false"
shape="ainfix &gt;=V6c0Iamany_stepsV0V1V4V2V3V5V6F">
......@@ -203,7 +203,7 @@
name="many_steps_seq"
locfile="../wp2.mlw"
loclnum="231" loccnumb="6" loccnume="20"
sum="463d6a2faaf5b29d3d104dddd9e5eb19"
sum="280929659e33b9d86316dd5438464f70"
proved="true"
expanded="false"
shape="ainfix =V6ainfix +ainfix +c1V9V10Aamany_stepsV7V8V5V2V3aSskipV10Aamany_stepsV0V1V4V7V8aSskipV9EIamany_stepsV0V1aSseqV4V5V2V3aSskipV6F">
......@@ -214,7 +214,7 @@
edited="wp2_Imp_many_steps_seq_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.58"/>
<result status="valid" time="1.30"/>
</proof>
</goal>
</theory>
......@@ -228,7 +228,7 @@
name="Test13"
locfile="../wp2.mlw"
loclnum="269" loccnumb="5" loccnume="11"
sum="8f8109446a10c1c41852be2a9606467a"
sum="b658d2ac0d91a6367c0a15f8d8c3dd69"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_sigmaamy_piaTconstc13aVintc13">
......@@ -261,7 +261,7 @@
name="Test42"
locfile="../wp2.mlw"
loclnum="272" loccnumb="5" loccnume="11"
sum="7799d81d820eefa52a7341c55acfe056"
sum="9e0f7495e71f1ecb7e20fab0aa06c784"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_sigmaamy_piaTvarc0aVintc42">
......@@ -294,7 +294,7 @@
name="Test0"
locfile="../wp2.mlw"
loclnum="275" loccnumb="5" loccnume="10"
sum="39f9d967e166c8a0449e8f009b3b343a"
sum="12ed35f59176d192e548c8b069a9f913"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_sigmaamy_piaTderefc0aVintc0">
......@@ -327,7 +327,7 @@
name="Test55"
locfile="../wp2.mlw"
loclnum="278" loccnumb="5" loccnume="11"
sum="124bef4c5037af2e977d4c62f11f7aa4"
sum="79b40ee38a3092564438bcc19dd756fe"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_sigmaamy_piaTbinaTvarc0aOplusaTconstc13aVintc55">
......@@ -345,7 +345,7 @@
name="Ass42"
locfile="../wp2.mlw"
loclnum="281" loccnumb="5" loccnume="10"
sum="52866c4bd8577719fc74ddb8734e4488"
sum="53e2b4134cf69052e917447365b11547"
proved="true"
expanded="false"
shape="ainfix =agetV1V0aVintc42Iaone_stepamy_sigmaamy_piaSassignV0aTconstc42V1V2aSskipFLc0">
......@@ -378,7 +378,7 @@
name="If42"
locfile="../wp2.mlw"
loclnum="287" loccnumb="5" loccnume="9"
sum="65710dfbf6b7d9f31b6c7db73bcea0f1"
sum="4aac77b4f51485ca09756c53a6369042"
proved="true"
expanded="false"
shape="ainfix =agetV3V0aVintc13Iaone_stepV1V2V5V3V4aSskipIaone_stepamy_sigmaamy_piaSifaTbinaTderefV0aOleaTconstc10aSassignV0aTconstc13aSassignV0aTconstc42V1V2V5FLc0">
......@@ -389,7 +389,7 @@
edited="wp2_TestSemantics_If42_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.67"/>
<result status="valid" time="2.17"/>
</proof>
</goal>
</theory>
......@@ -403,7 +403,7 @@
name="consequence_rule"
locfile="../wp2.mlw"
loclnum="309" loccnumb="6" loccnume="22"
sum="8c43d142f469f49a0827c970c6d9bd74"
sum="f5a3a490a893030f249bca80efbb8c4f"
proved="true"
expanded="false"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
......@@ -428,7 +428,7 @@
name="skip_rule"
locfile="../wp2.mlw"
loclnum="316" loccnumb="6" loccnume="15"
sum="6bf7ae34ccdfa310b1af3626b0b03f76"
sum="f9bea1f73f412d47702a30265a27ed5a"
proved="true"
expanded="false"
shape="avalid_tripleV0aSskipV0F">
......@@ -446,7 +446,7 @@
name="assign_rule"
locfile="../wp2.mlw"
loclnum="319" loccnumb="6" loccnume="17"
sum="beb761de1befb1782089a8d198000422"
sum="0c96fcc9c8c94ed3f7948f32800061f4"
proved="true"
expanded="false"
shape="avalid_tripleaFletV2V3asubstV0V1V2aSassignV1V3V0Iafresh_in_fmlaV2V0F">
......@@ -464,7 +464,7 @@
name="seq_rule"
locfile="../wp2.mlw"
loclnum="324" loccnumb="6" loccnume="14"
sum="50cfd418dc1ca5bd30218442c7cb0e0c"
sum="16047a9bd9df5cc77ab66df8f7262bef"
proved="true"
expanded="false"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
......@@ -489,7 +489,7 @@
name="if_rule"
locfile="../wp2.mlw"
loclnum="329" loccnumb="6" loccnume="13"
sum="4aa9f8a6dcaa50cf9966f93e3fa9234f"
sum="408fa3a12ea55807f3a8d84dc048c21e"
proved="true"
expanded="false"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
......@@ -507,7 +507,7 @@
name="assert_rule"
locfile="../wp2.mlw"
loclnum="335" loccnumb="6" loccnume="17"
sum="1a928030d59e225f399b8839608905d1"
sum="d21b7817e94465f7e430a54e26cfe4c4"
proved="true"
expanded="false"
shape="avalid_tripleV1aSassertV0V1Iavalid_fmlaaFimpliesV1V0F">
......@@ -525,7 +525,7 @@
name="assert_rule_ext"
locfile="../wp2.mlw"
loclnum="339" loccnumb="6" loccnume="21"
sum="848c2bf0bf5f71304aa29a5b89ae8247"
sum="b062e1c19e0d156adc26b90d1381156d"
proved="true"
expanded="false"
shape="avalid_tripleaFimpliesV0V1aSassertV0V1F">
......@@ -536,14 +536,14 @@
edited="wp2_HoareLogic_assert_rule_ext_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.26"/>
<result status="valid" time="1.53"/>
</proof>
</goal>
<goal
name="while_rule"
locfile="../wp2.mlw"
loclnum="343" loccnumb="6" loccnume="16"
sum="96f64972e9c3cfa386e0b0ea5af31be8"
sum="21308e604ef949a00c70a0cfb80b1f7e"
proved="true"
expanded="false"
shape="avalid_tripleV1aSwhileV0V1V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
......@@ -561,7 +561,7 @@
name="while_rule_ext"
locfile="../wp2.mlw"
loclnum="348" loccnumb="6" loccnume="20"
sum="24ee1c49c8a534345a743fa565f9cc45"
sum="4e50d02fbd31a0e50784958fa7a72750"
proved="true"
expanded="false"
shape="avalid_tripleV2aSwhileV0V1V3aFandaFnotaFtermV0V2Iavalid_tripleaFandaFtermV0V2V3V2Iavalid_fmlaaFimpliesV2V1F">
......@@ -586,7 +586,7 @@
name="assigns_refl"
locfile="../wp2.mlw"
loclnum="370" loccnumb="6" loccnume="18"
sum="917e738c805bc081f6e77003c2097720"
sum="a168300a72d66e8c101156a322dbf110"
proved="true"
expanded="false"
shape="aassignsV0V1V0F">
......@@ -603,7 +603,7 @@
name="assigns_trans"
locfile="../wp2.mlw"
loclnum="373" loccnumb="6" loccnume="19"
sum="ca448a2dac3e685af8e22fc106afb10e"
sum="825720978e5079583c0c279d13ab1150"
proved="true"
expanded="false"
shape="aassignsV0V3V2IaassignsV1V3V2AaassignsV0V3V1F">
......@@ -620,7 +620,7 @@
name="assigns_union_left"
locfile="../wp2.mlw"
loclnum="378" loccnumb="6" loccnume="24"
sum="1858fea2e545d1cf657098e7ae5de980"
sum="4739c14078e5a321416642d554e7d0de"
proved="true"
expanded="false"
shape="aassignsV0aunionV2V3V1IaassignsV0V2V1F">
......@@ -637,7 +637,7 @@
name="assigns_union_right"
locfile="../wp2.mlw"
loclnum="382" loccnumb="6" loccnume="25"
sum="0c66fb2a02b157088a963e0a1752b553"
sum="57386ca4927e42c3cd56a5c30fd3ebe1"
proved="true"
expanded="false"
shape="aassignsV0aunionV2V3V1IaassignsV0V3V1F">
......@@ -655,7 +655,7 @@
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="VC for compute_writes"
sum="263470248b97b3e3fdf32310f7e25862"
sum="b0a2b8d17c3d3143802895f1df6850c8"
proved="true"
expanded="false"
shape="CaassignsV1aemptyV3Iamany_stepsV1V2V0V3V4aSskipV5FaSskipaassignsV7asingletonV6V9Iamany_stepsV7V8V0V9V10aSskipV11FaSassignVwaassignsV16aunionV15V14V18Iamany_stepsV16V17V0V18V19aSskipV20FIaassignsV21V15V23Iamany_stepsV21V22V12V23V24aSskipV25FFIaassignsV26V14V28Iamany_stepsV26V27V13V28V29aSskipV30FFaSseqVVaassignsV35aunionV34V33V37Iamany_stepsV35V36V0V37V38aSskipV39FIaassignsV40V34V42Iamany_stepsV40V41V31V42V43aSskipV44FFIaassignsV45V33V47Iamany_stepsV45V46V32V47V48aSskipV49FFaSifwVVaassignsV52V51V54Iamany_stepsV52V53V0V54V55aSskipV56FIaassignsV57V51V59Iamany_stepsV57V58V50V59V60aSskipV61FFaSwhilewwVaassignsV62aemptyV64Iamany_stepsV62V63V0V64V65aSskipV66FaSassertwV0F">
......@@ -670,7 +670,7 @@
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="1. postcondition"
sum="bb5ab8c5a49354043a4ac8870c04c0bc"
sum="ff8de2ac027df4a0d293d26b816d1ebf"
proved="true"
expanded="false"
shape="postconditionCaassignsV1aemptyV3Iamany_stepsV1V2V0V3V4aSskipV5FaSskiptaSassignVwtaSseqVVtaSifwVVtaSwhilewwVtaSassertwV0F">
......@@ -690,7 +690,7 @@
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="2. postcondition"
sum="c08fe02ff7c778d454c3bfa688d7b976"
sum="dd9191fb7a781f06f48f415410ec243c"
proved="true"
expanded="false"
shape="postconditionCtaSskipaassignsV2asingletonV1V4Iamany_stepsV2V3V0V4V5aSskipV6FaSassignVwtaSseqVVtaSifwVVtaSwhilewwVtaSassertwV0F">
......@@ -711,7 +711,7 @@
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="3. postcondition"
sum="d30f9425af2a6ae302a6a9ae82d12c0e"
sum="0b4f44d952bd33222a9541bda281477c"
proved="true"
expanded="false"
shape="postconditionCtaSskiptaSassignVwaassignsV6aunionV5V4V8Iamany_stepsV6V7V0V8V9aSskipV10FIaassignsV11V5V13Iamany_stepsV11V12V2V13V14aSskipV15FFIaassignsV16V4V18Iamany_stepsV16V17V3V18V19aSskipV20FFaSseqVVtaSifwVVtaSwhilewwVtaSassertwV0F">
......@@ -739,7 +739,7 @@
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="4. postcondition"
sum="3d99e0ef75cd0886698f183735fbb5c2"
sum="886d457f88bec274ca9d465456e5d905"
proved="true"
expanded="false"
shape="postconditionCtaSskiptaSassignVwtaSseqVVaassignsV8aunionV7V6V10Iamany_stepsV8V9V0V10V11aSskipV12FIaassignsV13V7V15Iamany_stepsV13V14V4V15V16aSskipV17FFIaassignsV18V6V20Iamany_stepsV18V19V5V20V21aSskipV22FFaSifwVVtaSwhilewwVtaSassertwV0F">
......@@ -760,7 +760,7 @@
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="5. postcondition"
sum="7464dfc6796b18bc12805b10a000326a"
sum="3533b88fae070c7c83d6a1a0a3a2f5af"
proved="true"
expanded="false"
shape="postconditionCtaSskiptaSassignVwtaSseqVVtaSifwVVaassignsV8V7V10Iamany_stepsV8V9V0V10V11aSskipV12FIaassignsV13V7V15Iamany_stepsV13V14V6V15V16aSskipV17FFaSwhilewwVtaSassertwV0F">
......@@ -781,7 +781,7 @@
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="6. postcondition"
sum="151f0d3abbcf3d4bd1cf6f1493524930"
sum="9152d3bc1e32ed01365bcda5cce22948"
proved="true"
expanded="false"
shape="postconditionCtaSskiptaSassignVwtaSseqVVtaSifwVVtaSwhilewwVaassignsV7aemptyV9Iamany_stepsV7V8V0V9V10aSskipV11FaSassertwV0F">
......@@ -804,7 +804,7 @@
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="VC for wp"
sum="b98893955051aa18fbd79493e9263be4"
sum="80dc9a726d98389b21dea4bf407db378"
proved="true"
expanded="false"
shape="Cavalid_tripleV1V0V1aSskipavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSseqVVavalid_tripleaFletV8V7asubstV1V6V8V0V1Iafresh_in_fmlaV8V1FaSassignVVavalid_tripleaFandaFimpliesaFtermV9V13aFimpliesaFnotaFtermV9V12V0V1Iavalid_tripleV13V10V1FIavalid_tripleV12V11V1FaSifVVVavalid_tripleaFimpliesV14V1V0V1aSassertVavalid_tripleaFandV16V19V0V1Iaeval_fmlaV22V23V19Iamany_stepsV20V21V17V22V23aSskipV24FAaeval_fmlaV20V21aFandaFimpliesaFandaFtermV15V16V18aFimpliesaFandaFnotaFtermV15V16V1Iaeval_fmlaV20V21V19FFIavalid_tripleV18V17V16FaSwhileVVVV0F">
......@@ -819,7 +819,7 @@
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="1. postcondition"
sum="a244097660f21923673f60dabbfcef7c"
sum="1997ad871f0dd6955e025bf928ed436d"
proved="true"
expanded="false"
shape="postconditionCavalid_tripleV1V0V1aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVV0F">
......@@ -871,7 +871,7 @@
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="2. postcondition"
sum="a0fe266d6a46036af8570fb892f7ae5e"
sum="c74a84cad2fb98f2d4f29a2690f82b00"
proved="true"
expanded="false"
shape="postconditionCtaSskipavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVV0F">
......@@ -923,7 +923,7 @@
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="3. postcondition"
sum="b46a1a5f1aec9204b6d3ede6e2d7a980"
sum="bc20814f918b6acee3d956df9e110e85"
proved="true"
expanded="false"
shape="postconditionCtaSskiptaSseqVVavalid_tripleaFletV6V5asubstV1V4V6V0V1Iafresh_in_fmlaV6V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVV0F">
......@@ -975,7 +975,7 @@
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="4. postcondition"
sum="3bc07440eef1b2d233a0576f245cd525"
sum="4ca0db8d4e64ec6cb17d0dc50e37c807"
proved="true"
expanded="false"
shape="postconditionCtaSskiptaSseqVVtaSassignVVavalid_tripleaFandaFimpliesaFtermV6V10aFimpliesaFnotaFtermV6V9V0V1Iavalid_tripleV10V7V1FIavalid_tripleV9V8V1FaSifVVVtaSassertVtaSwhileVVVV0F">
......@@ -996,7 +996,7 @@
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="5. postcondition"
sum="20304ff46a692c27394dfbc56e492efa"
sum="ff39a83899b9df2d9f6dba34de44ceb0"
proved="true"
expanded="false"
shape="postconditionCtaSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFimpliesV9V1V0V1aSassertVtaSwhileVVVV0F">
......@@ -1048,7 +1048,7 @@
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="6. postcondition"
sum="ab23cada9e54c2b1db47382ca79fc8e0"
sum="89d58b046b3b166ada0c31cdedcf1d10"
proved="true"
expanded="false"
shape="postconditionCtaSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFandV11V14V0V1Iaeval_fmlaV17V18V14Iamany_stepsV15V16V12V17V18aSskipV19FAaeval_fmlaV15V16aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1Iaeval_fmlaV15V16V14FFIavalid_tripleV13V12V11FaSwhileVVVV0F">
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment