Commit 28fcb939 authored by MARCHE Claude's avatar MARCHE Claude

residuals: adding automata

parent c9dd7298
......@@ -22,10 +22,10 @@ module Residuals
end
lemma inversion_mem_star_gen :
forall c w r w' r'.
forall c w r w' r'.
w' = Cons c w /\ r' = Star r ->
mem w' r' ->
exists w1 w2. w = w1 ++ w2 /\ mem (Cons c w1) r /\ mem w2 r'
exists w1 w2. w = w1 ++ w2 /\ mem (Cons c w1) r /\ mem w2 r'
lemma inversion_mem_star :
forall c w r. mem (Cons c w) (Star r) ->
......@@ -62,16 +62,47 @@ end
module Test
type char = int
type char = int
clone import Residuals with type char = char
constant a : char = 65
constant aa : word = Cons a (Cons a Nil)
constant astar : regexp = Star (Char a)
let test_astar () = decide_mem aa astar
end
module DFA
type char
use import list.List
type word = list char
use import map.Map
(** automaton where states = 0..size-1, init state = 0 *)
type state = int
type t =
{ size : int;
is_final_state : map state bool;
transition : map (state,char) int;
}
function exec (a:t) (q:state) (w:word) : state =
match w with
| Nil -> q
| Cons c r -> let q' = a.transition[(q,c)] in exec a q' r
end
function accepts (a:t) (w:word) : bool =
a.is_final_state[exec a 0 w]
end
\ No newline at end of file
......@@ -36,22 +36,22 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="VC for accepts_epsilon"
sum="48fcc85fbe6685f00a9765d55690d1fc"
sum="74df7152cbead1333fca140341843275"
proved="true"
expanded="true"
expanded="false"
shape="CNamemaNilV0aEmptyamemaNilV0aEpsilonNamemaNilV0aCharwiamemaNilV0qainfix =V4aTrueIamemaNilV2qainfix =V4aTrueFACfaEmptyfaEpsilonfaCharwainfix =V6V2Oainfix =V5V2aAltVVainfix =V8V2Oainfix =V7V2aConcatVVainfix =V9V2aStarVV0amemaNilV0ainfix =V3aTrueIamemaNilV1qainfix =V3aTrueFACfaEmptyfaEpsilonfaCharwainfix =V11V1Oainfix =V10V1aAltVVainfix =V13V1Oainfix =V12V1aConcatVVainfix =V14V1aStarVV0aAltVViNamemaNilV0amemaNilV0qainfix =V18aTrueIamemaNilV16qainfix =V18aTrueFACfaEmptyfaEpsilonfaCharwainfix =V20V16Oainfix =V19V16aAltVVainfix =V22V16Oainfix =V21V16aConcatVVainfix =V23V16aStarVV0ainfix =V17aTrueIamemaNilV15qainfix =V17aTrueFACfaEmptyfaEpsilonfaCharwainfix =V25V15Oainfix =V24V15aAltVVainfix =V27V15Oainfix =V26V15aConcatVVainfix =V28V15aStarVV0aConcatVVamemaNilV0aStarwV0F">
<label
name="expl:VC for accepts_epsilon"/>
<transf
name="split_goal_wp"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter accepts_epsilon.1"
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="1. postcondition"
sum="0c567082071faadc8d39dd843ca262c7"
sum="5b46fdf36a6ff10b85a5278119664ee1"
proved="true"
expanded="false"
shape="postconditionCNamemaNilV0aEmptytaEpsilontaCharwtaAltVVtaConcatVVtaStarwV0F">
......@@ -71,7 +71,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="2. postcondition"
sum="60e65f54e0b08a10acb16938794ad156"
sum="5c8a34156d444b0ef47e6f0358a79dda"
proved="true"
expanded="false"
shape="postconditionCtaEmptyamemaNilV0aEpsilontaCharwtaAltVVtaConcatVVtaStarwV0F">
......@@ -91,7 +91,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="3. postcondition"
sum="5b9cd838b663393d29861fe2f23e4a55"
sum="5040da331e1f52a7ed99fabe92cfea2b"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilonNamemaNilV0aCharwtaAltVVtaConcatVVtaStarwV0F">
......@@ -111,7 +111,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="4. variant decrease"
sum="5ff8290542060e5164a0f71f8f419aa5"
sum="0a8c1443a3ee140caffa41b8dbba0bed"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharwCfaEmptyfaEpsilonfaCharwainfix =V4V1Oainfix =V3V1aAltVVainfix =V6V1Oainfix =V5V1aConcatVVainfix =V7V1aStarVV0aAltVVtaConcatVVtaStarwV0F">
......@@ -131,7 +131,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="5. postcondition"
sum="9982be8ed3531e175a55c353eedc72a0"
sum="d2dbdc9237c0fff99633ad3bfdadac20"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilontaCharwamemaNilV0Iainfix =V3aTrueIamemaNilV1qainfix =V3aTrueFaAltVVtaConcatVVtaStarwV0F">
......@@ -151,7 +151,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="6. variant decrease"
sum="27504aaf4564b78e40cbced94a36ca2d"
sum="baac14aadae8fc66b37a9f264dff92d7"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharwCfaEmptyfaEpsilonfaCharwainfix =V5V2Oainfix =V4V2aAltVVainfix =V7V2Oainfix =V6V2aConcatVVainfix =V8V2aStarVV0INainfix =V3aTrueIamemaNilV1qainfix =V3aTrueFaAltVVtaConcatVVtaStarwV0F">
......@@ -171,7 +171,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="7. postcondition"
sum="00c60d5111fd65156bb85d11a66d0d0a"
sum="d6609a77d16b41fcae4aa402dbae3018"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilontaCharwamemaNilV0qainfix =V4aTrueIamemaNilV2qainfix =V4aTrueFINainfix =V3aTrueIamemaNilV1qainfix =V3aTrueFaAltVVtaConcatVVtaStarwV0F">
......@@ -191,7 +191,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="8. variant decrease"
sum="0001d58021ddb4ac41f81a9765242dae"
sum="d7f65d0b67a475aa502dd177b27fbfd7"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharwtaAltVVCfaEmptyfaEpsilonfaCharwainfix =V6V3Oainfix =V5V3aAltVVainfix =V8V3Oainfix =V7V3aConcatVVainfix =V9V3aStarVV0aConcatVVtaStarwV0F">
......@@ -211,7 +211,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="9. variant decrease"
sum="096fc0e66dd12a08d6eaca41f8f93511"
sum="f12caa39483875e60072a3e806171107"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharwtaAltVVCfaEmptyfaEpsilonfaCharwainfix =V7V4Oainfix =V6V4aAltVVainfix =V9V4Oainfix =V8V4aConcatVVainfix =V10V4aStarVV0Iainfix =V5aTrueIamemaNilV3qainfix =V5aTrueFaConcatVVtaStarwV0F">
......@@ -231,7 +231,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="10. postcondition"
sum="64bf868780b97ec48040832d0ef7e525"
sum="1034bc50c39052a9c58d9f7471d435e6"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilontaCharwtaAltVVamemaNilV0qainfix =V6aTrueIamemaNilV4qainfix =V6aTrueFIainfix =V5aTrueIamemaNilV3qainfix =V5aTrueFaConcatVVtaStarwV0F">
......@@ -246,7 +246,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="1. postcondition"
sum="6bf428b3a0f54890888394ae5dc12173"
sum="c1930d5ce4978cb1b6e23baef50cccaf"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilontaCharwtaAltVVamemaNilV0Iainfix =V6aTrueIamemaNilV4qainfix =V6aTrueFIainfix =V5aTrueIamemaNilV3qainfix =V5aTrueFaConcatVVtaStarwV0F">
......@@ -274,7 +274,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="2. postcondition"
sum="fb515f4ed7b56c56a6d0613c266393b5"
sum="babf8cfe1338ae2f73e1fd5a2b5351c3"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilontaCharwtaAltVVainfix =V6aTrueIamemaNilV0IamemaNilV4qainfix =V6aTrueFIainfix =V5aTrueIamemaNilV3qainfix =V5aTrueFaConcatVVtaStarwV0F">
......@@ -296,7 +296,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="11. postcondition"
sum="f6f25f7d6f198c2638fd4fbf400cf661"
sum="184887d1b3b81a8d0b41eba2c44aa156"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilontaCharwtaAltVVNamemaNilV0INainfix =V5aTrueIamemaNilV3qainfix =V5aTrueFaConcatVVtaStarwV0F">
......@@ -316,7 +316,7 @@
locfile="../residual.mlw"
loclnum="12" loccnumb="10" loccnume="25"
expl="12. postcondition"
sum="b1af3bedd2c9fd43574a2cbac815033c"
sum="926de78a993a89fc163a80d218f1ed0e"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilontaCharwtaAltVVtaConcatVVamemaNilV0aStarwV0F">
......@@ -337,7 +337,7 @@
name="inversion_mem_star_gen"
locfile="../residual.mlw"
loclnum="24" loccnumb="8" loccnume="30"
sum="f072fb3bcbcbc5f0d31fd4891b37372e"
sum="9e897ff5951f54d82a83b358f6dd3bf3"
proved="true"
expanded="true"
shape="amemV6V4AamemaConsV0V5V2Aainfix =V1ainfix ++V5V6EIamemV3V4Iainfix =V4aStarV2Aainfix =V3aConsV0V1F">
......@@ -355,9 +355,9 @@
name="inversion_mem_star"
locfile="../residual.mlw"
loclnum="30" loccnumb="8" loccnume="26"
sum="f23c3a99cd07cdcb9045f8c4ee9dd4f5"
sum="aa3aeb8c647baf66d041cd09e602e1de"
proved="true"
expanded="true"
expanded="false"
shape="amemV4aStarV2AamemaConsV0V3V2Aainfix =V1ainfix ++V3V4EIamemaConsV0V1aStarV2F">
<proof
prover="0"
......@@ -373,7 +373,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="VC for residual"
sum="752fe5294fa9bae91f2b55fe6bfa68f2"
sum="e2cbf918c78af57dc49d12580f178dde"
proved="true"
expanded="true"
shape="CamemaConsV1V2V0qamemV2aEmptyFaEmptyamemaConsV1V3V0qamemV3aEmptyFaEpsilonamemaConsV1V5V0qamemV5iaEmptyaEpsilonainfix =V1V4FaCharVamemaConsV1V10V0qamemV10aAltV9V8FIamemaConsV1V11V6qamemV11V9FFACfaEmptyfaEpsilonfaCharwainfix =V13V6Oainfix =V12V6aAltVVainfix =V15V6Oainfix =V14V6aConcatVVainfix =V16V6aStarVV0IamemaConsV1V17V7qamemV17V8FFACfaEmptyfaEpsilonfaCharwainfix =V19V7Oainfix =V18V7aAltVVainfix =V21V7Oainfix =V20V7aConcatVVainfix =V22V7aStarVV0aAltVViamemaConsV1V27V0qamemV27aConcatV26V24FIamemaConsV1V28V23qamemV28V26FFACfaEmptyfaEpsilonfaCharwainfix =V30V23Oainfix =V29V23aAltVVainfix =V32V23Oainfix =V31V23aConcatVVainfix =V33V23aStarVV0amemaConsV1V36V0qamemV36aAltaConcatV35V24V34FIamemaConsV1V37V23qamemV37V35FFACfaEmptyfaEpsilonfaCharwainfix =V39V23Oainfix =V38V23aAltVVainfix =V41V23Oainfix =V40V23aConcatVVainfix =V42V23aStarVV0IamemaConsV1V43V24qamemV43V34FFACfaEmptyfaEpsilonfaCharwainfix =V45V24Oainfix =V44V24aAltVVainfix =V47V24Oainfix =V46V24aConcatVVainfix =V48V24aStarVV0ainfix =V25aTrueIamemaNilV23qainfix =V25aTrueFaConcatVVamemaConsV1V51V0qamemV51aConcatV50V0FIamemaConsV1V52V49qamemV52V50FFACfaEmptyfaEpsilonfaCharwainfix =V54V49Oainfix =V53V49aAltVVainfix =V56V49Oainfix =V55V49aConcatVVainfix =V57V49aStarVV0aStarVV0F">
......@@ -388,7 +388,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="1. postcondition"
sum="17ddf4a24eabc9002f86a438d7b45e0d"
sum="799ea04b3622c1612c3aa2e75f05d5d1"
proved="true"
expanded="false"
shape="postconditionCamemaConsV1V2V0qamemV2aEmptyFaEmptytaEpsilontaCharVtaAltVVtaConcatVVtaStarVV0F">
......@@ -416,7 +416,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="2. postcondition"
sum="6a53e1eb138d1cb3289111a40c6cf8a3"
sum="09ede6b6bfed9e469160ec13729c1250"
proved="true"
expanded="false"
shape="postconditionCtaEmptyamemaConsV1V2V0qamemV2aEmptyFaEpsilontaCharVtaAltVVtaConcatVVtaStarVV0F">
......@@ -444,7 +444,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="3. postcondition"
sum="964e4ff140e8414ef846420e38687dce"
sum="e929ca4220cdc677308a320f7c9c8796"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilonamemaConsV1V3V0qamemV3iaEmptyaEpsilonainfix =V1V2FaCharVtaAltVVtaConcatVVtaStarVV0F">
......@@ -472,7 +472,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="4. variant decrease"
sum="2197599faa3d4baef02b4243d0290cc2"
sum="f32039f1f83d97a9a195a61ebf4967ea"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharVCfaEmptyfaEpsilonfaCharwainfix =V6V4Oainfix =V5V4aAltVVainfix =V8V4Oainfix =V7V4aConcatVVainfix =V9V4aStarVV0aAltVVtaConcatVVtaStarVV0F">
......@@ -516,7 +516,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="5. variant decrease"
sum="dc7f44578ce3a7a3ab081151fa0149c6"
sum="3bd3590f9b829f5c8fa4d925b15022ef"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharVCfaEmptyfaEpsilonfaCharwainfix =V7V3Oainfix =V6V3aAltVVainfix =V9V3Oainfix =V8V3aConcatVVainfix =V10V3aStarVV0IamemaConsV1V11V4qamemV11V5FFaAltVVtaConcatVVtaStarVV0F">
......@@ -560,7 +560,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="6. postcondition"
sum="3dc976da6d8e7a1be789fffddff69988"
sum="b35831f0d18359f4341cf4c702c1e011"
proved="true"
expanded="false"
shape="postconditionCtaEmptytaEpsilontaCharVamemaConsV1V7V0qamemV7aAltV6V5FIamemaConsV1V8V3qamemV8V6FFIamemaConsV1V9V4qamemV9V5FFaAltVVtaConcatVVtaStarVV0F">
......@@ -588,7 +588,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="7. variant decrease"
sum="5d98a64f6f47b2aeddf40fd5bea5cc54"
sum="a7aa026c6e865fb5ccd9e4234c4be53a"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharVtaAltVVCfaEmptyfaEpsilonfaCharwainfix =V9V6Oainfix =V8V6aAltVVainfix =V11V6Oainfix =V10V6aConcatVVainfix =V12V6aStarVV0Iainfix =V7aTrueIamemaNilV5qainfix =V7aTrueFaConcatVVtaStarVV0F">
......@@ -632,7 +632,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="8. variant decrease"
sum="f6889b7df03846fcb355520dfb0ec87f"
sum="66b79b0845a8366a2d61b0d301a36947"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharVtaAltVVCfaEmptyfaEpsilonfaCharwainfix =V10V5Oainfix =V9V5aAltVVainfix =V12V5Oainfix =V11V5aConcatVVainfix =V13V5aStarVV0IamemaConsV1V14V6qamemV14V8FFIainfix =V7aTrueIamemaNilV5qainfix =V7aTrueFaConcatVVtaStarVV0F">
......@@ -676,9 +676,9 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="9. postcondition"
sum="3b58324d659f72ff18cc4b5ec6560ba8"
sum="fd927425a4b27cfadcb9e1409ca4c60e"
proved="true"
expanded="false"
expanded="true"
shape="postconditionCtaEmptytaEpsilontaCharVtaAltVVamemaConsV1V10V0qamemV10aAltaConcatV9V6V8FIamemaConsV1V11V5qamemV11V9FFIamemaConsV1V12V6qamemV12V8FFIainfix =V7aTrueIamemaNilV5qainfix =V7aTrueFaConcatVVtaStarVV0F">
<label
name="expl:VC for residual"/>
......@@ -697,7 +697,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="10. variant decrease"
sum="763004c4de603b377629dcd16c46a4d4"
sum="91c61f388bae65a8ebdf7f17d8532822"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharVtaAltVVCfaEmptyfaEpsilonfaCharwainfix =V9V5Oainfix =V8V5aAltVVainfix =V11V5Oainfix =V10V5aConcatVVainfix =V12V5aStarVV0INainfix =V7aTrueIamemaNilV5qainfix =V7aTrueFaConcatVVtaStarVV0F">
......@@ -741,9 +741,9 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="11. postcondition"
sum="dac274ab4786b8dad4826002c5738e9b"
sum="936fe3bf6df5d14f6dc11eb3e9300f8a"
proved="true"
expanded="false"
expanded="true"
shape="postconditionCtaEmptytaEpsilontaCharVtaAltVVamemaConsV1V9V0qamemV9aConcatV8V6FIamemaConsV1V10V5qamemV10V8FFINainfix =V7aTrueIamemaNilV5qainfix =V7aTrueFaConcatVVtaStarVV0F">
<label
name="expl:VC for residual"/>
......@@ -762,7 +762,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="12. variant decrease"
sum="57a69961a3efba6a4983c7ef19b9f360"
sum="37453e5296352028d467f6dc5480ad25"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptytaEpsilontaCharVtaAltVVtaConcatVVCfaEmptyfaEpsilonfaCharwainfix =V9V7Oainfix =V8V7aAltVVainfix =V11V7Oainfix =V10V7aConcatVVainfix =V12V7aStarVV0aStarVV0F">
......@@ -806,7 +806,7 @@
locfile="../residual.mlw"
loclnum="35" loccnumb="10" loccnume="18"
expl="13. postcondition"
sum="afb3725c00066a247666efe39d355d11"
sum="7ccd9e1da5bccb428ae146bd5f537292"
proved="true"
expanded="true"
shape="postconditionCtaEmptytaEpsilontaCharVtaAltVVtaConcatVVamemaConsV1V9V0qamemV9aConcatV8V0FIamemaConsV1V10V7qamemV10V8FFaStarVV0F">
......@@ -829,22 +829,22 @@
locfile="../residual.mlw"
loclnum="51" loccnumb="10" loccnume="20"
expl="VC for decide_mem"
sum="6865eaacca47b2cbd4c8aecbc0c4fbc1"
sum="e3af63d5aaa8e94fa71737ca6a65c667"
proved="true"
expanded="true"
expanded="false"
shape="CamemV0V1qainfix =V2aTrueIamemaNilV1qainfix =V2aTrueFaNilamemV0V1qainfix =V6aTrueIamemV4V5qainfix =V6aTrueFACfaNilainfix =V7V4aConswVV0IamemaConsV3V8V1qamemV8V5FFaConsVVV0F">
<label
name="expl:VC for decide_mem"/>
<transf
name="split_goal_wp"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter decide_mem.1"
locfile="../residual.mlw"
loclnum="51" loccnumb="10" loccnume="20"
expl="1. postcondition"
sum="c8ad3e884552de0d933883fc70144001"
sum="0f8f68e17dd7e366d5d291a59734e62b"
proved="true"
expanded="false"
shape="postconditionCamemV0V1qainfix =V2aTrueIamemaNilV1qainfix =V2aTrueFaNiltaConsVVV0F">
......@@ -864,7 +864,7 @@
locfile="../residual.mlw"
loclnum="51" loccnumb="10" loccnume="20"
expl="2. variant decrease"
sum="eab4c8847a6a1ee4284cd7ca686c787f"
sum="fce61617f50853e97acf3500df3ffd59"
proved="true"
expanded="false"
shape="variant decreaseCtaNilCfaNilainfix =V5V3aConswVV0IamemaConsV2V6V1qamemV6V4FFaConsVVV0F">
......@@ -884,7 +884,7 @@
locfile="../residual.mlw"
loclnum="51" loccnumb="10" loccnume="20"
expl="3. postcondition"
sum="e170fcb8205f1973079b7c04a7224db2"
sum="c2d2259500118507be70ea84efa96b95"
proved="true"
expanded="false"
shape="postconditionCtaNilamemV0V1qainfix =V5aTrueIamemV3V4qainfix =V5aTrueFIamemaConsV2V6V1qamemV6V4FFaConsVVV0F">
......@@ -913,18 +913,25 @@
locfile="../residual.mlw"
loclnum="75" loccnumb="6" loccnume="16"
expl="VC for test_astar"
sum="5778320b52b0388224d8d16acb66c20f"
sum="6490b4300db66621a0c599374ec74b4b"
proved="true"
expanded="true"
expanded="false"
shape="t">
<label
name="expl:VC for test_astar"/>
<transf
name="split_goal_wp"
proved="true"
expanded="true">
expanded="false">
</transf>
</goal>
</theory>
<theory
name="DFA"
locfile="../residual.mlw"
loclnum="81" loccnumb="7" loccnume="10"
verified="true"
expanded="false">
</theory>
</file>
</why3session>
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