insertion sort completed

examples/programs/insertion_sort.mlw

@@ -25,9 +25,12 @@ module InsertionSort
              0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2]) and
           (forall k: int. !j+1 <= k <= i -> v < a[k]) }
         variant { !j }
+        label L1:
         a[!j] <- a[!j - 1];
+        assert { exchange a[!j-1 <- v] (at a L1)[!j <- v] (!j - 1) !j};
         j := !j - 1
       done;
+      assert { forall k: int. 0 <= k < !j -> a[k] <= v };
       a[!j] <- v
     done
     { sorted a and permut a (old a) }

examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_4.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Definition unit  := unit.
+
+Parameter label : Type.
+
+Parameter at1: forall (a:Type), a -> label  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Inductive ref (a:Type) :=
+  | mk_ref : a -> ref a.
+Implicit Arguments mk_ref.
+
+Definition contents (a:Type)(u:(ref a)): a :=
+  match u with
+  | mk_ref contents1 => contents1
+  end.
+Implicit Arguments contents.
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a  -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b  -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter const: forall (b:Type) (a:Type), b  -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
+  b1):(map a b)) a1) = b1).
+
+Inductive array (a:Type) :=
+  | mk_array : Z -> (map Z a) -> array a.
+Implicit Arguments mk_array.
+
+Definition elts (a:Type)(u:(array a)): (map Z a) :=
+  match u with
+  | mk_array _ elts1 => elts1
+  end.
+Implicit Arguments elts.
+
+Definition length (a:Type)(u:(array a)): Z :=
+  match u with
+  | mk_array length1 _ => length1
+  end.
+Implicit Arguments length.
+
+Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
+Implicit Arguments get1.
+
+Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
+  match a1 with
+  | mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
+  end.
+Implicit Arguments set1.
+
+Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z),
+  (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 <  u)%Z) -> ((get a i1) <= (get a
+  i2))%Z.
+
+Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a)
+  l u).
+
+Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)).
+
+Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
+  (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i <  u)%Z) -> ((get a1
+  i) = (get a2 i)).
+Implicit Arguments map_eq_sub.
+
+Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z)
+  (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\
+  forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))).
+Implicit Arguments exchange.
+
+Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z)
+  (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j).
+
+Inductive permut_sub{a:Type}  : (map Z a) -> (map Z a) -> Z -> Z -> Prop :=
+  | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
+      (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
+  | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
+      (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
+  | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
+      forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
+      u) -> (permut_sub a1 a3 l u))
+  | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
+      (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i <  u)%Z) -> (((l <= j)%Z /\
+      (j <  u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
+Implicit Arguments permut_sub.
+
+Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z
+  a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\
+  (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
+
+Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
+  forall (l:Z) (u:Z), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z),
+  ((i <  l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))).
+
+Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
+  forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\
+  (i <  u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j <  u)%Z) /\ ((get a2
+  i) = (get a1 j)).
+
+Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z)
+  (j:Z): Prop := (exchange (elts a1) (elts a2) i j).
+Implicit Arguments exchange1.
+
+Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
+  (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
+Implicit Arguments permut_sub1.
+
+Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
+  ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z
+  (length a1)).
+Implicit Arguments permut.
+
+Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
+  (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
+Implicit Arguments array_eq_sub.
+
+Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
+  ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)).
+Implicit Arguments array_eq.
+
+Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
+  a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u).
+
+Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
+  a)), (array_eq a1 a2) -> (permut a1 a2).
+
+Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z Z)),
+  let a2 := (mk_array a a1) in ((1%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z
+  Z)), let a4 := (mk_array a a3) in forall (i:Z), ((1%Z <= i)%Z /\
+  (i <= (a - 1%Z)%Z)%Z) -> (((sorted_sub a3 0%Z i) /\ (permut a4 a2)) ->
+  (((0%Z <= i)%Z /\ (i <  a)%Z) -> let result := (get a3 i) in
+  ((((0%Z <= i)%Z /\ (i <= i)%Z) /\ ((permut (set1 a4 i result) a2) /\
+  ((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) ->
+  ((~ (k1 = i)) -> ((~ (k2 = i)) -> ((get a3 k1) <= (get a3 k2))%Z))) /\
+  forall (k:Z), (((i + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result <  (get a3
+  k))%Z))) -> forall (j:Z), forall (a5:(map Z Z)), let a6 := (mk_array a
+  a5) in ((((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut (set1 a6 j result) a2) /\
+  ((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) ->
+  ((~ (k1 = j)) -> ((~ (k2 = j)) -> ((get a5 k1) <= (get a5 k2))%Z))) /\
+  forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result <  (get a5
+  k))%Z))) -> ((0%Z <  j)%Z -> (((0%Z <= (j - 1%Z)%Z)%Z /\
+  ((j - 1%Z)%Z <  a)%Z) -> ((result <  (get a5 (j - 1%Z)%Z))%Z ->
+  (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z <  a)%Z) -> (((0%Z <= j)%Z /\
+  (j <  a)%Z) -> forall (a7:(map Z Z)), let a8 := (mk_array a a7) in
+  ((a7 = (set a5 j (get a5 (j - 1%Z)%Z))) -> ((exchange match (set1 a8
+  (j - 1%Z)%Z result) with
+  | mk_array _ elts1 => elts1
+  end match (set1 a6 j result) with
+  | mk_array _ elts1 => elts1
+  end (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut (set1 a8
+  j1 result) a2))))))))))))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intuition.
+intuition.
+unfold set1.
+unfold permut.
+split.
+simpl.
+auto.
+apply permut_trans with (elts (set1 (mk_array a a5) j (get a3 i))); auto.
+subst j1.
+apply permut_exchange with (j-1)%Z j.
+simpl; omega.
+simpl; omega.
+assumption.
+unfold permut in H17.
+intuition.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/insertion_sort/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<why3session name="examples/programs/insertion_sort/why3session.xml">
+ <file name="../insertion_sort.mlw" verified="true" expanded="true">
+  <theory name="InsertionSort" verified="true" expanded="true">
+   <goal name="WP_parameter insertion_sort" expl="correctness of parameter insertion_sort" sum="ef92331d960a2b4416cbb02fb9790f17" proved="true" expanded="true">
+    <transf name="split_goal" proved="true" expanded="true">
+     <goal name="WP_parameter insertion_sort.1" expl="normal postcondition" sum="2a41244e215651117e1ff02f7b903874" proved="true" expanded="true">
+      <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+       <result status="valid" time="0.04"/>
+      </proof>
+     </goal>
+     <goal name="WP_parameter insertion_sort.2" expl="for loop initialization" sum="31d78339e0c6376c167a6614f0ef9890" proved="true" expanded="true">
+      <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+       <result status="valid" time="0.03"/>
+      </proof>
+     </goal>
+     <goal name="WP_parameter insertion_sort.3" expl="for loop preservation" sum="84f7c0562e054e5bb16690fca7477335" proved="true" expanded="true">
+      <transf name="split_goal" proved="true" expanded="true">
+       <goal name="WP_parameter insertion_sort.3.1" expl="for loop preservation" sum="06c05dcdd09292b5e9c55a2faaf652c6" proved="true" expanded="true">
+        <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+         <result status="valid" time="0.02"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.2" expl="for loop preservation" sum="3134d01c92e614aae99ef369c3ce6cd3" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.3" expl="for loop preservation" sum="6e4882dcf03b5b7366a19dc279254af9" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+        <proof prover="z3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.26"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.4" expl="for loop preservation" sum="9b6aa0eb961b48af3ad659791ef78169" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+        <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+        <proof prover="z3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.00"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.5" expl="for loop preservation" sum="69a89c8c9b4a9be76d6db36bc7b5b91c" proved="true" expanded="true">
+        <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+         <result status="valid" time="0.02"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.6" expl="for loop preservation" sum="6bc474caa7630e70e3a699590d48b0f3" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.08"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.7" expl="for loop preservation" sum="0e8c0f61758025a24cef577f2f83009c" proved="true" expanded="true">
+        <transf name="split_goal" proved="true" expanded="true">
+         <goal name="WP_parameter insertion_sort.3.7.1" expl="for loop preservation" sum="a815ea7ad580c23f995fd0c6bbfb6a9b" proved="true" expanded="true">
+          <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.02"/>
+          </proof>
+         </goal>
+         <goal name="WP_parameter insertion_sort.3.7.2" expl="for loop preservation" sum="26e9e882f48142e7bbfc09885304c68a" proved="true" expanded="true">
+          <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.03"/>
+          </proof>
+         </goal>
+         <goal name="WP_parameter insertion_sort.3.7.3" expl="for loop preservation" sum="620b469e57272b0e9459c491dc715458" proved="true" expanded="true">
+          <proof prover="coq" timelimit="10" edited="insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_4.v" obsolete="false">
+           <result status="valid" time="0.76"/>
+          </proof>
+         </goal>
+         <goal name="WP_parameter insertion_sort.3.7.4" expl="for loop preservation" sum="f495be28de19eff26986fcbc1d6e1c42" proved="true" expanded="true">
+          <proof prover="z3" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.38"/>
+          </proof>
+         </goal>
+         <goal name="WP_parameter insertion_sort.3.7.5" expl="for loop preservation" sum="8563658557dd29d98c764aca0717b8ad" proved="true" expanded="true">
+          <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.04"/>
+          </proof>
+         </goal>
+        </transf>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.8" expl="for loop preservation" sum="583bb467e5adea0fa5655cc38c6ade6f" proved="true" expanded="true">
+        <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.9" expl="for loop preservation" sum="461c9ebad19b798f1b9aea9ca172171f" proved="true" expanded="true">
+        <proof prover="z3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.30"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.10" expl="for loop preservation" sum="679f58f4ef51e543c4abc050b2c00759" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.11" expl="for loop preservation" sum="64018d9c729019b9d1df0101137844e7" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.08"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.12" expl="for loop preservation" sum="2db3a3e685efb87df5de572b60ac2536" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.13" expl="for loop preservation" sum="acce33660a882d971cc7ce1f5bbfbbc0" proved="true" expanded="true">
+        <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+         <result status="valid" time="0.02"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.14" expl="for loop preservation" sum="0df91a25c37a1e4afa745e505e26f7a3" proved="true" expanded="true">
+        <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+         <result status="valid" time="0.02"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.15" expl="for loop preservation" sum="b2ffa80d7fd15a8ade1689e8386ed986" proved="true" expanded="true">
+        <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+         <result status="valid" time="0.02"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.16" expl="for loop preservation" sum="6bb4701d6433b7eb07c95aa7a911dac8" proved="true" expanded="true">
+        <transf name="split_goal" proved="true" expanded="true">
+         <goal name="WP_parameter insertion_sort.3.16.1" expl="for loop preservation" sum="99dfb3b9483e8c21e316a1e28499ce79" proved="true" expanded="true">
+          <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.02"/>
+          </proof>
+         </goal>
+         <goal name="WP_parameter insertion_sort.3.16.2" expl="for loop preservation" sum="2053997a28da90415fd6b46d2d75b705" proved="true" expanded="true">
+          <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.02"/>
+          </proof>
+         </goal>
+         <goal name="WP_parameter insertion_sort.3.16.3" expl="for loop preservation" sum="532d1e719813d890b534739020615dbf" proved="true" expanded="true">
+          <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.02"/>
+          </proof>
+         </goal>
+         <goal name="WP_parameter insertion_sort.3.16.4" expl="for loop preservation" sum="e0448c92bd31d8be686de0534a64046a" proved="true" expanded="true">
+          <proof prover="z3" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.00"/>
+          </proof>
+         </goal>
+         <goal name="WP_parameter insertion_sort.3.16.5" expl="for loop preservation" sum="d13c34fc9f323f850075a18711b94d6a" proved="true" expanded="true">
+          <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.01"/>
+          </proof>
+          <proof prover="z3" timelimit="10" edited="" obsolete="false">
+           <result status="valid" time="0.00"/>
+          </proof>
+         </goal>
+        </transf>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.17" expl="for loop preservation" sum="2472a32ce156f6eda1ad642d8f1027a4" proved="true" expanded="true">
+        <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.18" expl="for loop preservation" sum="a4e0a8694106c4bacaace830bc796277" proved="true" expanded="true">
+        <proof prover="z3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.04"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.19" expl="for loop preservation" sum="78bd9b34f24e244e308267c4547aac57" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.04"/>
+        </proof>
+        <proof prover="z3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.04"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.20" expl="for loop preservation" sum="8920e63deaeb05b751c9627248574f20" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.08"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter insertion_sort.3.21" expl="for loop preservation" sum="975e6f2ba29850c5e47e736464c85ab0" proved="true" expanded="true">
+        <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.04"/>
+        </proof>
+       </goal>
+      </transf>
+     </goal>
+     <goal name="WP_parameter insertion_sort.4" expl="normal postcondition" sum="2af561155cebd682e2289389043d7b0f" proved="true" expanded="true">
+      <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+       <result status="valid" time="0.02"/>
+      </proof>
+     </goal>
+    </transf>
+   </goal>
+  </theory>
+ </file>
+</why3session>