Commit 3ee1d6e5 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent 0bc081ae
......@@ -51,7 +51,7 @@
name="vertices_cardinal_pos"
locfile="../bellman_ford.mlw"
loclnum="30" loccnumb="8" loccnume="29"
sum="b53f5921e10c8afb9006fe710f5e239e"
sum="5e16c68f55cd4c91178c194510afe3e9"
proved="true"
expanded="true"
shape="ainfix >acardinalaverticesc0">
......@@ -68,7 +68,7 @@
name="path_in_vertices"
locfile="../bellman_ford.mlw"
loclnum="36" loccnumb="8" loccnume="24"
sum="06e5c788d62947e760a274766425f577"
sum="a9bf87357d644caa6cb99de3b0025d5d"
proved="true"
expanded="true"
shape="amemV1averticesIapathV0V2V1IamemV0averticesF">
......@@ -86,7 +86,7 @@
name="long_path_decomposition_pigeon1"
locfile="../bellman_ford.mlw"
loclnum="60" loccnumb="8" loccnume="39"
sum="f0f7e31c25a12d45a3ad5dc9fe881499"
sum="7c8d2322bed6f8662af6a4fec3d57db4"
proved="true"
expanded="true"
shape="amemV2averticesIamemV2aConsV1V0FINainfix =V0aNilIapathasV0V1F">
......@@ -104,7 +104,7 @@
name="long_path_decomposition_pigeon2"
locfile="../bellman_ford.mlw"
loclnum="65" loccnumb="8" loccnume="39"
sum="63a6266f8603de0769159337ca28ae4f"
sum="90517c9b20c3d697370bb72fd41cc63c"
proved="true"
expanded="true"
shape="ainfix =aConsV1V0ainfix ++V3aConsV2ainfix ++V4aConsV2V5EIainfix >alengthaConsV1V0acardinalaverticesIamemV6averticesIamemV6aConsV1V0FF">
......@@ -121,7 +121,7 @@
name="long_path_decomposition_pigeon3"
locfile="../bellman_ford.mlw"
loclnum="72" loccnumb="8" loccnume="39"
sum="80a24999193f86edd4df497d838bd516"
sum="fcf1da420ee6e7166c94a0ccd0780086"
proved="true"
expanded="true"
shape="ainfix =V0ainfix ++V3aConsV2ainfix ++V4aConsV2V5EOainfix =V0ainfix ++V6aConsV1V7EIainfix =aConsV1V0ainfix ++V9aConsV8ainfix ++V10aConsV8V11EF">
......@@ -132,14 +132,14 @@
edited="bellman_ford_Graph_long_path_decomposition_pigeon3_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.90"/>
<result status="valid" time="2.30"/>
</proof>
</goal>
<goal
name="long_path_decomposition"
locfile="../bellman_ford.mlw"
loclnum="80" loccnumb="8" loccnume="31"
sum="23fb64f5e5dd1b6dbd03d1f091879b05"
sum="8e4b82cd5090e85145d9346e4051efde"
proved="true"
expanded="true"
shape="ainfix =V0ainfix ++V3aConsV2ainfix ++V4aConsV2V5EOainfix =V0ainfix ++V6aConsV1V7EIainfix &gt;=alengthV0acardinalaverticesIapathasV0V1F">
......@@ -157,7 +157,7 @@
name="simple_path"
locfile="../bellman_ford.mlw"
loclnum="87" loccnumb="8" loccnume="19"
sum="a3c5122f1aaf999a3e09f307916627e4"
sum="71bc032f94c55b343930ca7aeee76a83"
proved="true"
expanded="true"
shape="ainfix &lt;alengthV2acardinalaverticesAapathasV2V0EIapathasV1V0F">
......@@ -175,7 +175,7 @@
name="key_lemma_1"
locfile="../bellman_ford.mlw"
loclnum="108" loccnumb="8" loccnume="19"
sum="70b203d2fb9a7d1caed9a15d173c6ee9"
sum="2d203ec9b998dd9591fa20311e8d88fd"
proved="true"
expanded="true"
shape="anegative_cycleV2EIainfix &lt;apath_weightV3V0V1AapathasV3V0EIainfix &gt;=apath_weightV4V0V1Iainfix &lt;alengthV4acardinalaverticesIapathasV4V0FF">
......@@ -186,7 +186,7 @@
edited="bf_Graph_key_lemma_1_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.95"/>
<result status="valid" time="3.78"/>
</proof>
</goal>
</theory>
......@@ -200,7 +200,7 @@
name="key_lemma_2"
locfile="../bellman_ford.mlw"
loclnum="172" loccnumb="8" loccnume="19"
sum="54f1a885649f0bed3927a75b8ea9b234"
sum="43720d4d68f48c2f07cf8db7ce7e6d1b"
proved="true"
expanded="true"
shape="Nanegative_cycleV1FIainv2V0aedgesIainv1V0acardinalaverticesaemptyF">
......@@ -211,7 +211,7 @@
edited="bf_WP_BellmanFord_key_lemma_2_1.v"
obsolete="false"
archived="false">
<result status="valid" time="20.81"/>
<result status="valid" time="23.91"/>
</proof>
</goal>
<goal
......@@ -219,7 +219,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="VC for relax"
sum="c8aca1da4f4de0d9216d3c5171abaf0b"
sum="b6b7bc4fd7482b212739620cec9e96aa"
proved="true"
expanded="true"
shape="iainv1V0V3aaddaTuple2V1V2V4ainv1V5V3aaddaTuple2V1V2V4Iainfix =V5asetV0V2CaInfiniteaInfiniteaFiniteainfix +V6aweightV1V2aFiniteVagetV0V1FCfaInfiniteCtaInfiniteainfix &lt;ainfix +V7aweightV1V2V8aFiniteVagetV0V2aFiniteVagetV0V1Iainv1V0V3V4ANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix &lt;=c1V3F">
......@@ -234,7 +234,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="1. postcondition"
sum="f58b8f56169155e93b18ccbc45fab278"
sum="5aa79747991b7109d3529327506c967e"
proved="true"
expanded="true"
shape="postconditionainv1V5V3aaddaTuple2V1V2V4Iainfix =V5asetV0V2CaInfiniteaInfiniteaFiniteainfix +V6aweightV1V2aFiniteVagetV0V1FICfaInfiniteCtaInfiniteainfix &lt;ainfix +V7aweightV1V2V8aFiniteVagetV0V2aFiniteVagetV0V1Iainv1V0V3V4ANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix &lt;=c1V3F">
......@@ -249,7 +249,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="1. postcondition"
sum="64e386e4036b488e35e60cf823b9a6c5"
sum="fb85dab7993070fb50c78026a8459d6f"
proved="true"
expanded="true"
shape="postconditionCainfix &gt;=ainfix +apath_weightV9V8aweightV8V6V7IamemaTuple2V8V6aaddaTuple2V1V2V4Iainfix &lt;alengthV9V3IapathasV9V8FAainfix &gt;=apath_weightV10V6V7Iainfix &lt;alengthV10V3IapathasV10V6FAainfix =apath_weightV11V6V7AapathasV11V6EaFiniteVainfix &gt;=alengthV13V3IapathasV13V12FIamemaTuple2V12V6aaddaTuple2V1V2V4FAainfix &gt;=alengthV14V3IapathasV14V6FaInfiniteamixfix []V5V6IamemV6averticesFIainfix =V5asetV0V2CaInfiniteaInfiniteaFiniteainfix +V15aweightV1V2aFiniteVagetV0V1FICfaInfiniteCtaInfiniteainfix &lt;ainfix +V16aweightV1V2V17aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV21V20aweightV20V18V19IamemaTuple2V20V18V4Iainfix &lt;alengthV21V3IapathasV21V20FAainfix &gt;=apath_weightV22V18V19Iainfix &lt;alengthV22V3IapathasV22V18FAainfix =apath_weightV23V18V19AapathasV23V18EaFiniteVainfix &gt;=alengthV25V3IapathasV25V24FIamemaTuple2V24V18V4FAainfix &gt;=alengthV26V3IapathasV26V18FaInfiniteamixfix []V0V18IamemV18averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -264,7 +264,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="1. postcondition"
sum="6eb78775de868eb95601e7b18f6773b7"
sum="00e010bc1ed55f7540173ea75fd600c4"
proved="true"
expanded="true"
shape="postconditionCainfix =apath_weightV8V6V7AapathasV8V6EaFiniteVtaInfiniteamixfix []V5V6IamemV6averticesFIainfix =V5asetV0V2CaInfiniteaInfiniteaFiniteainfix +V9aweightV1V2aFiniteVagetV0V1FICfaInfiniteCtaInfiniteainfix &lt;ainfix +V10aweightV1V2V11aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV15V14aweightV14V12V13IamemaTuple2V14V12V4Iainfix &lt;alengthV15V3IapathasV15V14FAainfix &gt;=apath_weightV16V12V13Iainfix &lt;alengthV16V3IapathasV16V12FAainfix =apath_weightV17V12V13AapathasV17V12EaFiniteVainfix &gt;=alengthV19V3IapathasV19V18FIamemaTuple2V18V12V4FAainfix &gt;=alengthV20V3IapathasV20V12FaInfiniteamixfix []V0V12IamemV12averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -277,7 +277,7 @@
edited="bf_WP_BellmanFord_WP_parameter_relax_7.v"
obsolete="false"
archived="false">
<result status="valid" time="1.80"/>
<result status="valid" time="2.15"/>
</proof>
</goal>
<goal
......@@ -285,7 +285,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="2. postcondition"
sum="07eba022f7a4038d7b4c32e2e7479489"
sum="5bdb126bdf163351d2e7da44717c3633"
proved="true"
expanded="true"
shape="postconditionCainfix &gt;=apath_weightV8V6V7Iainfix &lt;alengthV8V3IapathasV8V6FaFiniteVtaInfiniteamixfix []V5V6IamemV6averticesFIainfix =V5asetV0V2CaInfiniteaInfiniteaFiniteainfix +V9aweightV1V2aFiniteVagetV0V1FICfaInfiniteCtaInfiniteainfix &lt;ainfix +V10aweightV1V2V11aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV15V14aweightV14V12V13IamemaTuple2V14V12V4Iainfix &lt;alengthV15V3IapathasV15V14FAainfix &gt;=apath_weightV16V12V13Iainfix &lt;alengthV16V3IapathasV16V12FAainfix =apath_weightV17V12V13AapathasV17V12EaFiniteVainfix &gt;=alengthV19V3IapathasV19V18FIamemaTuple2V18V12V4FAainfix &gt;=alengthV20V3IapathasV20V12FaInfiniteamixfix []V0V12IamemV12averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -305,7 +305,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="3. postcondition"
sum="c9aff1b7364c86e4babf309ba2a2eb33"
sum="3b723418ef93190422276747a6719d72"
proved="true"
expanded="true"
shape="postconditionCainfix &gt;=ainfix +apath_weightV9V8aweightV8V6V7IamemaTuple2V8V6aaddaTuple2V1V2V4Iainfix &lt;alengthV9V3IapathasV9V8FaFiniteVtaInfiniteamixfix []V5V6IamemV6averticesFIainfix =V5asetV0V2CaInfiniteaInfiniteaFiniteainfix +V10aweightV1V2aFiniteVagetV0V1FICfaInfiniteCtaInfiniteainfix &lt;ainfix +V11aweightV1V2V12aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV16V15aweightV15V13V14IamemaTuple2V15V13V4Iainfix &lt;alengthV16V3IapathasV16V15FAainfix &gt;=apath_weightV17V13V14Iainfix &lt;alengthV17V3IapathasV17V13FAainfix =apath_weightV18V13V14AapathasV18V13EaFiniteVainfix &gt;=alengthV20V3IapathasV20V19FIamemaTuple2V19V13V4FAainfix &gt;=alengthV21V3IapathasV21V13FaInfiniteamixfix []V0V13IamemV13averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -325,7 +325,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="4. postcondition"
sum="4775c28ed8801f8e66408f7179b5bc23"
sum="cdf25077caeef3975e4a373ccec05f50"
proved="true"
expanded="true"
shape="postconditionCtaFiniteVainfix &gt;=alengthV8V3IapathasV8V6FaInfiniteamixfix []V5V6IamemV6averticesFIainfix =V5asetV0V2CaInfiniteaInfiniteaFiniteainfix +V9aweightV1V2aFiniteVagetV0V1FICfaInfiniteCtaInfiniteainfix &lt;ainfix +V10aweightV1V2V11aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV15V14aweightV14V12V13IamemaTuple2V14V12V4Iainfix &lt;alengthV15V3IapathasV15V14FAainfix &gt;=apath_weightV16V12V13Iainfix &lt;alengthV16V3IapathasV16V12FAainfix =apath_weightV17V12V13AapathasV17V12EaFiniteVainfix &gt;=alengthV19V3IapathasV19V18FIamemaTuple2V18V12V4FAainfix &gt;=alengthV20V3IapathasV20V12FaInfiniteamixfix []V0V12IamemV12averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -353,7 +353,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="5. postcondition"
sum="b02d89ffd039efaf14541bc672bf8759"
sum="ec19da139f9b32c2f0266d6e2a0d1f3b"
proved="true"
expanded="true"
shape="postconditionCtaFiniteVainfix &gt;=alengthV9V3IapathasV9V8FIamemaTuple2V8V6aaddaTuple2V1V2V4FaInfiniteamixfix []V5V6IamemV6averticesFIainfix =V5asetV0V2CaInfiniteaInfiniteaFiniteainfix +V10aweightV1V2aFiniteVagetV0V1FICfaInfiniteCtaInfiniteainfix &lt;ainfix +V11aweightV1V2V12aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV16V15aweightV15V13V14IamemaTuple2V15V13V4Iainfix &lt;alengthV16V3IapathasV16V15FAainfix &gt;=apath_weightV17V13V14Iainfix &lt;alengthV17V3IapathasV17V13FAainfix =apath_weightV18V13V14AapathasV18V13EaFiniteVainfix &gt;=alengthV20V3IapathasV20V19FIamemaTuple2V19V13V4FAainfix &gt;=alengthV21V3IapathasV21V13FaInfiniteamixfix []V0V13IamemV13averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -377,7 +377,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="2. postcondition"
sum="1aaf28f53b9bd30d8a05804c76b6e4c1"
sum="49e5511e4833c4a788f096deab9c11d0"
proved="true"
expanded="true"
shape="postconditionainv1V0V3aaddaTuple2V1V2V4INCfaInfiniteCtaInfiniteainfix &lt;ainfix +V5aweightV1V2V6aFiniteVagetV0V2aFiniteVagetV0V1Iainv1V0V3V4ANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix &lt;=c1V3F">
......@@ -392,7 +392,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="1. postcondition"
sum="a4d65d8285a3f1dd9abb0fd12114be97"
sum="e2a51009f338daf3cd2fbbddf285439e"
proved="true"
expanded="true"
shape="postconditionCainfix &gt;=ainfix +apath_weightV8V7aweightV7V5V6IamemaTuple2V7V5aaddaTuple2V1V2V4Iainfix &lt;alengthV8V3IapathasV8V7FAainfix &gt;=apath_weightV9V5V6Iainfix &lt;alengthV9V3IapathasV9V5FAainfix =apath_weightV10V5V6AapathasV10V5EaFiniteVainfix &gt;=alengthV12V3IapathasV12V11FIamemaTuple2V11V5aaddaTuple2V1V2V4FAainfix &gt;=alengthV13V3IapathasV13V5FaInfiniteamixfix []V0V5IamemV5averticesFINCfaInfiniteCtaInfiniteainfix &lt;ainfix +V14aweightV1V2V15aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV19V18aweightV18V16V17IamemaTuple2V18V16V4Iainfix &lt;alengthV19V3IapathasV19V18FAainfix &gt;=apath_weightV20V16V17Iainfix &lt;alengthV20V3IapathasV20V16FAainfix =apath_weightV21V16V17AapathasV21V16EaFiniteVainfix &gt;=alengthV23V3IapathasV23V22FIamemaTuple2V22V16V4FAainfix &gt;=alengthV24V3IapathasV24V16FaInfiniteamixfix []V0V16IamemV16averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -407,7 +407,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="1. postcondition"
sum="52bd9c45bc0a38db27e2d36001e9c223"
sum="122f5b6d51663df2345d9125f1418c31"
proved="true"
expanded="true"
shape="postconditionCainfix =apath_weightV7V5V6AapathasV7V5EaFiniteVtaInfiniteamixfix []V0V5IamemV5averticesFINCfaInfiniteCtaInfiniteainfix &lt;ainfix +V8aweightV1V2V9aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV13V12aweightV12V10V11IamemaTuple2V12V10V4Iainfix &lt;alengthV13V3IapathasV13V12FAainfix &gt;=apath_weightV14V10V11Iainfix &lt;alengthV14V3IapathasV14V10FAainfix =apath_weightV15V10V11AapathasV15V10EaFiniteVainfix &gt;=alengthV17V3IapathasV17V16FIamemaTuple2V16V10V4FAainfix &gt;=alengthV18V3IapathasV18V10FaInfiniteamixfix []V0V10IamemV10averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -435,7 +435,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="2. postcondition"
sum="22115b6544626bb9dc865c464b5b2365"
sum="81cb23c5ad77898b68accc2978bfdf1f"
proved="true"
expanded="true"
shape="postconditionCainfix &gt;=apath_weightV7V5V6Iainfix &lt;alengthV7V3IapathasV7V5FaFiniteVtaInfiniteamixfix []V0V5IamemV5averticesFINCfaInfiniteCtaInfiniteainfix &lt;ainfix +V8aweightV1V2V9aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV13V12aweightV12V10V11IamemaTuple2V12V10V4Iainfix &lt;alengthV13V3IapathasV13V12FAainfix &gt;=apath_weightV14V10V11Iainfix &lt;alengthV14V3IapathasV14V10FAainfix =apath_weightV15V10V11AapathasV15V10EaFiniteVainfix &gt;=alengthV17V3IapathasV17V16FIamemaTuple2V16V10V4FAainfix &gt;=alengthV18V3IapathasV18V10FaInfiniteamixfix []V0V10IamemV10averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -463,7 +463,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="3. postcondition"
sum="9ae2d4ab8c6d72ae93250b300dc10625"
sum="57ec36e66b9c6b9bf13c57a01d9cc4d0"
proved="true"
expanded="true"
shape="postconditionCainfix &gt;=ainfix +apath_weightV8V7aweightV7V5V6IamemaTuple2V7V5aaddaTuple2V1V2V4Iainfix &lt;alengthV8V3IapathasV8V7FaFiniteVtaInfiniteamixfix []V0V5IamemV5averticesFINCfaInfiniteCtaInfiniteainfix &lt;ainfix +V9aweightV1V2V10aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV14V13aweightV13V11V12IamemaTuple2V13V11V4Iainfix &lt;alengthV14V3IapathasV14V13FAainfix &gt;=apath_weightV15V11V12Iainfix &lt;alengthV15V3IapathasV15V11FAainfix =apath_weightV16V11V12AapathasV16V11EaFiniteVainfix &gt;=alengthV18V3IapathasV18V17FIamemaTuple2V17V11V4FAainfix &gt;=alengthV19V3IapathasV19V11FaInfiniteamixfix []V0V11IamemV11averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -483,7 +483,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="4. postcondition"
sum="42160ecc702231843209e3026f29145d"
sum="8ee77922beb02dd0371d7f229cfe8311"
proved="true"
expanded="true"
shape="postconditionCtaFiniteVainfix &gt;=alengthV7V3IapathasV7V5FaInfiniteamixfix []V0V5IamemV5averticesFINCfaInfiniteCtaInfiniteainfix &lt;ainfix +V8aweightV1V2V9aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV13V12aweightV12V10V11IamemaTuple2V12V10V4Iainfix &lt;alengthV13V3IapathasV13V12FAainfix &gt;=apath_weightV14V10V11Iainfix &lt;alengthV14V3IapathasV14V10FAainfix =apath_weightV15V10V11AapathasV15V10EaFiniteVainfix &gt;=alengthV17V3IapathasV17V16FIamemaTuple2V16V10V4FAainfix &gt;=alengthV18V3IapathasV18V10FaInfiniteamixfix []V0V10IamemV10averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -511,7 +511,7 @@
locfile="../bellman_ford.mlw"
loclnum="176" loccnumb="6" loccnume="11"
expl="5. postcondition"
sum="ea312b18d9faee458b08450a5a2057ed"
sum="6b95048997a5ba089d3278937cb868aa"
proved="true"
expanded="true"
shape="postconditionCtaFiniteVainfix &gt;=alengthV8V3IapathasV8V7FIamemaTuple2V7V5aaddaTuple2V1V2V4FaInfiniteamixfix []V0V5IamemV5averticesFINCfaInfiniteCtaInfiniteainfix &lt;ainfix +V9aweightV1V2V10aFiniteVagetV0V2aFiniteVagetV0V1ICainfix &gt;=ainfix +apath_weightV14V13aweightV13V11V12IamemaTuple2V13V11V4Iainfix &lt;alengthV14V3IapathasV14V13FAainfix &gt;=apath_weightV15V11V12Iainfix &lt;alengthV15V3IapathasV15V11FAainfix =apath_weightV16V11V12AapathasV16V11EaFiniteVainfix &gt;=alengthV18V3IapathasV18V17FIamemaTuple2V17V11V4FAainfix &gt;=alengthV19V3IapathasV19V11FaInfiniteamixfix []V0V11IamemV11averticesFANamemaTuple2V1V2V4AamemaTuple2V1V2aedgesAainfix =c1V3Oainfix &lt;c1V3F">
......@@ -537,7 +537,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="VC for bellman_ford"
sum="79e74ec33675b4a62e83522699829be5"
sum="ca35870721a2ba9714dc00a3c1f262f2"
proved="true"
expanded="true"
shape="iCainfix &gt;=apath_weightV7V5V6IapathasV7V5FAainfix =apath_weightV8V5V6AapathasV8V5EaFiniteVNapathasV9V5FaInfiniteagetV1V5IamemV5averticesFAainv2V1aedgesiainfix &lt;acardinalV10acardinalV3Aainfix &lt;=c0acardinalV3Aainv2V1adiffaedgesV10AasubsetV10aedgesanegative_cycleV14ECfaInfiniteCtaInfiniteainfix &lt;ainfix +V15aweightV11V12V16aFiniteVagetV1V12aFiniteVagetV1V11Iainfix =V10aremoveV13V3AamemV13V3LaTuple2V11V12FFANais_emptyV3Nainfix =V4aTrueIais_emptyV3qainfix =V4aTrueFIainv2V1adiffaedgesV3AasubsetV3aedgesFAainv2V1adiffaedgesV2AasubsetV2aedgesIainfix =V2aedgesFAainv1V1acardinalaverticesaemptyIainv1V1ainfix +V0c1aemptyAiainv1V20ainfix +V17c1aemptyAainv1V20V17aedgesainfix &lt;acardinalV23acardinalV19Aainfix &lt;=c0acardinalV19Aainv1V27V17adiffaedgesV23AasubsetV23aedgesIainv1V27V17aaddaTuple2V24V25V22FAainv1V20V17V22ANamemaTuple2V24V25V22AamemaTuple2V24V25aedgesAainfix &lt;=c1V17Iainfix =V23aremoveV26V19AamemV26V19LaTuple2V24V25FFANais_emptyV19LadiffaedgesV19Nainfix =V21aTrueIais_emptyV19qainfix =V21aTrueFIainv1V20V17adiffaedgesV19AasubsetV19aedgesFAainv1V1V17adiffaedgesV18AasubsetV18aedgesIainfix =V18aedgesFIainv1V1V17aemptyIainfix &lt;=V17V0Aainfix &lt;=c1V17FFAainv1ainitialize_single_sourceasc1aemptyIainfix &lt;=c1V0AiCainfix &gt;=apath_weightV33V31V32IapathasV33V31FAainfix =apath_weightV34V31V32AapathasV34V31EaFiniteVNapathasV35V31FaInfiniteagetainitialize_single_sourceasV31IamemV31averticesFAainv2ainitialize_single_sourceasaedgesiainfix &lt;acardinalV36acardinalV29Aainfix &lt;=c0acardinalV29Aainv2ainitialize_single_sourceasadiffaedgesV36AasubsetV36aedgesanegative_cycleV40ECfaInfiniteCtaInfiniteainfix &lt;ainfix +V41aweightV37V38V42aFiniteVagetainitialize_single_sourceasV38aFiniteVagetainitialize_single_sourceasV37Iainfix =V36aremoveV39V29AamemV39V29LaTuple2V37V38FFANais_emptyV29Nainfix =V30aTrueIais_emptyV29qainfix =V30aTrueFIainv2ainitialize_single_sourceasadiffaedgesV29AasubsetV29aedgesFAainv2ainitialize_single_sourceasadiffaedgesV28AasubsetV28aedgesIainfix =V28aedgesFAainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -552,7 +552,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. assertion"
sum="6b6dd5ed7cd6a31ed36a9c9405608c13"
sum="8a77850786db4a94afe57b1fee1e8018"
proved="true"
expanded="true"
shape="assertionainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -567,7 +567,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. assertion"
sum="d428e7c34d1d79e69819a06e821dec33"
sum="6ce8cd8e191c98bef346f8caf83463b6"
proved="true"
expanded="true"
shape="assertionCainfix &gt;=ainfix +apath_weightV4V3aweightV3V1V2IamemaTuple2V3V1aemptyIainfix &lt;alengthV4acardinalaverticesIapathasV4V3FAainfix &gt;=apath_weightV5V1V2Iainfix &lt;alengthV5acardinalaverticesIapathasV5V1FAainfix =apath_weightV6V1V2AapathasV6V1EaFiniteVainfix &gt;=alengthV8acardinalaverticesIapathasV8V7FIamemaTuple2V7V1aemptyFAainfix &gt;=alengthV9acardinalaverticesIapathasV9V1FaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix &lt;V0c1Lainfix -acardinalaverticesc1">
......@@ -582,7 +582,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. assertion"
sum="0dbb678b252337649b2d13f5a32a31c1"
sum="6fc50ccadf4e02efac91f00a10a4f0f7"
proved="true"
expanded="true"
shape="assertionCainfix =apath_weightV3V1V2AapathasV3V1EaFiniteVtaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix &lt;V0c1Lainfix -acardinalaverticesc1">
......@@ -618,7 +618,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="2. assertion"
sum="b6d760ae193e7f14d322b58b9666bcaa"
sum="79c7161fb5c477e62c2a1e9dd9124784"
proved="true"
expanded="true"
shape="assertionCainfix &gt;=apath_weightV3V1V2Iainfix &lt;alengthV3acardinalaverticesIapathasV3V1FaFiniteVtaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix &lt;V0c1Lainfix -acardinalaverticesc1">
......@@ -638,7 +638,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="3. assertion"
sum="22532fbc33d07c2aee3e3922c219c8ae"
sum="d38bb084b1fb4b18577ead8e3f95a962"
proved="true"
expanded="true"
shape="assertionCainfix &gt;=ainfix +apath_weightV4V3aweightV3V1V2IamemaTuple2V3V1aemptyIainfix &lt;alengthV4acardinalaverticesIapathasV4V3FaFiniteVtaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix &lt;V0c1Lainfix -acardinalaverticesc1">
......@@ -658,7 +658,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="4. assertion"
sum="15663698dcaaf6496d86b60d332ee042"
sum="642f35b2c9d6b312114799a19988e0d2"
proved="true"
expanded="true"
shape="assertionCtaFiniteVainfix &gt;=alengthV3acardinalaverticesIapathasV3V1FaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix &lt;V0c1Lainfix -acardinalaverticesc1">
......@@ -678,7 +678,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="5. assertion"
sum="e24b460ab56510b4696ff13cd8899212"
sum="5f78f0fac46ed7ff542eabac6956cbaa"
proved="true"
expanded="true"
shape="assertionCtaFiniteVainfix &gt;=alengthV4acardinalaverticesIapathasV4V3FIamemaTuple2V3V1aemptyFaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix &lt;V0c1Lainfix -acardinalaverticesc1">
......@@ -702,7 +702,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="2. loop invariant init"
sum="e91752eeb0a518b8a75f91cad1d16125"
sum="e59c1c75968a62d9d58e9a4a82d93d71"
proved="true"
expanded="true"
shape="loop invariant initainv2ainitialize_single_sourceasadiffaedgesV1AasubsetV1aedgesIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -722,7 +722,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="3. precondition"
sum="c8fd3caa88fd1529cb6c2838684f02f5"
sum="8507ab626047c9b76e2aa0513551329a"
proved="true"
expanded="true"
shape="preconditionNais_emptyV2INainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -742,7 +742,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="4. exceptional postcondition"
sum="88bbf6e2f8d6f3ab20e76bccd18882a0"
sum="18f0e6f12c4089f7cfa2a54ad1b2c6a4"
proved="true"
expanded="true"
shape="exceptional postconditionanegative_cycleV8EICfaInfiniteCtaInfiniteainfix &lt;ainfix +V9aweightV5V6V10aFiniteVagetainitialize_single_sourceasV6aFiniteVagetainitialize_single_sourceasV5Iainfix =V4aremoveV7V2AamemV7V2LaTuple2V5V6FFINais_emptyV2INainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -755,7 +755,7 @@
edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_20.v"
obsolete="false"
archived="false">
<result status="valid" time="2.28"/>
<result status="valid" time="2.82"/>
</proof>
</goal>
<goal
......@@ -763,7 +763,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="5. loop invariant preservation"
sum="692839b752af559f0d7f772f44ff3688"
sum="e7497bb98978b35101c9944b639199c9"
proved="true"
expanded="true"
shape="loop invariant preservationainv2ainitialize_single_sourceasadiffaedgesV4AasubsetV4aedgesINCfaInfiniteCtaInfiniteainfix &lt;ainfix +V8aweightV5V6V9aFiniteVagetainitialize_single_sourceasV6aFiniteVagetainitialize_single_sourceasV5Iainfix =V4aremoveV7V2AamemV7V2LaTuple2V5V6FFINais_emptyV2INainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -775,7 +775,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.26"/>
<result status="valid" time="4.03"/>
</proof>
</goal>
<goal
......@@ -783,7 +783,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="6. loop variant decrease"
sum="8549bf167fedebba6cd14539a5432d6e"
sum="b82b686bfa1c0650fb98bcbbf65bd350"
proved="true"
expanded="true"
shape="loop variant decreaseainfix &lt;acardinalV4acardinalV2Aainfix &lt;=c0acardinalV2INCfaInfiniteCtaInfiniteainfix &lt;ainfix +V8aweightV5V6V9aFiniteVagetainitialize_single_sourceasV6aFiniteVagetainitialize_single_sourceasV5Iainfix =V4aremoveV7V2AamemV7V2LaTuple2V5V6FFINais_emptyV2INainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -803,7 +803,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="7. assertion"
sum="72a69d0e156f922f476c6337d9756d64"
sum="459c47ab3c62bf9b2f5c6b68f98cf985"
proved="true"
expanded="true"
shape="assertionainv2ainitialize_single_sourceasaedgesINNainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -823,7 +823,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="8. postcondition"
sum="829f70ec8b1ee2a0c8d20c6717c36877"
sum="58fc2d1f54af38fbc9f497300edc2c1d"
proved="true"
expanded="true"
shape="postconditionCainfix &gt;=apath_weightV6V4V5IapathasV6V4FAainfix =apath_weightV7V4V5AapathasV7V4EaFiniteVNapathasV8V4FaInfiniteagetainitialize_single_sourceasV4IamemV4averticesFIainv2ainitialize_single_sourceasaedgesINNainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -838,7 +838,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. postcondition"
sum="dbe3bdfaff72e7ad2ce55be099bb4cc2"
sum="96691ad18a97642f021db7baf5e45411"
proved="true"
expanded="true"
shape="postconditionCainfix =apath_weightV6V4V5AapathasV6V4EaFiniteVtaInfiniteagetainitialize_single_sourceasV4IamemV4averticesFIainv2ainitialize_single_sourceasaedgesINNainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -874,7 +874,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="2. postcondition"
sum="c336a993420836ae7e3742d26bbde224"
sum="cebe924702622aaaba7ed1b80d09c4f5"
proved="true"
expanded="true"
shape="postconditionCainfix &gt;=apath_weightV6V4V5IapathasV6V4FaFiniteVtaInfiniteagetainitialize_single_sourceasV4IamemV4averticesFIainv2ainitialize_single_sourceasaedgesINNainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -894,7 +894,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="3. postcondition"
sum="70d02503f0b76046394e74e889e58200"
sum="f237f3ac1d45f1eb943f222f3c09b6b2"
proved="true"
expanded="true"
shape="postconditionCtaFiniteVNapathasV6V4FaInfiniteagetainitialize_single_sourceasV4IamemV4averticesFIainv2ainitialize_single_sourceasaedgesINNainfix =V3aTrueIais_emptyV2qainfix =V3aTrueFIainv2ainitialize_single_sourceasadiffaedgesV2AasubsetV2aedgesFIainfix =V1aedgesFIainv1ainitialize_single_sourceasacardinalaverticesaemptyIainfix &gt;c1V0Lainfix -acardinalaverticesc1">
......@@ -906,7 +906,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="8.28"/>
<result status="valid" time="9.34"/>
</proof>
<proof
prover="1"
......@@ -932,7 +932,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="9. loop invariant init"
sum="da25a4f5db721103c1b1ddc999b7a7bb"
sum="0845e64e5a2aa37cc8f1a82364a81e95"
proved="true"
expanded="true"
shape="loop invariant initainv1ainitialize_single_sourceasc1aemptyIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -947,7 +947,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. loop invariant init"
sum="3f57f1acddd9fa8b456cd823291838a2"
sum="1b98fdfff2146662bf8e02fb32818339"
proved="true"
expanded="true"
shape="loop invariant initCainfix &gt;=ainfix +apath_weightV4V3aweightV3V1V2IamemaTuple2V3V1aemptyIainfix &lt;alengthV4c1IapathasV4V3FAainfix &gt;=apath_weightV5V1V2Iainfix &lt;alengthV5c1IapathasV5V1FAainfix =apath_weightV6V1V2AapathasV6V1EaFiniteVainfix &gt;=alengthV8c1IapathasV8V7FIamemaTuple2V7V1aemptyFAainfix &gt;=alengthV9c1IapathasV9V1FaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -962,7 +962,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. loop invariant init"
sum="d44668f0f73e4ddae89b635f639a7169"
sum="d298a9ed0c16a6badd4f72f1f2f461d1"
proved="true"
expanded="true"
shape="loop invariant initCainfix =apath_weightV3V1V2AapathasV3V1EaFiniteVtaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -990,7 +990,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="2. loop invariant init"
sum="9ba024bc1593ca8b9a5672049a9656d9"
sum="29b9da2896386e715b5dbf1ee71eb2e1"
proved="true"
expanded="true"
shape="loop invariant initCainfix &gt;=apath_weightV3V1V2Iainfix &lt;alengthV3c1IapathasV3V1FaFiniteVtaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1010,7 +1010,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="3. loop invariant init"
sum="15ed0e058cc500d33bf7ddfbd9ad4116"
sum="a55ed21ebc5ac33ca5d1a38871818730"
proved="true"
expanded="true"
shape="loop invariant initCainfix &gt;=ainfix +apath_weightV4V3aweightV3V1V2IamemaTuple2V3V1aemptyIainfix &lt;alengthV4c1IapathasV4V3FaFiniteVtaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1030,7 +1030,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="4. loop invariant init"
sum="4c911a23654c09e02bcb7dd0d428c71b"
sum="71c3dcb35b51e51df1a20d6ffc93ccd8"
proved="true"
expanded="true"
shape="loop invariant initCtaFiniteVainfix &gt;=alengthV3c1IapathasV3V1FaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1050,7 +1050,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="5. loop invariant init"
sum="91487de17f1b43f546427ef27d6e8d70"
sum="d543a1f1b0333f73ad46decf6c38445a"
proved="true"
expanded="true"
shape="loop invariant initCtaFiniteVainfix &gt;=alengthV4c1IapathasV4V3FIamemaTuple2V3V1aemptyFaInfiniteamixfix []ainitialize_single_sourceasV1IamemV1averticesFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1074,7 +1074,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="10. loop invariant init"
sum="e6bd0453289f2dbb3fcf749aeddfac04"
sum="9866ed4de11d507123685d392d9de699"
proved="true"
expanded="true"
shape="loop invariant initainv1V1V2adiffaedgesV3AasubsetV3aedgesIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1089,7 +1089,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1."
sum="f9cb0747031d59713234e1281017c826"
sum="702158ef135b99f8e5519cea99508a5a"
proved="true"
expanded="true"
shape="asubsetV3aedgesIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1109,7 +1109,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="2."
sum="a64b9c8d061bf4df1130a1826b0ecbcf"
sum="58b7e2013f0d9891f9bee5aad1c21457"
proved="true"
expanded="true"
shape="ainv1V1V2adiffaedgesV3Iainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1131,7 +1131,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="11. precondition"
sum="b9b2eb4c674e7fcfed33db727fc2d014"
sum="7043b4351d8f64a1b1b691fd8a627235"
proved="true"
expanded="true"
shape="preconditionNais_emptyV4LadiffaedgesV4INainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1151,7 +1151,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="12. precondition"
sum="692bae9dc7287f0c1f5a68f35bde0818"
sum="1e87115be628bd90c706cfbfd9afa9ee"
proved="true"
expanded="true"
shape="preconditionNamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix &lt;=c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINais_emptyV4LadiffaedgesV4INainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1171,7 +1171,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="13. precondition"
sum="aa788f5d1a5155eecb3e17485d896239"
sum="db2bfa659a918b13f873173d70bbc424"
proved="true"
expanded="true"
shape="preconditionainv1V5V2V7Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINais_emptyV4LadiffaedgesV4INainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1191,7 +1191,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="14. loop invariant preservation"
sum="b5a857cc1ce115e5487badd431f51139"
sum="4214b77234f0b844620b0f38f0e05647"
proved="true"
expanded="true"
shape="loop invariant preservationainv1V12V2adiffaedgesV8AasubsetV8aedgesIainv1V12V2aaddaTuple2V9V10V7FIainv1V5V2V7ANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix &lt;=c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINais_emptyV4LadiffaedgesV4INainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1206,7 +1206,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1."
sum="1604ba88ff0e50bea7635297ad6e2890"
sum="8dd6f29b6225f50e34e3bf9bff9400a6"
proved="true"
expanded="true"
shape="asubsetV8aedgesIainv1V12V2aaddaTuple2V9V10V7FIainv1V5V2V7ANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix &lt;=c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINais_emptyV4LadiffaedgesV4INainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1226,7 +1226,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="2."
sum="effb301c80d52086603a235b176c77ae"
sum="e69ac961b128975ecf2f22ccfa0d931f"
proved="true"
expanded="true"
shape="ainv1V12V2adiffaedgesV8Iainv1V12V2aaddaTuple2V9V10V7FIainv1V5V2V7ANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix &lt;=c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINais_emptyV4LadiffaedgesV4INainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1241,7 +1241,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1."
sum="5679429441edaf12aa38a5ffd3c0ec41"
sum="586462471476bdaab0b7c903aa8630ee"
proved="true"
expanded="true"
shape="Cainfix &gt;=ainfix +apath_weightV16V15aweightV15V13V14IamemaTuple2V15V13adiffaedgesV8Iainfix &lt;alengthV16V2IapathasV16V15FAainfix &gt;=apath_weightV17V13V14Iainfix &lt;alengthV17V2IapathasV17V13FAainfix =apath_weightV18V13V14AapathasV18V13EaFiniteVainfix &gt;=alengthV20V2IapathasV20V19FIamemaTuple2V19V13adiffaedgesV8FAainfix &gt;=alengthV21V2IapathasV21V13FaInfiniteamixfix []V12V13IamemV13averticesFICainfix &gt;=ainfix +apath_weightV25V24aweightV24V22V23IamemaTuple2V24V22aaddaTuple2V9V10V7Iainfix &lt;alengthV25V2IapathasV25V24FAainfix &gt;=apath_weightV26V22V23Iainfix &lt;alengthV26V2IapathasV26V22FAainfix =apath_weightV27V22V23AapathasV27V22EaFiniteVainfix &gt;=alengthV29V2IapathasV29V28FIamemaTuple2V28V22aaddaTuple2V9V10V7FAainfix &gt;=alengthV30V2IapathasV30V22FaInfiniteamixfix []V12V22IamemV22averticesFFICainfix &gt;=ainfix +apath_weightV34V33aweightV33V31V32IamemaTuple2V33V31V7Iainfix &lt;alengthV34V2IapathasV34V33FAainfix &gt;=apath_weightV35V31V32Iainfix &lt;alengthV35V2IapathasV35V31FAainfix =apath_weightV36V31V32AapathasV36V31EaFiniteVainfix &gt;=alengthV38V2IapathasV38V37FIamemaTuple2V37V31V7FAainfix &gt;=alengthV39V2IapathasV39V31FaInfiniteamixfix []V5V31IamemV31averticesFANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix =c1V2Oainfix &lt;c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINNamemV40V4FLadiffaedgesV4INainfix =V6aTrueINamemV41V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV45V44aweightV44V42V43IamemaTuple2V44V42adiffaedgesV4Iainfix &lt;alengthV45V2IapathasV45V44FAainfix &gt;=apath_weightV46V42V43Iainfix &lt;alengthV46V2IapathasV46V42FAainfix =apath_weightV47V42V43AapathasV47V42EaFiniteVainfix &gt;=alengthV49V2IapathasV49V48FIamemaTuple2V48V42adiffaedgesV4FAainfix &gt;=alengthV50V2IapathasV50V42FaInfiniteamixfix []V5V42IamemV42averticesFAamemV51aedgesIamemV51V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV55V54aweightV54V52V53IamemaTuple2V54V52aemptyIainfix &lt;alengthV55V2IapathasV55V54FAainfix &gt;=apath_weightV56V52V53Iainfix &lt;alengthV56V2IapathasV56V52FAainfix =apath_weightV57V52V53AapathasV57V52EaFiniteVainfix &gt;=alengthV59V2IapathasV59V58FIamemaTuple2V58V52aemptyFAainfix &gt;=alengthV60V2IapathasV60V52FaInfiniteamixfix []V1V52IamemV52averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1256,7 +1256,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1."
sum="3476885811ffdc6470f9206bec28fe31"
sum="c293bede2ae341100457c31eff1a43d3"
proved="true"
expanded="true"
shape="Cainfix =apath_weightV15V13V14AapathasV15V13EaFiniteVtaInfiniteamixfix []V12V13IamemV13averticesFICainfix &gt;=ainfix +apath_weightV19V18aweightV18V16V17IamemaTuple2V18V16aaddaTuple2V9V10V7Iainfix &lt;alengthV19V2IapathasV19V18FAainfix &gt;=apath_weightV20V16V17Iainfix &lt;alengthV20V2IapathasV20V16FAainfix =apath_weightV21V16V17AapathasV21V16EaFiniteVainfix &gt;=alengthV23V2IapathasV23V22FIamemaTuple2V22V16aaddaTuple2V9V10V7FAainfix &gt;=alengthV24V2IapathasV24V16FaInfiniteamixfix []V12V16IamemV16averticesFFICainfix &gt;=ainfix +apath_weightV28V27aweightV27V25V26IamemaTuple2V27V25V7Iainfix &lt;alengthV28V2IapathasV28V27FAainfix &gt;=apath_weightV29V25V26Iainfix &lt;alengthV29V2IapathasV29V25FAainfix =apath_weightV30V25V26AapathasV30V25EaFiniteVainfix &gt;=alengthV32V2IapathasV32V31FIamemaTuple2V31V25V7FAainfix &gt;=alengthV33V2IapathasV33V25FaInfiniteamixfix []V5V25IamemV25averticesFANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix =c1V2Oainfix &lt;c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINNamemV34V4FLadiffaedgesV4INainfix =V6aTrueINamemV35V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV39V38aweightV38V36V37IamemaTuple2V38V36adiffaedgesV4Iainfix &lt;alengthV39V2IapathasV39V38FAainfix &gt;=apath_weightV40V36V37Iainfix &lt;alengthV40V2IapathasV40V36FAainfix =apath_weightV41V36V37AapathasV41V36EaFiniteVainfix &gt;=alengthV43V2IapathasV43V42FIamemaTuple2V42V36adiffaedgesV4FAainfix &gt;=alengthV44V2IapathasV44V36FaInfiniteamixfix []V5V36IamemV36averticesFAamemV45aedgesIamemV45V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV49V48aweightV48V46V47IamemaTuple2V48V46aemptyIainfix &lt;alengthV49V2IapathasV49V48FAainfix &gt;=apath_weightV50V46V47Iainfix &lt;alengthV50V2IapathasV50V46FAainfix =apath_weightV51V46V47AapathasV51V46EaFiniteVainfix &gt;=alengthV53V2IapathasV53V52FIamemaTuple2V52V46aemptyFAainfix &gt;=alengthV54V2IapathasV54V46FaInfiniteamixfix []V1V46IamemV46averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1284,7 +1284,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="2."
sum="cceb8f0b6815acecbf6ded80db59d678"
sum="73f59e15519e8c8a7b6aa3fb10720077"
proved="true"
expanded="true"
shape="Cainfix &gt;=apath_weightV15V13V14Iainfix &lt;alengthV15V2IapathasV15V13FaFiniteVtaInfiniteamixfix []V12V13IamemV13averticesFICainfix &gt;=ainfix +apath_weightV19V18aweightV18V16V17IamemaTuple2V18V16aaddaTuple2V9V10V7Iainfix &lt;alengthV19V2IapathasV19V18FAainfix &gt;=apath_weightV20V16V17Iainfix &lt;alengthV20V2IapathasV20V16FAainfix =apath_weightV21V16V17AapathasV21V16EaFiniteVainfix &gt;=alengthV23V2IapathasV23V22FIamemaTuple2V22V16aaddaTuple2V9V10V7FAainfix &gt;=alengthV24V2IapathasV24V16FaInfiniteamixfix []V12V16IamemV16averticesFFICainfix &gt;=ainfix +apath_weightV28V27aweightV27V25V26IamemaTuple2V27V25V7Iainfix &lt;alengthV28V2IapathasV28V27FAainfix &gt;=apath_weightV29V25V26Iainfix &lt;alengthV29V2IapathasV29V25FAainfix =apath_weightV30V25V26AapathasV30V25EaFiniteVainfix &gt;=alengthV32V2IapathasV32V31FIamemaTuple2V31V25V7FAainfix &gt;=alengthV33V2IapathasV33V25FaInfiniteamixfix []V5V25IamemV25averticesFANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix =c1V2Oainfix &lt;c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINNamemV34V4FLadiffaedgesV4INainfix =V6aTrueINamemV35V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV39V38aweightV38V36V37IamemaTuple2V38V36adiffaedgesV4Iainfix &lt;alengthV39V2IapathasV39V38FAainfix &gt;=apath_weightV40V36V37Iainfix &lt;alengthV40V2IapathasV40V36FAainfix =apath_weightV41V36V37AapathasV41V36EaFiniteVainfix &gt;=alengthV43V2IapathasV43V42FIamemaTuple2V42V36adiffaedgesV4FAainfix &gt;=alengthV44V2IapathasV44V36FaInfiniteamixfix []V5V36IamemV36averticesFAamemV45aedgesIamemV45V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV49V48aweightV48V46V47IamemaTuple2V48V46aemptyIainfix &lt;alengthV49V2IapathasV49V48FAainfix &gt;=apath_weightV50V46V47Iainfix &lt;alengthV50V2IapathasV50V46FAainfix =apath_weightV51V46V47AapathasV51V46EaFiniteVainfix &gt;=alengthV53V2IapathasV53V52FIamemaTuple2V52V46aemptyFAainfix &gt;=alengthV54V2IapathasV54V46FaInfiniteamixfix []V1V46IamemV46averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1296,7 +1296,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.42"/>
<result status="valid" time="1.96"/>
</proof>
<proof
prover="1"
......@@ -1312,7 +1312,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="3."
sum="255369a1a731aeb4e324201a4f63fdd8"
sum="adf05b17be39130d56be319c2e239af2"
proved="true"
expanded="true"
shape="Cainfix &gt;=ainfix +apath_weightV16V15aweightV15V13V14IamemaTuple2V15V13adiffaedgesV8Iainfix &lt;alengthV16V2IapathasV16V15FaFiniteVtaInfiniteamixfix []V12V13IamemV13averticesFICainfix &gt;=ainfix +apath_weightV20V19aweightV19V17V18IamemaTuple2V19V17aaddaTuple2V9V10V7Iainfix &lt;alengthV20V2IapathasV20V19FAainfix &gt;=apath_weightV21V17V18Iainfix &lt;alengthV21V2IapathasV21V17FAainfix =apath_weightV22V17V18AapathasV22V17EaFiniteVainfix &gt;=alengthV24V2IapathasV24V23FIamemaTuple2V23V17aaddaTuple2V9V10V7FAainfix &gt;=alengthV25V2IapathasV25V17FaInfiniteamixfix []V12V17IamemV17averticesFFICainfix &gt;=ainfix +apath_weightV29V28aweightV28V26V27IamemaTuple2V28V26V7Iainfix &lt;alengthV29V2IapathasV29V28FAainfix &gt;=apath_weightV30V26V27Iainfix &lt;alengthV30V2IapathasV30V26FAainfix =apath_weightV31V26V27AapathasV31V26EaFiniteVainfix &gt;=alengthV33V2IapathasV33V32FIamemaTuple2V32V26V7FAainfix &gt;=alengthV34V2IapathasV34V26FaInfiniteamixfix []V5V26IamemV26averticesFANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix =c1V2Oainfix &lt;c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINNamemV35V4FLadiffaedgesV4INainfix =V6aTrueINamemV36V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV40V39aweightV39V37V38IamemaTuple2V39V37adiffaedgesV4Iainfix &lt;alengthV40V2IapathasV40V39FAainfix &gt;=apath_weightV41V37V38Iainfix &lt;alengthV41V2IapathasV41V37FAainfix =apath_weightV42V37V38AapathasV42V37EaFiniteVainfix &gt;=alengthV44V2IapathasV44V43FIamemaTuple2V43V37adiffaedgesV4FAainfix &gt;=alengthV45V2IapathasV45V37FaInfiniteamixfix []V5V37IamemV37averticesFAamemV46aedgesIamemV46V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV50V49aweightV49V47V48IamemaTuple2V49V47aemptyIainfix &lt;alengthV50V2IapathasV50V49FAainfix &gt;=apath_weightV51V47V48Iainfix &lt;alengthV51V2IapathasV51V47FAainfix =apath_weightV52V47V48AapathasV52V47EaFiniteVainfix &gt;=alengthV54V2IapathasV54V53FIamemaTuple2V53V47aemptyFAainfix &gt;=alengthV55V2IapathasV55V47FaInfiniteamixfix []V1V47IamemV47averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1324,7 +1324,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="17.04"/>
<result status="valid" time="19.52"/>
</proof>
</goal>
<goal
......@@ -1332,7 +1332,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="4."
sum="f77672e773edaf84e8302a04d633901d"
sum="0a7640b8683819a9ed4279c37e51437a"
proved="true"
expanded="true"
shape="CtaFiniteVainfix &gt;=alengthV15V2IapathasV15V13FaInfiniteamixfix []V12V13IamemV13averticesFICainfix &gt;=ainfix +apath_weightV19V18aweightV18V16V17IamemaTuple2V18V16aaddaTuple2V9V10V7Iainfix &lt;alengthV19V2IapathasV19V18FAainfix &gt;=apath_weightV20V16V17Iainfix &lt;alengthV20V2IapathasV20V16FAainfix =apath_weightV21V16V17AapathasV21V16EaFiniteVainfix &gt;=alengthV23V2IapathasV23V22FIamemaTuple2V22V16aaddaTuple2V9V10V7FAainfix &gt;=alengthV24V2IapathasV24V16FaInfiniteamixfix []V12V16IamemV16averticesFFICainfix &gt;=ainfix +apath_weightV28V27aweightV27V25V26IamemaTuple2V27V25V7Iainfix &lt;alengthV28V2IapathasV28V27FAainfix &gt;=apath_weightV29V25V26Iainfix &lt;alengthV29V2IapathasV29V25FAainfix =apath_weightV30V25V26AapathasV30V25EaFiniteVainfix &gt;=alengthV32V2IapathasV32V31FIamemaTuple2V31V25V7FAainfix &gt;=alengthV33V2IapathasV33V25FaInfiniteamixfix []V5V25IamemV25averticesFANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix =c1V2Oainfix &lt;c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINNamemV34V4FLadiffaedgesV4INainfix =V6aTrueINamemV35V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV39V38aweightV38V36V37IamemaTuple2V38V36adiffaedgesV4Iainfix &lt;alengthV39V2IapathasV39V38FAainfix &gt;=apath_weightV40V36V37Iainfix &lt;alengthV40V2IapathasV40V36FAainfix =apath_weightV41V36V37AapathasV41V36EaFiniteVainfix &gt;=alengthV43V2IapathasV43V42FIamemaTuple2V42V36adiffaedgesV4FAainfix &gt;=alengthV44V2IapathasV44V36FaInfiniteamixfix []V5V36IamemV36averticesFAamemV45aedgesIamemV45V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV49V48aweightV48V46V47IamemaTuple2V48V46aemptyIainfix &lt;alengthV49V2IapathasV49V48FAainfix &gt;=apath_weightV50V46V47Iainfix &lt;alengthV50V2IapathasV50V46FAainfix =apath_weightV51V46V47AapathasV51V46EaFiniteVainfix &gt;=alengthV53V2IapathasV53V52FIamemaTuple2V52V46aemptyFAainfix &gt;=alengthV54V2IapathasV54V46FaInfiniteamixfix []V1V46IamemV46averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1360,7 +1360,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="5."
sum="2ecfb941bf7644d79bb49c98834216aa"
sum="192069a32da2f2e3327f7b6635c59b2b"
proved="true"
expanded="true"
shape="CtaFiniteVainfix &gt;=alengthV16V2IapathasV16V15FIamemaTuple2V15V13adiffaedgesV8FaInfiniteamixfix []V12V13IamemV13averticesFICainfix &gt;=ainfix +apath_weightV20V19aweightV19V17V18IamemaTuple2V19V17aaddaTuple2V9V10V7Iainfix &lt;alengthV20V2IapathasV20V19FAainfix &gt;=apath_weightV21V17V18Iainfix &lt;alengthV21V2IapathasV21V17FAainfix =apath_weightV22V17V18AapathasV22V17EaFiniteVainfix &gt;=alengthV24V2IapathasV24V23FIamemaTuple2V23V17aaddaTuple2V9V10V7FAainfix &gt;=alengthV25V2IapathasV25V17FaInfiniteamixfix []V12V17IamemV17averticesFFICainfix &gt;=ainfix +apath_weightV29V28aweightV28V26V27IamemaTuple2V28V26V7Iainfix &lt;alengthV29V2IapathasV29V28FAainfix &gt;=apath_weightV30V26V27Iainfix &lt;alengthV30V2IapathasV30V26FAainfix =apath_weightV31V26V27AapathasV31V26EaFiniteVainfix &gt;=alengthV33V2IapathasV33V32FIamemaTuple2V32V26V7FAainfix &gt;=alengthV34V2IapathasV34V26FaInfiniteamixfix []V5V26IamemV26averticesFANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix =c1V2Oainfix &lt;c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINNamemV35V4FLadiffaedgesV4INainfix =V6aTrueINamemV36V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV40V39aweightV39V37V38IamemaTuple2V39V37adiffaedgesV4Iainfix &lt;alengthV40V2IapathasV40V39FAainfix &gt;=apath_weightV41V37V38Iainfix &lt;alengthV41V2IapathasV41V37FAainfix =apath_weightV42V37V38AapathasV42V37EaFiniteVainfix &gt;=alengthV44V2IapathasV44V43FIamemaTuple2V43V37adiffaedgesV4FAainfix &gt;=alengthV45V2IapathasV45V37FaInfiniteamixfix []V5V37IamemV37averticesFAamemV46aedgesIamemV46V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV50V49aweightV49V47V48IamemaTuple2V49V47aemptyIainfix &lt;alengthV50V2IapathasV50V49FAainfix &gt;=apath_weightV51V47V48Iainfix &lt;alengthV51V2IapathasV51V47FAainfix =apath_weightV52V47V48AapathasV52V47EaFiniteVainfix &gt;=alengthV54V2IapathasV54V53FIamemaTuple2V53V47aemptyFAainfix &gt;=alengthV55V2IapathasV55V47FaInfiniteamixfix []V1V47IamemV47averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1394,7 +1394,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="15. loop variant decrease"
sum="2d77d42e409fbdf5e3f3842d8bb185b3"
sum="dc7ad5337510293404548ff06a5c3c55"
proved="true"
expanded="true"
shape="loop variant decreaseainfix &lt;acardinalV8acardinalV4Aainfix &lt;=c0acardinalV4Iainv1V12V2aaddaTuple2V9V10V7FIainv1V5V2V7ANamemaTuple2V9V10V7AamemaTuple2V9V10aedgesAainfix &lt;=c1V2Iainfix =V8aremoveV11V4AamemV11V4LaTuple2V9V10FFINais_emptyV4LadiffaedgesV4INainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1414,7 +1414,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="16. assertion"
sum="4af81a0c677ee019bc1dc5583e2c9f2a"
sum="40d4bb4a2ef21ef8b4960de7fc367202"
proved="true"
expanded="true"
shape="assertionainv1V5V2aedgesINNainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1429,7 +1429,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. assertion"
sum="ff3c89e08abaa368aa8fa689e451a327"
sum="76c558ab7e3c522c1cb4b981193e7d8b"
proved="true"
expanded="true"
shape="assertionCainfix &gt;=ainfix +apath_weightV10V9aweightV9V7V8IamemaTuple2V9V7aedgesIainfix &lt;alengthV10V2IapathasV10V9FAainfix &gt;=apath_weightV11V7V8Iainfix &lt;alengthV11V2IapathasV11V7FAainfix =apath_weightV12V7V8AapathasV12V7EaFiniteVainfix &gt;=alengthV14V2IapathasV14V13FIamemaTuple2V13V7aedgesFAainfix &gt;=alengthV15V2IapathasV15V7FaInfiniteamixfix []V5V7IamemV7averticesFINNainfix =V6aTrueINamemV16V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV20V19aweightV19V17V18IamemaTuple2V19V17adiffaedgesV4Iainfix &lt;alengthV20V2IapathasV20V19FAainfix &gt;=apath_weightV21V17V18Iainfix &lt;alengthV21V2IapathasV21V17FAainfix =apath_weightV22V17V18AapathasV22V17EaFiniteVainfix &gt;=alengthV24V2IapathasV24V23FIamemaTuple2V23V17adiffaedgesV4FAainfix &gt;=alengthV25V2IapathasV25V17FaInfiniteamixfix []V5V17IamemV17averticesFAamemV26aedgesIamemV26V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV30V29aweightV29V27V28IamemaTuple2V29V27aemptyIainfix &lt;alengthV30V2IapathasV30V29FAainfix &gt;=apath_weightV31V27V28Iainfix &lt;alengthV31V2IapathasV31V27FAainfix =apath_weightV32V27V28AapathasV32V27EaFiniteVainfix &gt;=alengthV34V2IapathasV34V33FIamemaTuple2V33V27aemptyFAainfix &gt;=alengthV35V2IapathasV35V27FaInfiniteamixfix []V1V27IamemV27averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1441,7 +1441,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="4.68"/>
<result status="valid" time="5.33"/>
</proof>
</goal>
</transf>
......@@ -1451,7 +1451,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="17. loop invariant preservation"
sum="29ca61034aa0f18f959b3ee960edbc05"
sum="39e7e66e946bb9e75cb135c896baa255"
proved="true"
expanded="true"
shape="loop invariant preservationainv1V5ainfix +V2c1aemptyIainv1V5V2aedgesINNainfix =V6aTrueIais_emptyV4qainfix =V6aTrueFIainv1V5V2adiffaedgesV4AasubsetV4aedgesFIainfix =V3aedgesFIainv1V1V2aemptyIainfix &lt;=V2V0Aainfix &lt;=c1V2FFIainfix &lt;=c1V0Lainfix -acardinalaverticesc1">
......@@ -1466,7 +1466,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. loop invariant preservation"
sum="bf8db9dd443d1a5ff5575e19737ad3f6"
sum="13859cc5a69e2e66342f6b66e90d08b6"
proved="true"
expanded="true"
shape="loop invariant preservationCainfix &gt;=ainfix +apath_weightV10V9aweightV9V7V8IamemaTuple2V9V7aemptyIainfix &lt;alengthV10ainfix +V2c1IapathasV10V9FAainfix &gt;=apath_weightV11V7V8Iainfix &lt;alengthV11ainfix +V2c1IapathasV11V7FAainfix =apath_weightV12V7V8AapathasV12V7EaFiniteVainfix &gt;=alengthV14ainfix +V2c1IapathasV14V13FIamemaTuple2V13V7aemptyFAainfix &gt;=alengthV15ainfix +V2c1IapathasV15V7FaInfiniteamixfix []V5V7IamemV7averticesFICainfix &gt;=ainfix +apath_weightV19V18aweightV18V16V17IamemaTuple2V18V16aedgesIainfix &lt;alengthV19V2IapathasV19V18FAainfix &gt;=apath_weightV20V16V17Iainfix &lt;alengthV20V2IapathasV20V16FAainfix =apath_weightV21V16V17AapathasV21V16EaFiniteVainfix &gt;=alengthV23V2IapathasV23V22FIamemaTuple2V22V16aedgesFAainfix &gt;=alengthV24V2IapathasV24V16FaInfiniteamixfix []V5V16IamemV16averticesFINNainfix =V6aTrueINamemV25V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV29V28aweightV28V26V27IamemaTuple2V28V26adiffaedgesV4Iainfix &lt;alengthV29V2IapathasV29V28FAainfix &gt;=apath_weightV30V26V27Iainfix &lt;alengthV30V2IapathasV30V26FAainfix =apath_weightV31V26V27AapathasV31V26EaFiniteVainfix &gt;=alengthV33V2IapathasV33V32FIamemaTuple2V32V26adiffaedgesV4FAainfix &gt;=alengthV34V2IapathasV34V26FaInfiniteamixfix []V5V26IamemV26averticesFAamemV35aedgesIamemV35V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV39V38aweightV38V36V37IamemaTuple2V38V36aemptyIainfix &lt;alengthV39V2IapathasV39V38FAainfix &gt;=apath_weightV40V36V37Iainfix &lt;alengthV40V2IapathasV40V36FAainfix =apath_weightV41V36V37AapathasV41V36EaFiniteVainfix &gt;=alengthV43V2IapathasV43V42FIamemaTuple2V42V36aemptyFAainfix &gt;=alengthV44V2IapathasV44V36FaInfiniteamixfix []V1V36IamemV36averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1481,7 +1481,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="1. loop invariant preservation"
sum="6684b9b91afe1c21001cdca9eaa2c51d"
sum="c017302b2c5a279c2f75607fbc62b445"
proved="true"
expanded="true"
shape="loop invariant preservationCainfix =apath_weightV9V7V8AapathasV9V7EaFiniteVtaInfiniteamixfix []V5V7IamemV7averticesFICainfix &gt;=ainfix +apath_weightV13V12aweightV12V10V11IamemaTuple2V12V10aedgesIainfix &lt;alengthV13V2IapathasV13V12FAainfix &gt;=apath_weightV14V10V11Iainfix &lt;alengthV14V2IapathasV14V10FAainfix =apath_weightV15V10V11AapathasV15V10EaFiniteVainfix &gt;=alengthV17V2IapathasV17V16FIamemaTuple2V16V10aedgesFAainfix &gt;=alengthV18V2IapathasV18V10FaInfiniteamixfix []V5V10IamemV10averticesFINNainfix =V6aTrueINamemV19V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV23V22aweightV22V20V21IamemaTuple2V22V20adiffaedgesV4Iainfix &lt;alengthV23V2IapathasV23V22FAainfix &gt;=apath_weightV24V20V21Iainfix &lt;alengthV24V2IapathasV24V20FAainfix =apath_weightV25V20V21AapathasV25V20EaFiniteVainfix &gt;=alengthV27V2IapathasV27V26FIamemaTuple2V26V20adiffaedgesV4FAainfix &gt;=alengthV28V2IapathasV28V20FaInfiniteamixfix []V5V20IamemV20averticesFAamemV29aedgesIamemV29V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV33V32aweightV32V30V31IamemaTuple2V32V30aemptyIainfix &lt;alengthV33V2IapathasV33V32FAainfix &gt;=apath_weightV34V30V31Iainfix &lt;alengthV34V2IapathasV34V30FAainfix =apath_weightV35V30V31AapathasV35V30EaFiniteVainfix &gt;=alengthV37V2IapathasV37V36FIamemaTuple2V36V30aemptyFAainfix &gt;=alengthV38V2IapathasV38V30FaInfiniteamixfix []V1V30IamemV30averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1501,7 +1501,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="2. loop invariant preservation"
sum="95b86554a5252094d8ba14c81cba4b08"
sum="fd2327b37f4f2f4d42630f1d3449f747"
proved="true"
expanded="true"
shape="loop invariant preservationCainfix &gt;=apath_weightV9V7V8Iainfix &lt;alengthV9ainfix +V2c1IapathasV9V7FaFiniteVtaInfiniteamixfix []V5V7IamemV7averticesFICainfix &gt;=ainfix +apath_weightV13V12aweightV12V10V11IamemaTuple2V12V10aedgesIainfix &lt;alengthV13V2IapathasV13V12FAainfix &gt;=apath_weightV14V10V11Iainfix &lt;alengthV14V2IapathasV14V10FAainfix =apath_weightV15V10V11AapathasV15V10EaFiniteVainfix &gt;=alengthV17V2IapathasV17V16FIamemaTuple2V16V10aedgesFAainfix &gt;=alengthV18V2IapathasV18V10FaInfiniteamixfix []V5V10IamemV10averticesFINNainfix =V6aTrueINamemV19V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV23V22aweightV22V20V21IamemaTuple2V22V20adiffaedgesV4Iainfix &lt;alengthV23V2IapathasV23V22FAainfix &gt;=apath_weightV24V20V21Iainfix &lt;alengthV24V2IapathasV24V20FAainfix =apath_weightV25V20V21AapathasV25V20EaFiniteVainfix &gt;=alengthV27V2IapathasV27V26FIamemaTuple2V26V20adiffaedgesV4FAainfix &gt;=alengthV28V2IapathasV28V20FaInfiniteamixfix []V5V20IamemV20averticesFAamemV29aedgesIamemV29V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV33V32aweightV32V30V31IamemaTuple2V32V30aemptyIainfix &lt;alengthV33V2IapathasV33V32FAainfix &gt;=apath_weightV34V30V31Iainfix &lt;alengthV34V2IapathasV34V30FAainfix =apath_weightV35V30V31AapathasV35V30EaFiniteVainfix &gt;=alengthV37V2IapathasV37V36FIamemaTuple2V36V30aemptyFAainfix &gt;=alengthV38V2IapathasV38V30FaInfiniteamixfix []V1V30IamemV30averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1522,7 +1522,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="3. loop invariant preservation"
sum="c646a33e5575dab2fdfa8abaf91d56b3"
sum="374f1eebba87563b10316cb6d63153dc"
proved="true"
expanded="true"
shape="loop invariant preservationCainfix &gt;=ainfix +apath_weightV10V9aweightV9V7V8IamemaTuple2V9V7aemptyIainfix &lt;alengthV10ainfix +V2c1IapathasV10V9FaFiniteVtaInfiniteamixfix []V5V7IamemV7averticesFICainfix &gt;=ainfix +apath_weightV14V13aweightV13V11V12IamemaTuple2V13V11aedgesIainfix &lt;alengthV14V2IapathasV14V13FAainfix &gt;=apath_weightV15V11V12Iainfix &lt;alengthV15V2IapathasV15V11FAainfix =apath_weightV16V11V12AapathasV16V11EaFiniteVainfix &gt;=alengthV18V2IapathasV18V17FIamemaTuple2V17V11aedgesFAainfix &gt;=alengthV19V2IapathasV19V11FaInfiniteamixfix []V5V11IamemV11averticesFINNainfix =V6aTrueINamemV20V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV24V23aweightV23V21V22IamemaTuple2V23V21adiffaedgesV4Iainfix &lt;alengthV24V2IapathasV24V23FAainfix &gt;=apath_weightV25V21V22Iainfix &lt;alengthV25V2IapathasV25V21FAainfix =apath_weightV26V21V22AapathasV26V21EaFiniteVainfix &gt;=alengthV28V2IapathasV28V27FIamemaTuple2V27V21adiffaedgesV4FAainfix &gt;=alengthV29V2IapathasV29V21FaInfiniteamixfix []V5V21IamemV21averticesFAamemV30aedgesIamemV30V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV34V33aweightV33V31V32IamemaTuple2V33V31aemptyIainfix &lt;alengthV34V2IapathasV34V33FAainfix &gt;=apath_weightV35V31V32Iainfix &lt;alengthV35V2IapathasV35V31FAainfix =apath_weightV36V31V32AapathasV36V31EaFiniteVainfix &gt;=alengthV38V2IapathasV38V37FIamemaTuple2V37V31aemptyFAainfix &gt;=alengthV39V2IapathasV39V31FaInfiniteamixfix []V1V31IamemV31averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1558,7 +1558,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="4. loop invariant preservation"
sum="b0869bb09074e922e1ceb3ab0482fca9"
sum="5a1a8f322264afc65e51a875f685703f"
proved="true"
expanded="true"
shape="loop invariant preservationCtaFiniteVainfix &gt;=alengthV9ainfix +V2c1IapathasV9V7FaInfiniteamixfix []V5V7IamemV7averticesFICainfix &gt;=ainfix +apath_weightV13V12aweightV12V10V11IamemaTuple2V12V10aedgesIainfix &lt;alengthV13V2IapathasV13V12FAainfix &gt;=apath_weightV14V10V11Iainfix &lt;alengthV14V2IapathasV14V10FAainfix =apath_weightV15V10V11AapathasV15V10EaFiniteVainfix &gt;=alengthV17V2IapathasV17V16FIamemaTuple2V16V10aedgesFAainfix &gt;=alengthV18V2IapathasV18V10FaInfiniteamixfix []V5V10IamemV10averticesFINNainfix =V6aTrueINamemV19V4Fqainfix =V6aTrueFICainfix &gt;=ainfix +apath_weightV23V22aweightV22V20V21IamemaTuple2V22V20adiffaedgesV4Iainfix &lt;alengthV23V2IapathasV23V22FAainfix &gt;=apath_weightV24V20V21Iainfix &lt;alengthV24V2IapathasV24V20FAainfix =apath_weightV25V20V21AapathasV25V20EaFiniteVainfix &gt;=alengthV27V2IapathasV27V26FIamemaTuple2V26V20adiffaedgesV4FAainfix &gt;=alengthV28V2IapathasV28V20FaInfiniteamixfix []V5V20IamemV20averticesFAamemV29aedgesIamemV29V4FFIainfix =V3aedgesFICainfix &gt;=ainfix +apath_weightV33V32aweightV32V30V31IamemaTuple2V32V30aemptyIainfix &lt;alengthV33V2IapathasV33V32FAainfix &gt;=apath_weightV34V30V31Iainfix &lt;alengthV34V2IapathasV34V30FAainfix =apath_weightV35V30V31AapathasV35V30EaFiniteVainfix &gt;=alengthV37V2IapathasV37V36FIamemaTuple2V36V30aemptyFAainfix &gt;=alengthV38V2IapathasV38V30FaInfiniteamixfix []V1V30IamemV30averticesFIainfix =V2V0Oainfix &lt;V2V0Aainfix =c1V2Oainfix &lt;c1V2FFIainfix =c1V0Oainfix &lt;c1V0Lainfix -acardinalaverticesc1">
......@@ -1579,7 +1579,7 @@
locfile="../bellman_ford.mlw"
loclnum="186" loccnumb="6" loccnume="18"
expl="5. loop invariant preservation"