Commit 6b553a1e authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated sessions on moloch

parent b49532a5
......@@ -2,6 +2,7 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Definition unit := unit.
Parameter qtmark : Type.
......@@ -81,6 +82,14 @@ Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a)
Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)).
Parameter k: Z.
Axiom k_positive : (0%Z < k)%Z.
Definition k_values(a:(array Z)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < (length a))%Z) -> ((0%Z <= (get1 a i))%Z /\ ((get1 a i) < k)%Z).
Definition param := ((map Z Z)* Z)%type.
Definition eq(p:((map Z Z)* Z)%type) (i:Z): Prop :=
......@@ -125,11 +134,11 @@ Axiom Full : forall (p:((map Z Z)* Z)%type) (a:Z) (b:Z), (a < b)%Z ->
((forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> (eq p n)) -> ((num_of p a
b) = (b - a)%Z)).
Axiom num_of_increasing : forall (p:((map Z Z)* Z)%type) (i:Z) (j:Z) (k:Z),
((i <= j)%Z /\ (j <= k)%Z) -> ((num_of p i j) <= (num_of p i k))%Z.
Axiom num_of_increasing : forall (p:((map Z Z)* Z)%type) (i:Z) (j:Z) (k1:Z),
((i <= j)%Z /\ (j <= k1)%Z) -> ((num_of p i j) <= (num_of p i k1))%Z.
Axiom num_of_strictly_increasing : forall (p:((map Z Z)* Z)%type) (i:Z) (j:Z)
(k:Z) (l:Z), (((i <= j)%Z /\ (j <= k)%Z) /\ (k < l)%Z) -> ((eq p k) ->
(k1:Z) (l:Z), (((i <= j)%Z /\ (j <= k1)%Z) /\ (k1 < l)%Z) -> ((eq p k1) ->
((num_of p i j) < (num_of p i l))%Z).
Axiom num_of_change_any : forall (p1:((map Z Z)* Z)%type) (p2:((map Z Z)*
......@@ -186,12 +195,12 @@ Axiom Full1 : forall (p:((map Z Z)* Z)%type) (a:Z) (b:Z), (a < b)%Z ->
((forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> (lt p n)) -> ((num_of1 p a
b) = (b - a)%Z)).
Axiom num_of_increasing1 : forall (p:((map Z Z)* Z)%type) (i:Z) (j:Z) (k:Z),
((i <= j)%Z /\ (j <= k)%Z) -> ((num_of1 p i j) <= (num_of1 p i k))%Z.
Axiom num_of_increasing1 : forall (p:((map Z Z)* Z)%type) (i:Z) (j:Z) (k1:Z),
((i <= j)%Z /\ (j <= k1)%Z) -> ((num_of1 p i j) <= (num_of1 p i k1))%Z.
Axiom num_of_strictly_increasing1 : forall (p:((map Z Z)* Z)%type) (i:Z)
(j:Z) (k:Z) (l:Z), (((i <= j)%Z /\ (j <= k)%Z) /\ (k < l)%Z) -> ((lt p
k) -> ((num_of1 p i j) < (num_of1 p i l))%Z).
(j:Z) (k1:Z) (l:Z), (((i <= j)%Z /\ (j <= k1)%Z) /\ (k1 < l)%Z) -> ((lt p
k1) -> ((num_of1 p i j) < (num_of1 p i l))%Z).
Axiom num_of_change_any1 : forall (p1:((map Z Z)* Z)%type) (p2:((map Z Z)*
Z)%type) (a:Z) (b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> ((lt p1
......@@ -205,14 +214,6 @@ Axiom num_of_change_some1 : forall (p1:((map Z Z)* Z)%type) (p2:((map Z Z)*
Definition numlt(a:(array Z)) (v:Z) (i:Z) (j:Z): Z := (num_of1 ((elts a), v)
i j).
Parameter k: Z.
Axiom k_positive : (0%Z < k)%Z.
Definition k_values(a:(array Z)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < (length a))%Z) -> ((0%Z <= (get1 a i))%Z /\ ((get1 a i) < k)%Z).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
......
......@@ -3,6 +3,9 @@
Require Import ZArith.
Require Import Rbase.
Require Import ZOdiv.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Definition unit := unit.
Parameter qtmark : Type.
......@@ -29,9 +32,6 @@ Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.
Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
(x <= y)%Z).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
......
......@@ -3,6 +3,9 @@
Require Import ZArith.
Require Import Rbase.
Require Import ZOdiv.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Definition unit := unit.
Parameter qtmark : Type.
......@@ -29,9 +32,6 @@ Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.
Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
(x <= y)%Z).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
......
......@@ -3,6 +3,9 @@
Require Import ZArith.
Require Import Rbase.
Require Import ZOdiv.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Definition unit := unit.
Parameter qtmark : Type.
......@@ -29,9 +32,6 @@ Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.
Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
(x <= y)%Z).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
......@@ -142,6 +142,10 @@ Unset Implicit Arguments.
Axiom mem_occurs_first : forall (a:Type) (b:Type), forall (k:a) (v:b)
(l:(list (a* b)%type)), (occurs_first k v l) -> (mem (k, v) l).
Axiom cons_occurs_first : forall (a:Type) (b:Type), forall (k1:a) (v1:b)
(l:(list (a* b)%type)), (occurs_first k1 v1 l) -> forall (k:a) (v:b),
(~ (k = k1)) -> (occurs_first k1 v1 (Cons (k, v) l)).
Definition valid (a:Type) (b:Type)(h:(t a b)): Prop :=
(0%Z < (length (data h)))%Z /\ ((forall (k:a) (v:b), ((get2 h
k) = (Some v)) <-> (occurs_first k v (get1 (data h) (idx h k)))) /\
......
......@@ -3,6 +3,9 @@
Require Import ZArith.
Require Import Rbase.
Require Import ZOdiv.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Definition unit := unit.
Parameter qtmark : Type.
......@@ -29,9 +32,6 @@ Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.
Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
(x <= y)%Z).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
......
......@@ -13,7 +13,7 @@
<prover
id="2"
name="Coq"
version="8.2pl2"/>
version="8.3pl3"/>
<prover
id="3"
name="Z3"
......@@ -46,10 +46,10 @@
<proof
prover="2"
timelimit="10"
edited="hash_tables_WP_HashTableImpl_mem_occurs_first_1.v"
edited="hash_tables_WP_HashTableImpl_mem_occurs_first_2.v"
obsolete="false"
archived="false">
<result status="valid" time="0.77"/>
<result status="valid" time="0.59"/>
</proof>
</goal>
<goal
......@@ -65,14 +65,14 @@
timelimit="20"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="1"
timelimit="20"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -115,7 +115,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
......@@ -151,7 +151,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -203,7 +203,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -223,7 +223,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
......@@ -243,7 +243,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
<result status="valid" time="0.35"/>
</proof>
</goal>
<goal
......@@ -263,7 +263,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="1.49"/>
<result status="valid" time="1.10"/>
</proof>
</goal>
<goal
......@@ -315,7 +315,7 @@
expl="precondition"
sum="0c15f39a237a1cee7d6de08d77579ce8"
proved="true"
expanded="false"
expanded="true"
shape="ainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iavalidamk tV4amk arrayV0V3FFFFF">
<label
name="expl:parameter add">
......@@ -325,7 +325,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
......@@ -335,7 +335,7 @@
expl="precondition"
sum="edf3b4f24bb9eac9964f3252a59e4f1d"
proved="true"
expanded="false"
expanded="true"
shape="ainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iavalidamk tV4amk arrayV0V3FFFFF">
<label
name="expl:parameter add">
......@@ -345,7 +345,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -381,7 +381,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter add.3.1.0"
name="WP_parameter add.3.1.1"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="101" loccnumb="6" loccnume="9"
expl="parameter add"
......@@ -397,13 +397,13 @@
proved="true"
expanded="true">
<goal
name="WP_parameter add.3.1.0.0"
name="WP_parameter add.3.1.1.1"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="101" loccnumb="6" loccnume="9"
expl="parameter add"
sum="93b6aa461479bf916ced6982d604ff56"
proved="true"
expanded="false"
expanded="true"
shape="ainfix >alengthadataamk tV6amk arrayV0V5c0Iainfix =V6asetV4V1aSomeV2FIainfix =V5asetV3amodaabsahashV1V0aConsaTuple2V1V2agetV3amodaabsahashV1V0FIainfix <amodaabsahashV1V0V0Aainfix =c0amodaabsahashV1V0Oainfix <c0amodaabsahashV1V0Iainfix <amodaabsahashV1V0V0Aainfix =c0amodaabsahashV1V0Oainfix <c0amodaabsahashV1V0Iainfix =V9aidxamk tV4amk arrayV0V3V7IamemaTuple2V7V8amixfix []adataamk tV4amk arrayV0V3V9Iainfix <V9alengthadataamk tV4amk arrayV0V3Aainfix <=c0V9FFAaoccurs_firstV10V11amixfix []adataamk tV4amk arrayV0V3aidxamk tV4amk arrayV0V3V10qainfix =agetamk tV4amk arrayV0V3V10aSomeV11FAainfix >alengthadataamk tV4amk arrayV0V3c0FFFFF">
<label
name="expl:parameter add">
......@@ -417,7 +417,7 @@
</proof>
</goal>
<goal
name="WP_parameter add.3.1.0.1"
name="WP_parameter add.3.1.1.2"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="101" loccnumb="6" loccnume="9"
expl="parameter add"
......@@ -431,14 +431,14 @@
<proof
prover="2"
timelimit="20"
edited="hash_tables_WP_HashTableImpl_WP_parameter_add_1.v"
edited="hash_tables_WP_HashTableImpl_WP_parameter_add_3.v"
obsolete="false"
archived="false">
<result status="valid" time="0.73"/>
<result status="valid" time="0.74"/>
</proof>
</goal>
<goal
name="WP_parameter add.3.1.0.2"
name="WP_parameter add.3.1.1.3"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="101" loccnumb="6" loccnume="9"
expl="parameter add"
......@@ -454,11 +454,11 @@
timelimit="20"
obsolete="false"
archived="false">
<result status="valid" time="1.56"/>
<result status="valid" time="1.18"/>
</proof>
</goal>
<goal
name="WP_parameter add.3.1.0.3"
name="WP_parameter add.3.1.1.4"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="101" loccnumb="6" loccnume="9"
expl="parameter add"
......@@ -472,10 +472,10 @@
<proof
prover="2"
timelimit="20"
edited="hash_tables_WP_HashTableImpl_WP_parameter_add_2.v"
edited="hash_tables_WP_HashTableImpl_WP_parameter_add_4.v"
obsolete="false"
archived="false">
<result status="valid" time="0.74"/>
<result status="valid" time="0.72"/>
</proof>
</goal>
</transf>
......@@ -489,7 +489,7 @@
expl="parameter add"
sum="189ea93466913e0b9563df5ba4c4602b"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =agetV6V1aSomeV2Iavalidamk tV6amk arrayV0V5Iainfix =V6asetV4V1aSomeV2FIainfix =V5asetV3amodaabsahashV1V0aConsaTuple2V1V2agetV3amodaabsahashV1V0FIainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iavalidamk tV4amk arrayV0V3FFFFF">
<label
name="expl:parameter add">
......@@ -499,7 +499,7 @@
timelimit="30"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -509,7 +509,7 @@
expl="parameter add"
sum="36361ea7cddb5b7f2295c1198bb05d58"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =agetV6V7agetV4V7Iainfix =V7V1NFIavalidamk tV6amk arrayV0V5Iainfix =V6asetV4V1aSomeV2FIainfix =V5asetV3amodaabsahashV1V0aConsaTuple2V1V2agetV3amodaabsahashV1V0FIainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iavalidamk tV4amk arrayV0V3FFFFF">
<label
name="expl:parameter add">
......@@ -519,7 +519,7 @@
timelimit="30"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
......@@ -533,7 +533,7 @@
expl="parameter lookup"
sum="9e3702e537e0dedc39485f070b374dbd"
proved="true"
expanded="false"
expanded="true"
shape="CV1aNilamemaTuple2V0V2V1NFaConsaTuple2VVViainfix =V0V3aoccurs_firstV0V4V1amemaTuple2V0V6V1NFIamemaTuple2V0V7V5NFAaoccurs_firstV0V8V1Iaoccurs_firstV0V8V5FFF">
<label
name="expl:parameter lookup">
......@@ -553,7 +553,7 @@
expl="parameter find"
sum="7df23c1341f47cacd2cc6990d3b1af50"
proved="true"
expanded="false"
expanded="true"
shape="LagetV2amodaabsahashV1V0ainfix =agetV3V1aNoneIamemaTuple2V1V5V4NFAainfix =agetV3V1aSomeV6Iaoccurs_firstV1V6V4FAainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iavalidamk tV3amk arrayV0V2FFFF">
<label
name="expl:parameter find">
......@@ -561,7 +561,7 @@
<transf
name="split_goal"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter find.1"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
......@@ -569,7 +569,7 @@
expl="precondition"
sum="f1dba4d2143790a152c3951d81c6390e"
proved="true"
expanded="false"
expanded="true"
shape="ainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iavalidamk tV3amk arrayV0V2FFFF">
<label
name="expl:parameter find">
......@@ -579,7 +579,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal
......@@ -589,7 +589,7 @@
expl="normal postcondition"
sum="39532d3e8787e4b70b51cd9125d2d841"
proved="true"
expanded="false"
expanded="true"
shape="LagetV2amodaabsahashV1V0ainfix =agetV3V1aSomeV5Iaoccurs_firstV1V5V4FIainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iavalidamk tV3amk arrayV0V2FFFF">
<label
name="expl:parameter find">
......@@ -599,7 +599,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.42"/>
<result status="valid" time="0.32"/>
</proof>
</goal>
<goal
......@@ -609,7 +609,7 @@
expl="exceptional postcondition"
sum="caf50d892506cd9c1de44fa17859a070"
proved="true"
expanded="false"
expanded="true"
shape="LagetV2amodaabsahashV1V0ainfix =agetV3V1aNoneIamemaTuple2V1V5V4NFIainfix =agetV3V1aSomeV6Iaoccurs_firstV1V6V4FIainfix <amodaabsahashV1V0V0Aainfix <=c0amodaabsahashV1V0Iavalidamk tV3amk arrayV0V2FFFF">
<label
name="expl:parameter find">
......@@ -617,10 +617,10 @@
<proof
prover="2"
timelimit="10"
edited="hash_tables_WP_HashTableImpl_WP_parameter_find_1.v"
edited="hash_tables_WP_HashTableImpl_WP_parameter_find_2.v"
obsolete="false"
archived="false">
<result status="valid" time="0.57"/>
<result status="valid" time="0.63"/>
</proof>
</goal>
</transf>
......
......@@ -51,7 +51,7 @@
expl="precondition"
sum="e309e03e7e3741ce8a66c83cc70dfcae"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =alengthaNilainfix +alengthaNilc1Oainfix =alengthaNilalengthaNilIainfix >=alengthV0c2F">
<label
name="expl:parameter split">
......@@ -71,7 +71,7 @@
expl="normal postcondition"
sum="3383c0b32849184c47e1df0d16f14a43"
proved="true"
expanded="false"
expanded="true"
shape="apermutV0ainfix ++V1V2Aainfix <=c1alengthV2Aainfix <=c1alengthV1Iapermutainfix ++V1V2ainfix ++aNilainfix ++aNilV0Aainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1FIainfix =alengthaNilainfix +alengthaNilc1Oainfix =alengthaNilalengthaNilIainfix >=alengthV0c2F">
<label
name="expl:parameter split">
......@@ -91,7 +91,7 @@
expl="parameter split"
sum="545b6e81593a4100d88bf4e348eb286d"
proved="true"
expanded="false"
expanded="true"
shape="CV3aNilapermutainfix ++V1V2ainfix ++V1ainfix ++V2V3Aainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1aConsVVtIainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1FFFIainfix >=alengthV0c2F">
<label
name="expl:parameter split">
......@@ -111,7 +111,7 @@
expl="parameter split"
sum="34656297f11a1464315897ad7c1112ba"
proved="true"
expanded="false"
expanded="true"
shape="CV3aNiltaConsVVainfix =alengthaConsV4V1ainfix +alengthV2c1Oainfix =alengthaConsV4V1alengthV2Aainfix <alengthV5alengthV3Aainfix <=c0alengthV3Iainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1FFFIainfix >=alengthV0c2F">
<label
name="expl:parameter split">
......@@ -141,13 +141,13 @@
proved="true"
expanded="true">
<goal
name="WP_parameter split.5.0"
name="WP_parameter split.5.1"
locfile="examples/programs/mergesort_list/../mergesort_list.mlw"
loclnum="12" loccnumb="6" loccnume="11"
expl="parameter split"
sum="d66e5fe1179e30a6daf00f8ce32191ec"
proved="true"
expanded="false"
expanded="true"
shape="CV3aNiltaConsVVainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6Iapermutainfix ++V6V7ainfix ++V2ainfix ++aConsV4V1V5Aainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6FIainfix =alengthaConsV4V1ainfix +alengthV2c1Oainfix =alengthaConsV4V1alengthV2Aainfix <alengthV5alengthV3Aainfix <=c0alengthV3Iainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1FFFIainfix >=alengthV0c2F">
<label
name="expl:parameter split">
......@@ -157,11 +157,11 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter split.5.1"
name="WP_parameter split.5.2"
locfile="examples/programs/mergesort_list/../mergesort_list.mlw"
loclnum="12" loccnumb="6" loccnume="11"
expl="parameter split"
......@@ -177,7 +177,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="1.88"/>
<result status="valid" time="1.94"/>
</proof>
</goal>
</transf>
......@@ -191,7 +191,7 @@
expl="parameter merge"
sum="891111ea736658ed4790e0db98e650ae"
proved="true"
expanded="false"
expanded="true"
shape="CV1aConsVVCV0aConsVViainfix <=V4V2apermutaConsV4V6ainfix ++V0V1AasortedaConsV4V6IapermutV6ainfix ++V5V1AasortedV6FAasortedV1AasortedV5Aainfix <ainfix +alengthV5alengthV1ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1apermutaConsV2V7ainfix ++V0V1AasortedaConsV2V7IapermutV7ainfix ++V0V3AasortedV7FAasortedV3AasortedV0Aainfix <ainfix +alengthV0alengthV3ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1aNilapermutV1ainfix ++V0V1AasortedV1aNilCV0aNilapermutV1ainfix ++V0V1AasortedV1wapermutV0ainfix ++V0V1AasortedV0IasortedV1AasortedV0FF">
<label
name="expl:parameter merge">
......@@ -199,7 +199,7 @@
<transf
name="split_goal"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter merge.1"
locfile="examples/programs/mergesort_list/../mergesort_list.mlw"
......@@ -207,7 +207,7 @@
expl="parameter merge"
sum="6229f05c1e9a1608ac272a54308b7c75"
proved="true"
expanded="false"
expanded="true"
shape="CV1aConsVVCV0aConsVVasortedV1AasortedV5Aainfix <ainfix +alengthV5alengthV1ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1Iainfix <=V4V2aNiltaNiltIasortedV1AasortedV0FF">
<label
name="expl:parameter merge">
......@@ -227,7 +227,7 @@
expl="parameter merge"
sum="990f60cd608f4581a5a1db9eaa9b79d0"
proved="true"
expanded="false"
expanded="true"
shape="CV1aConsVVCV0aConsVVapermutaConsV4V6ainfix ++V0V1AasortedaConsV4V6IapermutV6ainfix ++V5V1AasortedV6FIasortedV1AasortedV5Aainfix <ainfix +alengthV5alengthV1ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1Iainfix <=V4V2aNiltaNiltIasortedV1AasortedV0FF">
<label
name="expl:parameter merge">
......@@ -237,7 +237,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.77"/>
<result status="valid" time="0.82"/>
</proof>
</goal>
<goal
......@@ -247,7 +247,7 @@
expl="parameter merge"
sum="90c2c680cba8970dd1a5f7cea3dedc85"
proved="true"
expanded="false"
expanded="true"
shape="CV1aConsVVCV0aConsVVasortedV3AasortedV0Aainfix <ainfix +alengthV0alengthV3ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1Iainfix <=V4V2NaNiltaNiltIasortedV1AasortedV0FF">
<label
name="expl:parameter merge">
......@@ -274,7 +274,7 @@
expl="parameter merge"
sum="97a0aa41004451e6280a9235311f9abc"
proved="true"