diff --git a/examples/programs/edit_distance.mlw b/examples/programs/edit_distance.mlw
index 166639c05d2771e9bf460837cbc28464f7b14588..2a862abe4b64fefc873488b97c737cf55c088dc1 100644
--- a/examples/programs/edit_distance.mlw
+++ b/examples/programs/edit_distance.mlw
@@ -45,7 +45,7 @@ theory Word
      repository, in examples/edit-distance/words.v)
      It would be really  helpful to have recursive definitions output
      as such in Coq when possible *)
-(***
+
   use export list.Append
 
   function last_char (a: char) (u: word) : char = match u with
@@ -89,7 +89,7 @@ theory Word
   lemma dist_concat_right:
     forall u v w: word, n: int.
     dist v w n -> dist v (u ++ w) (length u + n)
-***)
+
   (* end of intermediate lemmas *)
 
   lemma min_dist_equal:
diff --git a/examples/programs/edit_distance/edit_distance_Word_dist_concat_left_1.v b/examples/programs/edit_distance/edit_distance_Word_dist_concat_left_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..de107ecfabc3103d707e036cd62daeb057662fbd
--- /dev/null
+++ b/examples/programs/edit_distance/edit_distance_Word_dist_concat_left_1.v
@@ -0,0 +1,152 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
+  (y <= (Zmax x y))%Z.
+
+Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
+
+Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
+  ((Zmin x y) <= y)%Z.
+
+Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
+
+Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
+
+Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
+
+Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
+
+Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
+
+Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
+
+Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil  => 0%Z
+  | Cons _ r => (1%Z + (length r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
+  (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall (a:Type), forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil:(list a))).
+
+Parameter char : Type.
+
+Definition word  := (list char).
+
+Inductive dist : (list char) -> (list char) -> Z -> Prop :=
+  | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
+  | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
+  | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
+  | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
+
+Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
+  w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
+
+Set Implicit Arguments.
+Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
+  a) :=
+  match l1 with
+  | Nil  => l2
+  | Cons x1 r1 => (Cons x1 (infix_plpl r1 l2))
+  end.
+Unset Implicit Arguments.
+
+Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
+  (Nil:(list a))) = l).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil  => False
+  | Cons y r => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
+  (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
+
+Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
+  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
+
+Set Implicit Arguments.
+Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
+  match u with
+  | Nil  => a
+  | Cons c uqt => (last_char c uqt)
+  end.
+Unset Implicit Arguments.
+
+Set Implicit Arguments.
+Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
+  match u with
+  | Nil  => (Nil:(list char))
+  | Cons c uqt => (Cons a (but_last c uqt))
+  end.
+Unset Implicit Arguments.
+
+Axiom first_last_explicit : forall (u:(list char)) (a:char),
+  ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil:(list
+  char)))) = (Cons a u)).
+
+Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
+  exists b:char, ((infix_plpl v (Cons b (Nil:(list char)))) = (Cons a u)) /\
+  ((length v) = (length u)).
+
+Axiom key_lemma_right : forall (w1:(list char)) (wqt2:(list char)) (m:Z)
+  (a:char), (dist w1 wqt2 m) -> forall (w2:(list char)), (wqt2 = (Cons a
+  w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z,
+  (w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
+  ((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
+
+Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+  w2 n) -> (dist w2 w1 n).
+
+Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
+  (a:char), (dist (Cons a w1) w2 m) -> exists u2:(list char), exists v2:(list
+  char), exists k:Z, (w2 = (infix_plpl u2 v2)) /\ ((dist w1 v2 k) /\
+  ((k + (length u2))%Z <= (m + 1%Z)%Z)%Z).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem dist_concat_left : forall (u:(list char)) (v:(list char)) (w:(list
+  char)) (n:Z), (dist v w n) -> (dist (infix_plpl u v) w ((length u) + n)%Z).
+(* YOU MAY EDIT THE PROOF BELOW *)
+simple induction u; intros.
+auto.
+unfold length; fold length.
+replace (1 + length l + n)%Z with (length l + n + 1)%Z;
+ [ idtac | omega ].
+apply dist_add_left; auto.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/examples/programs/edit_distance/edit_distance_Word_dist_symetry_1.v b/examples/programs/edit_distance/edit_distance_Word_dist_symetry_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..dbc5297d03828520f9fa59d6ee32ad6fe0adc1e1
--- /dev/null
+++ b/examples/programs/edit_distance/edit_distance_Word_dist_symetry_1.v
@@ -0,0 +1,143 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
+  (y <= (Zmax x y))%Z.
+
+Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
+
+Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
+  ((Zmin x y) <= y)%Z.
+
+Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
+
+Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
+
+Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
+
+Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
+
+Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
+
+Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
+
+Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil  => 0%Z
+  | Cons _ r => (1%Z + (length r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
+  (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall (a:Type), forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil:(list a))).
+
+Parameter char : Type.
+
+Definition word  := (list char).
+
+Inductive dist : (list char) -> (list char) -> Z -> Prop :=
+  | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
+  | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
+  | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
+  | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
+
+Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
+  w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
+
+Set Implicit Arguments.
+Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
+  a) :=
+  match l1 with
+  | Nil  => l2
+  | Cons x1 r1 => (Cons x1 (infix_plpl r1 l2))
+  end.
+Unset Implicit Arguments.
+
+Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
+  (Nil:(list a))) = l).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil  => False
+  | Cons y r => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
+  (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
+
+Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
+  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
+
+Set Implicit Arguments.
+Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
+  match u with
+  | Nil  => a
+  | Cons c uqt => (last_char c uqt)
+  end.
+Unset Implicit Arguments.
+
+Set Implicit Arguments.
+Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
+  match u with
+  | Nil  => (Nil:(list char))
+  | Cons c uqt => (Cons a (but_last c uqt))
+  end.
+Unset Implicit Arguments.
+
+Axiom first_last_explicit : forall (u:(list char)) (a:char),
+  ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil:(list
+  char)))) = (Cons a u)).
+
+Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
+  exists b:char, ((infix_plpl v (Cons b (Nil:(list char)))) = (Cons a u)) /\
+  ((length v) = (length u)).
+
+Axiom key_lemma_right : forall (w1:(list char)) (wqt2:(list char)) (m:Z)
+  (a:char), (dist w1 wqt2 m) -> forall (w2:(list char)), (wqt2 = (Cons a
+  w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z,
+  (w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
+  ((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z),
+  (dist w1 w2 n) -> (dist w2 w1 n).
+(* YOU MAY EDIT THE PROOF BELOW *)
+simple induction 1; intros.
+exact dist_eps.
+apply dist_add_right; assumption.
+apply dist_add_left; assumption.
+apply dist_context; assumption.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/examples/programs/edit_distance/edit_distance_Word_first_last_1.v b/examples/programs/edit_distance/edit_distance_Word_first_last_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..e840cd1d0264764120bac06d0bbf447c08f624c5
--- /dev/null
+++ b/examples/programs/edit_distance/edit_distance_Word_first_last_1.v
@@ -0,0 +1,139 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
+  (y <= (Zmax x y))%Z.
+
+Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
+
+Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
+  ((Zmin x y) <= y)%Z.
+
+Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
+
+Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
+
+Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
+
+Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
+
+Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
+
+Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
+
+Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil  => 0%Z
+  | Cons _ r => (1%Z + (length r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
+  (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall (a:Type), forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil:(list a))).
+
+Parameter char : Type.
+
+Definition word  := (list char).
+
+Inductive dist : (list char) -> (list char) -> Z -> Prop :=
+  | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
+  | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
+  | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
+  | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
+
+Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
+  w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
+
+Set Implicit Arguments.
+Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
+  a) :=
+  match l1 with
+  | Nil  => l2
+  | Cons x1 r1 => (Cons x1 (infix_plpl r1 l2))
+  end.
+Unset Implicit Arguments.
+
+Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
+  (Nil:(list a))) = l).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil  => False
+  | Cons y r => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
+  (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
+
+Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
+  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
+
+Set Implicit Arguments.
+Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
+  match u with
+  | Nil  => a
+  | Cons c uqt => (last_char c uqt)
+  end.
+Unset Implicit Arguments.
+
+Set Implicit Arguments.
+Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
+  match u with
+  | Nil  => (Nil:(list char))
+  | Cons c uqt => (Cons a (but_last c uqt))
+  end.
+Unset Implicit Arguments.
+
+Axiom first_last_explicit : forall (u:(list char)) (a:char),
+  ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil:(list
+  char)))) = (Cons a u)).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem first_last : forall (a:char) (u:(list char)), exists v:(list char),
+  exists b:char, ((infix_plpl v (Cons b (Nil:(list char)))) = (Cons a u)) /\
+  ((length v) = (length u)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros a u.
+exists (but_last a u).
+exists (last_char a u).
+split.
+ exact (first_last_explicit u a).
+generalize a; induction u; intros.
+simpl; omega.
+unfold but_last; fold but_last.
+unfold length; fold length.
+generalize (IHu a0); intros; omega.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/examples/programs/edit_distance/edit_distance_Word_first_last_explicit_1.v b/examples/programs/edit_distance/edit_distance_Word_first_last_explicit_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..e3f185bb0f008a46a503071a8e8ef4e5e62aa95c
--- /dev/null
+++ b/examples/programs/edit_distance/edit_distance_Word_first_last_explicit_1.v
@@ -0,0 +1,130 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
+  (y <= (Zmax x y))%Z.
+
+Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
+
+Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
+  ((Zmin x y) <= y)%Z.
+
+Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
+
+Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
+
+Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
+
+Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
+
+Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
+
+Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
+
+Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil  => 0%Z
+  | Cons _ r => (1%Z + (length r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
+  (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall (a:Type), forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil:(list a))).
+
+Parameter char : Type.
+
+Definition word  := (list char).
+
+Inductive dist : (list char) -> (list char) -> Z -> Prop :=
+  | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
+  | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
+  | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
+  | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
+
+Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
+  w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
+
+Set Implicit Arguments.
+Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
+  a) :=
+  match l1 with
+  | Nil  => l2
+  | Cons x1 r1 => (Cons x1 (infix_plpl r1 l2))
+  end.
+Unset Implicit Arguments.
+
+Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
+  (Nil:(list a))) = l).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil  => False
+  | Cons y r => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
+  (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
+
+Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
+  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
+
+Set Implicit Arguments.
+Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
+  match u with
+  | Nil  => a
+  | Cons c uqt => (last_char c uqt)
+  end.
+Unset Implicit Arguments.
+
+Set Implicit Arguments.
+Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
+  match u with
+  | Nil  => (Nil:(list char))
+  | Cons c uqt => (Cons a (but_last c uqt))
+  end.
+Unset Implicit Arguments.
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem first_last_explicit : forall (u:(list char)) (a:char),
+  ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil:(list
+  char)))) = (Cons a u)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+simple induction u; simpl.
+reflexivity.
+intros.
+rewrite (H a).
+reflexivity.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/examples/programs/edit_distance/edit_distance_Word_key_lemma_right_1.v b/examples/programs/edit_distance/edit_distance_Word_key_lemma_right_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..fe76272147ee03941740491959ea6905d12181c6
--- /dev/null
+++ b/examples/programs/edit_distance/edit_distance_Word_key_lemma_right_1.v
@@ -0,0 +1,171 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
+  (y <= (Zmax x y))%Z.
+
+Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
+
+Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
+  ((Zmin x y) <= y)%Z.
+
+Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
+
+Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
+
+Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
+
+Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
+
+Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
+
+Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
+
+Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil  => 0%Z
+  | Cons _ r => (1%Z + (length r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
+  (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall (a:Type), forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil:(list a))).
+
+Parameter char : Type.
+
+Definition word  := (list char).
+
+Inductive dist : (list char) -> (list char) -> Z -> Prop :=
+  | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
+  | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
+  | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
+  | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
+
+Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
+  w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
+
+Set Implicit Arguments.
+Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
+  a) :=
+  match l1 with
+  | Nil  => l2
+  | Cons x1 r1 => (Cons x1 (infix_plpl r1 l2))
+  end.
+Unset Implicit Arguments.
+
+Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
+  (Nil:(list a))) = l).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil  => False
+  | Cons y r => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
+  (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
+
+Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
+  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
+
+Set Implicit Arguments.
+Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
+  match u with
+  | Nil  => a
+  | Cons c uqt => (last_char c uqt)
+  end.
+Unset Implicit Arguments.
+
+Set Implicit Arguments.
+Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
+  match u with
+  | Nil  => (Nil:(list char))
+  | Cons c uqt => (Cons a (but_last c uqt))
+  end.
+Unset Implicit Arguments.
+
+Axiom first_last_explicit : forall (u:(list char)) (a:char),
+  ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil:(list
+  char)))) = (Cons a u)).
+
+Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
+  exists b:char, ((infix_plpl v (Cons b (Nil:(list char)))) = (Cons a u)) /\
+  ((length v) = (length u)).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+Lemma app_comm_cons: forall (A:Type) (x y : list A) (a: A),
+   Cons a (infix_plpl x y) = infix_plpl (Cons a x) y.
+simpl; auto.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+Theorem key_lemma_right : forall (w1:(list char)) (wqt2:(list char)) (m:Z)
+  (a:char), (dist w1 wqt2 m) -> forall (w2:(list char)), (wqt2 = (Cons a
+  w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z,
+  (w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
+  ((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros w1 w'2 m a H; elim H.
+(* 1. [dist_eps]: absurd *)
+intros; discriminate H0.
+(* 2. [dist_add_left]: we use induction hypothesis. *)
+intros w'1 w3 n Hdist Hrec b w2 Heq.
+  elim (Hrec w2 Heq); intros u'1 Hex.
+elim Hex; clear Hex; intros v'1 Hex.
+elim Hex; clear Hex; intros k Hex.
+decompose [and] Hex; clear Hex.
+elim (first_last b u'1); intros u1 Hex.
+elim Hex; intros c [Hc Hlength].
+exists u1; exists (Cons c v'1); exists (k + 1)%Z.
+repeat split.
+rewrite H0.
+rewrite app_comm_cons.
+rewrite <- Hc.
+rewrite <- Append_assoc; reflexivity.
+apply dist_add_left; assumption.
+omega.
+(* 3. [dist_add_right]: direct *)
+intros.
+exists Nil; exists w0; exists n.
+repeat split.
+inversion H2.
+rewrite <- H5; assumption.
+simpl; omega.
+(* 4. [dist_context]: direct *)
+intros.
+inversion H2.
+exists (Cons a Nil); exists w0; exists n.
+repeat split.
+rewrite <- H5; assumption.
+simpl; omega.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/examples/programs/edit_distance/edit_distance_Word_min_dist_diff_1.v b/examples/programs/edit_distance/edit_distance_Word_min_dist_diff_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..a41e66726e732c5e92d63d93f68bbb7d5a71321c
--- /dev/null
+++ b/examples/programs/edit_distance/edit_distance_Word_min_dist_diff_1.v
@@ -0,0 +1,164 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
+  (y <= (Zmax x y))%Z.
+
+Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
+
+Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
+  ((Zmin x y) <= y)%Z.
+
+Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
+
+Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
+
+Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
+
+Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
+
+Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
+
+Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
+
+Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil  => 0%Z
+  | Cons _ r => (1%Z + (length r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
+  (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall (a:Type), forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil:(list a))).
+
+Parameter char : Type.
+
+Definition word  := (list char).
+
+Inductive dist : (list char) -> (list char) -> Z -> Prop :=
+  | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
+  | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
+  | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
+  | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
+
+Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
+  w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
+
+Set Implicit Arguments.
+Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
+  a) :=
+  match l1 with
+  | Nil  => l2
+  | Cons x1 r1 => (Cons x1 (infix_plpl r1 l2))
+  end.
+Unset Implicit Arguments.
+
+Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
+  (Nil:(list a))) = l).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil  => False
+  | Cons y r => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
+  (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
+
+Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
+  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
+
+Set Implicit Arguments.
+Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
+  match u with
+  | Nil  => a
+  | Cons c uqt => (last_char c uqt)
+  end.
+Unset Implicit Arguments.
+
+Set Implicit Arguments.
+Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
+  match u with
+  | Nil  => (Nil:(list char))
+  | Cons c uqt => (Cons a (but_last c uqt))
+  end.
+Unset Implicit Arguments.
+
+Axiom first_last_explicit : forall (u:(list char)) (a:char),
+  ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil:(list
+  char)))) = (Cons a u)).
+
+Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
+  exists b:char, ((infix_plpl v (Cons b (Nil:(list char)))) = (Cons a u)) /\
+  ((length v) = (length u)).
+
+Axiom key_lemma_right : forall (w1:(list char)) (wqt2:(list char)) (m:Z)
+  (a:char), (dist w1 wqt2 m) -> forall (w2:(list char)), (wqt2 = (Cons a
+  w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z,
+  (w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
+  ((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
+
+Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+  w2 n) -> (dist w2 w1 n).
+
+Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
+  (a:char), (dist (Cons a w1) w2 m) -> exists u2:(list char), exists v2:(list
+  char), exists k:Z, (w2 = (infix_plpl u2 v2)) /\ ((dist w1 v2 k) /\
+  ((k + (length u2))%Z <= (m + 1%Z)%Z)%Z).
+
+Axiom dist_concat_left : forall (u:(list char)) (v:(list char)) (w:(list
+  char)) (n:Z), (dist v w n) -> (dist (infix_plpl u v) w ((length u) + n)%Z).
+
+Axiom dist_concat_right : forall (u:(list char)) (v:(list char)) (w:(list
+  char)) (n:Z), (dist v w n) -> (dist v (infix_plpl u w) ((length u) + n)%Z).
+
+Axiom min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char)
+  (n:Z), (min_dist w1 w2 n) -> (min_dist (Cons a w1) (Cons a w2) n).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem min_dist_diff : forall (w1:(list char)) (w2:(list char)) (a:char)
+  (b:char) (m:Z) (p:Z), (~ (a = b)) -> ((min_dist (Cons a w1) w2 p) ->
+  ((min_dist w1 (Cons b w2) m) -> (min_dist (Cons a w1) (Cons b w2)
+  ((Zmin m p) + 1%Z)%Z))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros w1 w2 a b m p.
+ unfold min_dist; intuition.
+unfold Zmin.
+case (m ?= p)%Z; generalize dist_add_left dist_add_right; intuition.
+
+generalize (Zle_min_l m p) (Zle_min_r m p) Zplus_le_compat_r Zle_trans.
+inversion H1; intuition eauto.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/examples/programs/edit_distance/edit_distance_Word_min_dist_equal_1.v b/examples/programs/edit_distance/edit_distance_Word_min_dist_equal_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..a445ed3a465479168db17d0ccf9764485be24e77
--- /dev/null
+++ b/examples/programs/edit_distance/edit_distance_Word_min_dist_equal_1.v
@@ -0,0 +1,180 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
+  (y <= (Zmax x y))%Z.
+
+Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
+
+Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
+  ((Zmin x y) <= y)%Z.
+
+Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
+
+Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
+
+Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
+
+Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
+
+Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
+
+Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
+
+Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil  => 0%Z
+  | Cons _ r => (1%Z + (length r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
+  (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall (a:Type), forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil:(list a))).
+
+Parameter char : Type.
+
+Definition word  := (list char).
+
+Inductive dist : (list char) -> (list char) -> Z -> Prop :=
+  | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
+  | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
+  | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
+  | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+      w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
+
+Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
+  w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
+
+Set Implicit Arguments.
+Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
+  a) :=
+  match l1 with
+  | Nil  => l2
+  | Cons x1 r1 => (Cons x1 (infix_plpl r1 l2))
+  end.
+Unset Implicit Arguments.
+
+Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
+  (Nil:(list a))) = l).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil  => False
+  | Cons y r => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
+  (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
+
+Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
+  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
+
+Set Implicit Arguments.
+Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
+  match u with
+  | Nil  => a
+  | Cons c uqt => (last_char c uqt)
+  end.
+Unset Implicit Arguments.
+
+Set Implicit Arguments.
+Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
+  match u with
+  | Nil  => (Nil:(list char))
+  | Cons c uqt => (Cons a (but_last c uqt))
+  end.
+Unset Implicit Arguments.
+
+Axiom first_last_explicit : forall (u:(list char)) (a:char),
+  ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil:(list
+  char)))) = (Cons a u)).
+
+Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
+  exists b:char, ((infix_plpl v (Cons b (Nil:(list char)))) = (Cons a u)) /\
+  ((length v) = (length u)).
+
+Axiom key_lemma_right : forall (w1:(list char)) (wqt2:(list char)) (m:Z)
+  (a:char), (dist w1 wqt2 m) -> forall (w2:(list char)), (wqt2 = (Cons a
+  w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z,
+  (w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
+  ((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
+
+Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
+  w2 n) -> (dist w2 w1 n).
+
+Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
+  (a:char), (dist (Cons a w1) w2 m) -> exists u2:(list char), exists v2:(list
+  char), exists k:Z, (w2 = (infix_plpl u2 v2)) /\ ((dist w1 v2 k) /\
+  ((k + (length u2))%Z <= (m + 1%Z)%Z)%Z).
+
+Axiom dist_concat_left : forall (u:(list char)) (v:(list char)) (w:(list
+  char)) (n:Z), (dist v w n) -> (dist (infix_plpl u v) w ((length u) + n)%Z).
+
+Axiom dist_concat_right : forall (u:(list char)) (v:(list char)) (w:(list
+  char)) (n:Z), (dist v w n) -> (dist v (infix_plpl u w) ((length u) + n)%Z).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char)
+  (n:Z), (min_dist w1 w2 n) -> (min_dist (Cons a w1) (Cons a w2) n).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros w1 w2 a n.
+unfold min_dist.
+generalize dist_context; intuition.
+
+inversion H0.
+
+elim (key_lemma_right w1 (Cons a w2) n0 a H7 w2);
+ [ idtac | reflexivity ].
+intros u1 Hex; elim Hex; clear Hex.
+intros v1 Hex; elim Hex; clear Hex.
+intros k Hex.
+ decompose [and] Hex; clear Hex.
+generalize (dist_concat_left u1 v1 w2 k H10); intro.
+apply Zle_trans with (length u1 + k)%Z.
+apply H2.
+rewrite H8; assumption.
+omega.
+elim (key_lemma_left w1 w2 n0 a H7).
+intros u2 Hex; elim Hex; clear Hex.
+intros v2 Hex; elim Hex; clear Hex.
+intros k Hex.
+ decompose [and] Hex; clear Hex.
+generalize (dist_concat_right u2 w1 v2 k H10); intro.
+apply Zle_trans with (length u2 + k)%Z.
+apply H2.
+rewrite H8; assumption.
+omega.
+auto.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/examples/programs/edit_distance/why3session.xml b/examples/programs/edit_distance/why3session.xml
index 2902cbbafdff77544df59496f8cddf2d8504a478..5f6ccc88d1a786003776e72178e0c7cd436367b2 100644
--- a/examples/programs/edit_distance/why3session.xml
+++ b/examples/programs/edit_distance/why3session.xml
@@ -10,252 +10,297 @@
  <prover id="spass" name="Spass" version="3.5"/>
  <prover id="yices" name="Yices" version="1.0.27"/>
  <prover id="z3" name="Z3" version="2.19"/>
- <file name="../edit_distance.mlw" verified="false" expanded="true">
-  <theory name="Word" verified="false" expanded="true">
-   <goal name="min_dist_equal" sum="3d9a456ed12e2816ce8864d5cf0ab831" proved="false" expanded="true" shape="amin_distaConsV2V0aConsV2V1V3Iamin_distV0V1V3F">
+ <file name="../edit_distance.mlw" verified="true" expanded="false">
+  <theory name="Word" verified="true" expanded="false">
+   <goal name="first_last_explicit" sum="f2e89ddf4b2be8dc8d7a05fdca747b1c" proved="true" expanded="false" shape="ainfix =ainfix ++abut_lastV1V0aConsalast_charV1V0aNilaConsV1V0F">
+    <proof prover="coq" timelimit="10" edited="edit_distance_Word_first_last_explicit_1.v" obsolete="false">
+     <result status="valid" time="0.67"/>
+    </proof>
+   </goal>
+   <goal name="first_last" sum="92d066e416bf5a837d3259d2a67189d1" proved="true" expanded="false" shape="ainfix =alengthV2alengthV1Aainfix =ainfix ++V2aConsV3aNilaConsV0V1EF">
+    <proof prover="coq" timelimit="10" edited="edit_distance_Word_first_last_1.v" obsolete="false">
+     <result status="valid" time="0.59"/>
+    </proof>
+   </goal>
+   <goal name="key_lemma_right" sum="c618ca07adc8a26c676dfd82d22f9ed6" proved="true" expanded="false" shape="ainfix <=ainfix +V7alengthV5ainfix +V2c1AadistV6V4V7Aainfix =V0ainfix ++V5V6EIainfix =V1aConsV3V4FIadistV0V1V2F">
+    <proof prover="coq" timelimit="10" edited="edit_distance_Word_key_lemma_right_1.v" obsolete="false">
+     <result status="valid" time="0.67"/>
+    </proof>
+   </goal>
+   <goal name="dist_symetry" sum="8ac1f467726d438111fbe5b3a6e7d654" proved="true" expanded="false" shape="adistV1V0V2IadistV0V1V2F">
+    <proof prover="coq" timelimit="10" edited="edit_distance_Word_dist_symetry_1.v" obsolete="false">
+     <result status="valid" time="0.57"/>
+    </proof>
+   </goal>
+   <goal name="key_lemma_left" sum="83a00e37099a61e949f2acb824f854ca" proved="true" expanded="false" shape="ainfix <=ainfix +V6alengthV4ainfix +V2c1AadistV0V5V6Aainfix =V1ainfix ++V4V5EIadistaConsV3V0V1V2F">
+    <proof prover="z3" timelimit="10" edited="" obsolete="false">
+     <result status="valid" time="0.12"/>
+    </proof>
+   </goal>
+   <goal name="dist_concat_left" sum="107eb39afb9ff2776b9e4d3470d378f7" proved="true" expanded="false" shape="adistainfix ++V0V1V2ainfix +alengthV0V3IadistV1V2V3F">
+    <proof prover="coq" timelimit="10" edited="edit_distance_Word_dist_concat_left_1.v" obsolete="false">
+     <result status="valid" time="0.59"/>
+    </proof>
+   </goal>
+   <goal name="dist_concat_right" sum="39ae0e182374dcd9caa813d9f373b3a7" proved="true" expanded="false" shape="adistV1ainfix ++V0V2ainfix +alengthV0V3IadistV1V2V3F">
+    <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
+     <result status="valid" time="0.04"/>
+    </proof>
+   </goal>
+   <goal name="min_dist_equal" sum="7f4ca766ae9ec84190c6fd804d472971" proved="true" expanded="false" shape="amin_distaConsV2V0aConsV2V1V3Iamin_distV0V1V3F">
+    <proof prover="coq" timelimit="10" edited="edit_distance_Word_min_dist_equal_1.v" obsolete="false">
+     <result status="valid" time="0.67"/>
+    </proof>
    </goal>
-   <goal name="min_dist_diff" sum="4015bdb0b34c4343107f056d5e1ed1f9" proved="false" expanded="true" shape="amin_distaConsV2V0aConsV3V1ainfix +aminV4V5c1Iamin_distV0aConsV3V1V4Iamin_distaConsV2V0V1V5Iainfix =V2V3NF">
+   <goal name="min_dist_diff" sum="7dcf33667e57a730bd647227058aa252" proved="true" expanded="false" shape="amin_distaConsV2V0aConsV3V1ainfix +aminV4V5c1Iamin_distV0aConsV3V1V4Iamin_distaConsV2V0V1V5Iainfix =V2V3NF">
+    <proof prover="coq" timelimit="10" edited="edit_distance_Word_min_dist_diff_1.v" obsolete="false">
+     <result status="valid" time="0.66"/>
+    </proof>
    </goal>
-   <goal name="min_dist_eps" sum="0b1723159f9fb8ec3f503bb7e0cb16f4" proved="true" expanded="true" shape="amin_distaConsV1V0aNilainfix +V2c1Iamin_distV0aNilV2F">
+   <goal name="min_dist_eps" sum="85566f1f6c4084974df6132552f2c7e7" proved="true" expanded="false" shape="amin_distaConsV1V0aNilainfix +V2c1Iamin_distV0aNilV2F">
     <proof prover="coq" timelimit="20" edited="edit_distance_Word_min_dist_eps_1.v" obsolete="false">
-     <result status="valid" time="0.64"/>
+     <result status="valid" time="0.66"/>
     </proof>
    </goal>
-   <goal name="min_dist_eps_length" sum="c2c90d9dc7c409bb88ee27f06189633f" proved="true" expanded="true" shape="amin_distaNilV0alengthV0F">
+   <goal name="min_dist_eps_length" sum="361dc0bb5844a317a52c6754352ca181" proved="true" expanded="false" shape="amin_distaNilV0alengthV0F">
     <proof prover="coq" timelimit="20" edited="edit_distance_Word_min_dist_eps_length_1.v" obsolete="false">
-     <result status="valid" time="0.67"/>
+     <result status="valid" time="0.69"/>
     </proof>
    </goal>
   </theory>
-  <theory name="WP EditDistance" verified="true" expanded="true">
-   <goal name="suffix_length" sum="4d219c5494bb9a132e2bcd56ccd675e4" proved="true" expanded="true" shape="ainfix =alengthasuffixV0V1ainfix -alengthV0V1Iainfix <=V1alengthV0Aainfix <=c0V1F">
+  <theory name="WP EditDistance" verified="true" expanded="false">
+   <goal name="suffix_length" sum="49d4196e7d96d9844d50819ec63953e5" proved="true" expanded="false" shape="ainfix =alengthasuffixV0V1ainfix -alengthV0V1Iainfix <=V1alengthV0Aainfix <=c0V1F">
     <proof prover="coq" timelimit="20" edited="edit_distance_WP_EditDistance_suffix_length_1.v" obsolete="false">
-     <result status="valid" time="0.73"/>
+     <result status="valid" time="0.78"/>
     </proof>
    </goal>
-   <goal name="WP_parameter distance" expl="correctness of parameter distance" sum="8a605e9a5c20c02132987dd701850a28" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV7c0Aainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V8agetV7V8Iainfix <=V8V1Aainfix <=c0V8FAamin_distasuffixV5ainfix +ainfix +V9c-1c1asuffixV4V13agetV12V13Iainfix <=V13V1Aainfix <=c0V13FIamin_distasuffixV5ainfix +V9c1asuffixV4ainfix +ainfix +c0c-1c1V11Aamin_distasuffixV5ainfix +V9c1asuffixV4V14agetV12V14Iainfix <=V14ainfix +c0c-1Aainfix <=c0V14FAamin_distasuffixV5V9asuffixV4V15agetV12V15Iainfix <=V15V1Aainfix <ainfix +c0c-1V15FAiainfix =agetV3V9agetV2V16amin_distasuffixV5ainfix +V9c1asuffixV4ainfix +ainfix +V16c-1c1V17Aamin_distasuffixV5ainfix +V9c1asuffixV4V19agetV18V19Iainfix <=V19ainfix +V16c-1Aainfix <=c0V19FAamin_distasuffixV5V9asuffixV4V20agetV18V20Iainfix <=V20V1Aainfix <ainfix +V16c-1V20FIainfix =V18asetV12V16V11FAainfix <V16ainfix +V1c1Aainfix <=c0V16amin_distasuffixV5ainfix +V9c1asuffixV4ainfix +ainfix +V16c-1c1V17Aamin_distasuffixV5ainfix +V9c1asuffixV4V22agetV21V22Iainfix <=V22ainfix +V16c-1Aainfix <=c0V22FAamin_distasuffixV5V9asuffixV4V23agetV21V23Iainfix <=V23V1Aainfix <ainfix +V16c-1V23FIainfix =V21asetV12V16ainfix +aminagetV12V16agetV12ainfix +V16c1c1FAainfix <V16ainfix +V1c1Aainfix <=c0V16Aainfix <ainfix +V16c1ainfix +V1c1Aainfix <=c0ainfix +V16c1Aainfix <V16ainfix +V1c1Aainfix <=c0V16Aainfix <V16V1Aainfix <=c0V16Aainfix <V9V0Aainfix <=c0V9Iainfix =V17agetV12V16FAainfix <V16ainfix +V1c1Aainfix <=c0V16Iamin_distasuffixV5ainfix +V9c1asuffixV4ainfix +V16c1V11Aamin_distasuffixV5ainfix +V9c1asuffixV4V24agetV12V24Iainfix <=V24V16Aainfix <=c0V24FAamin_distasuffixV5V9asuffixV4V25agetV12V25Iainfix <=V25V1Aainfix <V16V25FIainfix >=V16c0Aainfix >=ainfix -V1c1V16FFFAamin_distasuffixV5ainfix +V9c1asuffixV4ainfix +ainfix -V1c1c1agetV7V1Aamin_distasuffixV5ainfix +V9c1asuffixV4V26agetV10V26Iainfix <=V26ainfix -V1c1Aainfix <=c0V26FAamin_distasuffixV5V9asuffixV4V27agetV10V27Iainfix <=V27V1Aainfix <ainfix -V1c1V27FIainfix >=ainfix -V1c1c0Aamin_distasuffixV5ainfix +ainfix +V9c-1c1asuffixV4V28agetV10V28Iainfix <=V28V1Aainfix <=c0V28FIainfix <ainfix -V1c1c0Iainfix =V10asetV7V1ainfix +agetV7V1c1FAainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V9c1asuffixV4V29agetV7V29Iainfix <=V29V1Aainfix <=c0V29FIainfix >=V9c0Aainfix >=ainfix -V0c1V9FFAamin_distasuffixV5ainfix +ainfix -V0c1c1asuffixV4V30agetV6V30Iainfix <=V30V1Aainfix <=c0V30FIainfix >=ainfix -V0c1c0Aamin_distasuffixV5c0asuffixV4c0agetV6c0Aainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix =agetV6V31ainfix -V1V31Iainfix <V31ainfix +V1c1Aainfix <=c0V31FAainfix =agetV33V34ainfix -V1V34Iainfix <V34ainfix +V32c1Aainfix <=c0V34FIainfix =V33asetV6V32ainfix -V1V32FAainfix <V32ainfix +V1c1Aainfix <=c0V32Iainfix =agetV6V35ainfix -V1V35Iainfix <V35V32Aainfix <=c0V35FIainfix <=V32V1Aainfix <=c0V32FFAainfix =agetaconstc0V36ainfix -V1V36Iainfix <V36c0Aainfix <=c0V36FIainfix <=c0V1Aamin_distasuffixV5c0asuffixV4c0agetV37c0Aainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V38agetV37V38Iainfix <=V38V1Aainfix <=c0V38FAamin_distasuffixV5ainfix +ainfix +V39c-1c1asuffixV4V43agetV42V43Iainfix <=V43V1Aainfix <=c0V43FIamin_distasuffixV5ainfix +V39c1asuffixV4ainfix +ainfix +c0c-1c1V41Aamin_distasuffixV5ainfix +V39c1asuffixV4V44agetV42V44Iainfix <=V44ainfix +c0c-1Aainfix <=c0V44FAamin_distasuffixV5V39asuffixV4V45agetV42V45Iainfix <=V45V1Aainfix <ainfix +c0c-1V45FAiainfix =agetV3V39agetV2V46amin_distasuffixV5ainfix +V39c1asuffixV4ainfix +ainfix +V46c-1c1V47Aamin_distasuffixV5ainfix +V39c1asuffixV4V49agetV48V49Iainfix <=V49ainfix +V46c-1Aainfix <=c0V49FAamin_distasuffixV5V39asuffixV4V50agetV48V50Iainfix <=V50V1Aainfix <ainfix +V46c-1V50FIainfix =V48asetV42V46V41FAainfix <V46ainfix +V1c1Aainfix <=c0V46amin_distasuffixV5ainfix +V39c1asuffixV4ainfix +ainfix +V46c-1c1V47Aamin_distasuffixV5ainfix +V39c1asuffixV4V52agetV51V52Iainfix <=V52ainfix +V46c-1Aainfix <=c0V52FAamin_distasuffixV5V39asuffixV4V53agetV51V53Iainfix <=V53V1Aainfix <ainfix +V46c-1V53FIainfix =V51asetV42V46ainfix +aminagetV42V46agetV42ainfix +V46c1c1FAainfix <V46ainfix +V1c1Aainfix <=c0V46Aainfix <ainfix +V46c1ainfix +V1c1Aainfix <=c0ainfix +V46c1Aainfix <V46ainfix +V1c1Aainfix <=c0V46Aainfix <V46V1Aainfix <=c0V46Aainfix <V39V0Aainfix <=c0V39Iainfix =V47agetV42V46FAainfix <V46ainfix +V1c1Aainfix <=c0V46Iamin_distasuffixV5ainfix +V39c1asuffixV4ainfix +V46c1V41Aamin_distasuffixV5ainfix +V39c1asuffixV4V54agetV42V54Iainfix <=V54V46Aainfix <=c0V54FAamin_distasuffixV5V39asuffixV4V55agetV42V55Iainfix <=V55V1Aainfix <V46V55FIainfix >=V46c0Aainfix >=ainfix -V1c1V46FFFAamin_distasuffixV5ainfix +V39c1asuffixV4ainfix +ainfix -V1c1c1agetV37V1Aamin_distasuffixV5ainfix +V39c1asuffixV4V56agetV40V56Iainfix <=V56ainfix -V1c1Aainfix <=c0V56FAamin_distasuffixV5V39asuffixV4V57agetV40V57Iainfix <=V57V1Aainfix <ainfix -V1c1V57FIainfix >=ainfix -V1c1c0Aamin_distasuffixV5ainfix +ainfix +V39c-1c1asuffixV4V58agetV40V58Iainfix <=V58V1Aainfix <=c0V58FIainfix <ainfix -V1c1c0Iainfix =V40asetV37V1ainfix +agetV37V1c1FAainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V39c1asuffixV4V59agetV37V59Iainfix <=V59V1Aainfix <=c0V59FIainfix >=V39c0Aainfix >=ainfix -V0c1V39FFAamin_distasuffixV5ainfix +ainfix -V0c1c1asuffixV4V60agetaconstc0V60Iainfix <=V60V1Aainfix <=c0V60FIainfix >=ainfix -V0c1c0Aamin_distasuffixV5c0asuffixV4c0agetaconstc0c0Aainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix >c0V1Aainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
-    <transf name="split_goal" proved="true" expanded="true">
-     <goal name="WP_parameter distance.1" expl="precondition" sum="482ce4a63d91491d0b2069818a38675d" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+   <goal name="WP_parameter distance" expl="correctness of parameter distance" sum="f207722c1f131fd039fbadd92e9fb5a7" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV7c0Aainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V8agetV7V8Iainfix <=V8V1Aainfix <=c0V8FAamin_distasuffixV5ainfix +ainfix +V9c-1c1asuffixV4V13agetV12V13Iainfix <=V13V1Aainfix <=c0V13FIamin_distasuffixV5ainfix +V9c1asuffixV4ainfix +ainfix +c0c-1c1V11Aamin_distasuffixV5ainfix +V9c1asuffixV4V14agetV12V14Iainfix <=V14ainfix +c0c-1Aainfix <=c0V14FAamin_distasuffixV5V9asuffixV4V15agetV12V15Iainfix <=V15V1Aainfix <ainfix +c0c-1V15FAiainfix =agetV3V9agetV2V16amin_distasuffixV5ainfix +V9c1asuffixV4ainfix +ainfix +V16c-1c1V17Aamin_distasuffixV5ainfix +V9c1asuffixV4V19agetV18V19Iainfix <=V19ainfix +V16c-1Aainfix <=c0V19FAamin_distasuffixV5V9asuffixV4V20agetV18V20Iainfix <=V20V1Aainfix <ainfix +V16c-1V20FIainfix =V18asetV12V16V11FAainfix <V16ainfix +V1c1Aainfix <=c0V16amin_distasuffixV5ainfix +V9c1asuffixV4ainfix +ainfix +V16c-1c1V17Aamin_distasuffixV5ainfix +V9c1asuffixV4V22agetV21V22Iainfix <=V22ainfix +V16c-1Aainfix <=c0V22FAamin_distasuffixV5V9asuffixV4V23agetV21V23Iainfix <=V23V1Aainfix <ainfix +V16c-1V23FIainfix =V21asetV12V16ainfix +aminagetV12V16agetV12ainfix +V16c1c1FAainfix <V16ainfix +V1c1Aainfix <=c0V16Aainfix <ainfix +V16c1ainfix +V1c1Aainfix <=c0ainfix +V16c1Aainfix <V16ainfix +V1c1Aainfix <=c0V16Aainfix <V16V1Aainfix <=c0V16Aainfix <V9V0Aainfix <=c0V9Iainfix =V17agetV12V16FAainfix <V16ainfix +V1c1Aainfix <=c0V16Iamin_distasuffixV5ainfix +V9c1asuffixV4ainfix +V16c1V11Aamin_distasuffixV5ainfix +V9c1asuffixV4V24agetV12V24Iainfix <=V24V16Aainfix <=c0V24FAamin_distasuffixV5V9asuffixV4V25agetV12V25Iainfix <=V25V1Aainfix <V16V25FIainfix >=V16c0Aainfix >=ainfix -V1c1V16FFFAamin_distasuffixV5ainfix +V9c1asuffixV4ainfix +ainfix -V1c1c1agetV7V1Aamin_distasuffixV5ainfix +V9c1asuffixV4V26agetV10V26Iainfix <=V26ainfix -V1c1Aainfix <=c0V26FAamin_distasuffixV5V9asuffixV4V27agetV10V27Iainfix <=V27V1Aainfix <ainfix -V1c1V27FIainfix >=ainfix -V1c1c0Aamin_distasuffixV5ainfix +ainfix +V9c-1c1asuffixV4V28agetV10V28Iainfix <=V28V1Aainfix <=c0V28FIainfix <ainfix -V1c1c0Iainfix =V10asetV7V1ainfix +agetV7V1c1FAainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V9c1asuffixV4V29agetV7V29Iainfix <=V29V1Aainfix <=c0V29FIainfix >=V9c0Aainfix >=ainfix -V0c1V9FFAamin_distasuffixV5ainfix +ainfix -V0c1c1asuffixV4V30agetV6V30Iainfix <=V30V1Aainfix <=c0V30FIainfix >=ainfix -V0c1c0Aamin_distasuffixV5c0asuffixV4c0agetV6c0Aainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix =agetV6V31ainfix -V1V31Iainfix <V31ainfix +V1c1Aainfix <=c0V31FAainfix =agetV33V34ainfix -V1V34Iainfix <V34ainfix +V32c1Aainfix <=c0V34FIainfix =V33asetV6V32ainfix -V1V32FAainfix <V32ainfix +V1c1Aainfix <=c0V32Iainfix =agetV6V35ainfix -V1V35Iainfix <V35V32Aainfix <=c0V35FIainfix <=V32V1Aainfix <=c0V32FFAainfix =agetaconstc0V36ainfix -V1V36Iainfix <V36c0Aainfix <=c0V36FIainfix <=c0V1Aamin_distasuffixV5c0asuffixV4c0agetV37c0Aainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V38agetV37V38Iainfix <=V38V1Aainfix <=c0V38FAamin_distasuffixV5ainfix +ainfix +V39c-1c1asuffixV4V43agetV42V43Iainfix <=V43V1Aainfix <=c0V43FIamin_distasuffixV5ainfix +V39c1asuffixV4ainfix +ainfix +c0c-1c1V41Aamin_distasuffixV5ainfix +V39c1asuffixV4V44agetV42V44Iainfix <=V44ainfix +c0c-1Aainfix <=c0V44FAamin_distasuffixV5V39asuffixV4V45agetV42V45Iainfix <=V45V1Aainfix <ainfix +c0c-1V45FAiainfix =agetV3V39agetV2V46amin_distasuffixV5ainfix +V39c1asuffixV4ainfix +ainfix +V46c-1c1V47Aamin_distasuffixV5ainfix +V39c1asuffixV4V49agetV48V49Iainfix <=V49ainfix +V46c-1Aainfix <=c0V49FAamin_distasuffixV5V39asuffixV4V50agetV48V50Iainfix <=V50V1Aainfix <ainfix +V46c-1V50FIainfix =V48asetV42V46V41FAainfix <V46ainfix +V1c1Aainfix <=c0V46amin_distasuffixV5ainfix +V39c1asuffixV4ainfix +ainfix +V46c-1c1V47Aamin_distasuffixV5ainfix +V39c1asuffixV4V52agetV51V52Iainfix <=V52ainfix +V46c-1Aainfix <=c0V52FAamin_distasuffixV5V39asuffixV4V53agetV51V53Iainfix <=V53V1Aainfix <ainfix +V46c-1V53FIainfix =V51asetV42V46ainfix +aminagetV42V46agetV42ainfix +V46c1c1FAainfix <V46ainfix +V1c1Aainfix <=c0V46Aainfix <ainfix +V46c1ainfix +V1c1Aainfix <=c0ainfix +V46c1Aainfix <V46ainfix +V1c1Aainfix <=c0V46Aainfix <V46V1Aainfix <=c0V46Aainfix <V39V0Aainfix <=c0V39Iainfix =V47agetV42V46FAainfix <V46ainfix +V1c1Aainfix <=c0V46Iamin_distasuffixV5ainfix +V39c1asuffixV4ainfix +V46c1V41Aamin_distasuffixV5ainfix +V39c1asuffixV4V54agetV42V54Iainfix <=V54V46Aainfix <=c0V54FAamin_distasuffixV5V39asuffixV4V55agetV42V55Iainfix <=V55V1Aainfix <V46V55FIainfix >=V46c0Aainfix >=ainfix -V1c1V46FFFAamin_distasuffixV5ainfix +V39c1asuffixV4ainfix +ainfix -V1c1c1agetV37V1Aamin_distasuffixV5ainfix +V39c1asuffixV4V56agetV40V56Iainfix <=V56ainfix -V1c1Aainfix <=c0V56FAamin_distasuffixV5V39asuffixV4V57agetV40V57Iainfix <=V57V1Aainfix <ainfix -V1c1V57FIainfix >=ainfix -V1c1c0Aamin_distasuffixV5ainfix +ainfix +V39c-1c1asuffixV4V58agetV40V58Iainfix <=V58V1Aainfix <=c0V58FIainfix <ainfix -V1c1c0Iainfix =V40asetV37V1ainfix +agetV37V1c1FAainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V39c1asuffixV4V59agetV37V59Iainfix <=V59V1Aainfix <=c0V59FIainfix >=V39c0Aainfix >=ainfix -V0c1V39FFAamin_distasuffixV5ainfix +ainfix -V0c1c1asuffixV4V60agetaconstc0V60Iainfix <=V60V1Aainfix <=c0V60FIainfix >=ainfix -V0c1c0Aamin_distasuffixV5c0asuffixV4c0agetaconstc0c0Aainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix >c0V1Aainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+    <transf name="split_goal" proved="true" expanded="false">
+     <goal name="WP_parameter distance.1" expl="precondition" sum="c9910924b74765215fb81ee8dca23454" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+       <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.2" expl="precondition" sum="057f96a39d96bcce1b7f7b65e718f669" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.2" expl="precondition" sum="ea10d52917d571033195cc16831ee35d" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.3" expl="normal postcondition" sum="9ae036c1975202482cc0a54e929de0be" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetaconstc0c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.3" expl="normal postcondition" sum="9af015fd5bcc839d05cede4ad5a55b19" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetaconstc0c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.4" expl="for loop initialization" sum="2525bcb1b12a7360b21c9e62a3313747" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix -V0c1c1asuffixV4V6agetaconstc0V6Iainfix <=V6V1Aainfix <=c0V6FIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.4" expl="for loop initialization" sum="25ee5c7b6f1b8b99be55096911033922" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix -V0c1c1asuffixV4V6agetaconstc0V6Iainfix <=V6V1Aainfix <=c0V6FIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.5" expl="for loop preservation" sum="28bfb31792785bf04a6307d5a0a0f00c" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V7c-1c1asuffixV4V11agetV10V11Iainfix <=V11V1Aainfix <=c0V11FIamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +c0c-1c1V9Aamin_distasuffixV5ainfix +V7c1asuffixV4V12agetV10V12Iainfix <=V12ainfix +c0c-1Aainfix <=c0V12FAamin_distasuffixV5V7asuffixV4V13agetV10V13Iainfix <=V13V1Aainfix <ainfix +c0c-1V13FAiainfix =agetV3V7agetV2V14amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +V14c-1c1V15Aamin_distasuffixV5ainfix +V7c1asuffixV4V17agetV16V17Iainfix <=V17ainfix +V14c-1Aainfix <=c0V17FAamin_distasuffixV5V7asuffixV4V18agetV16V18Iainfix <=V18V1Aainfix <ainfix +V14c-1V18FIainfix =V16asetV10V14V9FAainfix <V14ainfix +V1c1Aainfix <=c0V14amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +V14c-1c1V15Aamin_distasuffixV5ainfix +V7c1asuffixV4V20agetV19V20Iainfix <=V20ainfix +V14c-1Aainfix <=c0V20FAamin_distasuffixV5V7asuffixV4V21agetV19V21Iainfix <=V21V1Aainfix <ainfix +V14c-1V21FIainfix =V19asetV10V14ainfix +aminagetV10V14agetV10ainfix +V14c1c1FAainfix <V14ainfix +V1c1Aainfix <=c0V14Aainfix <ainfix +V14c1ainfix +V1c1Aainfix <=c0ainfix +V14c1Aainfix <V14ainfix +V1c1Aainfix <=c0V14Aainfix <V14V1Aainfix <=c0V14Aainfix <V7V0Aainfix <=c0V7Iainfix =V15agetV10V14FAainfix <V14ainfix +V1c1Aainfix <=c0V14Iamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +V14c1V9Aamin_distasuffixV5ainfix +V7c1asuffixV4V22agetV10V22Iainfix <=V22V14Aainfix <=c0V22FAamin_distasuffixV5V7asuffixV4V23agetV10V23Iainfix <=V23V1Aainfix <V14V23FIainfix >=V14c0Aainfix >=ainfix -V1c1V14FFFAamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix -V1c1c1agetV6V1Aamin_distasuffixV5ainfix +V7c1asuffixV4V24agetV8V24Iainfix <=V24ainfix -V1c1Aainfix <=c0V24FAamin_distasuffixV5V7asuffixV4V25agetV8V25Iainfix <=V25V1Aainfix <ainfix -V1c1V25FIainfix >=ainfix -V1c1c0Aamin_distasuffixV5ainfix +ainfix +V7c-1c1asuffixV4V26agetV8V26Iainfix <=V26V1Aainfix <=c0V26FIainfix <ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FAainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V27agetV6V27Iainfix <=V27V1Aainfix <=c0V27FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
-      <transf name="split_goal" proved="true" expanded="true">
-       <goal name="WP_parameter distance.5.1" expl="for loop preservation" sum="173e25f2fbfb94fd4f27e448346cab7e" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V8agetV6V8Iainfix <=V8V1Aainfix <=c0V8FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.5" expl="for loop preservation" sum="4e42f5c7d6fd7b597ade4c4b0328533e" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V7c-1c1asuffixV4V11agetV10V11Iainfix <=V11V1Aainfix <=c0V11FIamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +c0c-1c1V9Aamin_distasuffixV5ainfix +V7c1asuffixV4V12agetV10V12Iainfix <=V12ainfix +c0c-1Aainfix <=c0V12FAamin_distasuffixV5V7asuffixV4V13agetV10V13Iainfix <=V13V1Aainfix <ainfix +c0c-1V13FAiainfix =agetV3V7agetV2V14amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +V14c-1c1V15Aamin_distasuffixV5ainfix +V7c1asuffixV4V17agetV16V17Iainfix <=V17ainfix +V14c-1Aainfix <=c0V17FAamin_distasuffixV5V7asuffixV4V18agetV16V18Iainfix <=V18V1Aainfix <ainfix +V14c-1V18FIainfix =V16asetV10V14V9FAainfix <V14ainfix +V1c1Aainfix <=c0V14amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +V14c-1c1V15Aamin_distasuffixV5ainfix +V7c1asuffixV4V20agetV19V20Iainfix <=V20ainfix +V14c-1Aainfix <=c0V20FAamin_distasuffixV5V7asuffixV4V21agetV19V21Iainfix <=V21V1Aainfix <ainfix +V14c-1V21FIainfix =V19asetV10V14ainfix +aminagetV10V14agetV10ainfix +V14c1c1FAainfix <V14ainfix +V1c1Aainfix <=c0V14Aainfix <ainfix +V14c1ainfix +V1c1Aainfix <=c0ainfix +V14c1Aainfix <V14ainfix +V1c1Aainfix <=c0V14Aainfix <V14V1Aainfix <=c0V14Aainfix <V7V0Aainfix <=c0V7Iainfix =V15agetV10V14FAainfix <V14ainfix +V1c1Aainfix <=c0V14Iamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +V14c1V9Aamin_distasuffixV5ainfix +V7c1asuffixV4V22agetV10V22Iainfix <=V22V14Aainfix <=c0V22FAamin_distasuffixV5V7asuffixV4V23agetV10V23Iainfix <=V23V1Aainfix <V14V23FIainfix >=V14c0Aainfix >=ainfix -V1c1V14FFFAamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix -V1c1c1agetV6V1Aamin_distasuffixV5ainfix +V7c1asuffixV4V24agetV8V24Iainfix <=V24ainfix -V1c1Aainfix <=c0V24FAamin_distasuffixV5V7asuffixV4V25agetV8V25Iainfix <=V25V1Aainfix <ainfix -V1c1V25FIainfix >=ainfix -V1c1c0Aamin_distasuffixV5ainfix +ainfix +V7c-1c1asuffixV4V26agetV8V26Iainfix <=V26V1Aainfix <=c0V26FIainfix <ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FAainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V27agetV6V27Iainfix <=V27V1Aainfix <=c0V27FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+      <transf name="split_goal" proved="true" expanded="false">
+       <goal name="WP_parameter distance.5.1" expl="for loop preservation" sum="eb4fd3f7a6b3904be6e1cd7a845500c2" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V8agetV6V8Iainfix <=V8V1Aainfix <=c0V8FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.5.2" expl="for loop preservation" sum="a58536bd9183d46f98b7415c7a2a1b29" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V8agetV6V8Iainfix <=V8V1Aainfix <=c0V8FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.5.2" expl="for loop preservation" sum="e5422b6a09370c076fbf1e708e4cc509" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V8agetV6V8Iainfix <=V8V1Aainfix <=c0V8FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.5.3" expl="for loop preservation" sum="a7c38461dc9744059ae56f0b75d5a310" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V8agetV6V8Iainfix <=V8V1Aainfix <=c0V8FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.5.3" expl="for loop preservation" sum="ebd86af395de008dcb678b718091bf37" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V8agetV6V8Iainfix <=V8V1Aainfix <=c0V8FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.5.4" expl="for loop preservation" sum="f6adcd2670c299f9ef50fdbca89cde90" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V7c-1c1asuffixV4V9agetV8V9Iainfix <=V9V1Aainfix <=c0V9FIainfix <ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V10agetV6V10Iainfix <=V10V1Aainfix <=c0V10FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.5.4" expl="for loop preservation" sum="ec1a62c0adf7a9e2d6d0a25e7c052c93" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V7c-1c1asuffixV4V9agetV8V9Iainfix <=V9V1Aainfix <=c0V9FIainfix <ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V10agetV6V10Iainfix <=V10V1Aainfix <=c0V10FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.5.5" expl="for loop preservation" sum="df16b3564e58b7a2f4bd746b5402f818" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix -V1c1c1agetV6V1Aamin_distasuffixV5ainfix +V7c1asuffixV4V9agetV8V9Iainfix <=V9ainfix -V1c1Aainfix <=c0V9FAamin_distasuffixV5V7asuffixV4V10agetV8V10Iainfix <=V10V1Aainfix <ainfix -V1c1V10FIainfix >=ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V11agetV6V11Iainfix <=V11V1Aainfix <=c0V11FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.5.5" expl="for loop preservation" sum="b2684ca59ef0428b7975bf768842fa73" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix -V1c1c1agetV6V1Aamin_distasuffixV5ainfix +V7c1asuffixV4V9agetV8V9Iainfix <=V9ainfix -V1c1Aainfix <=c0V9FAamin_distasuffixV5V7asuffixV4V10agetV8V10Iainfix <=V10V1Aainfix <ainfix -V1c1V10FIainfix >=ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V11agetV6V11Iainfix <=V11V1Aainfix <=c0V11FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.01"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.5.6" expl="for loop preservation" sum="9a917f603e7affca11b5496af3c7c3b4" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3iainfix =agetV3V7agetV2V11amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +V11c-1c1V12Aamin_distasuffixV5ainfix +V7c1asuffixV4V14agetV13V14Iainfix <=V14ainfix +V11c-1Aainfix <=c0V14FAamin_distasuffixV5V7asuffixV4V15agetV13V15Iainfix <=V15V1Aainfix <ainfix +V11c-1V15FIainfix =V13asetV10V11V9FAainfix <V11ainfix +V1c1Aainfix <=c0V11amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +V11c-1c1V12Aamin_distasuffixV5ainfix +V7c1asuffixV4V17agetV16V17Iainfix <=V17ainfix +V11c-1Aainfix <=c0V17FAamin_distasuffixV5V7asuffixV4V18agetV16V18Iainfix <=V18V1Aainfix <ainfix +V11c-1V18FIainfix =V16asetV10V11ainfix +aminagetV10V11agetV10ainfix +V11c1c1FAainfix <V11ainfix +V1c1Aainfix <=c0V11Aainfix <ainfix +V11c1ainfix +V1c1Aainfix <=c0ainfix +V11c1Aainfix <V11ainfix +V1c1Aainfix <=c0V11Aainfix <V11V1Aainfix <=c0V11Aainfix <V7V0Aainfix <=c0V7Iainfix =V12agetV10V11FAainfix <V11ainfix +V1c1Aainfix <=c0V11Iamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +V11c1V9Aamin_distasuffixV5ainfix +V7c1asuffixV4V19agetV10V19Iainfix <=V19V11Aainfix <=c0V19FAamin_distasuffixV5V7asuffixV4V20agetV10V20Iainfix <=V20V1Aainfix <V11V20FIainfix >=V11c0Aainfix >=ainfix -V1c1V11FFFIainfix >=ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V21agetV6V21Iainfix <=V21V1Aainfix <=c0V21FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.5.6" expl="for loop preservation" sum="02e29e37dbd84fb329d291f760e2c773" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3iainfix =agetV3V7agetV2V11amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +V11c-1c1V12Aamin_distasuffixV5ainfix +V7c1asuffixV4V14agetV13V14Iainfix <=V14ainfix +V11c-1Aainfix <=c0V14FAamin_distasuffixV5V7asuffixV4V15agetV13V15Iainfix <=V15V1Aainfix <ainfix +V11c-1V15FIainfix =V13asetV10V11V9FAainfix <V11ainfix +V1c1Aainfix <=c0V11amin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +V11c-1c1V12Aamin_distasuffixV5ainfix +V7c1asuffixV4V17agetV16V17Iainfix <=V17ainfix +V11c-1Aainfix <=c0V17FAamin_distasuffixV5V7asuffixV4V18agetV16V18Iainfix <=V18V1Aainfix <ainfix +V11c-1V18FIainfix =V16asetV10V11ainfix +aminagetV10V11agetV10ainfix +V11c1c1FAainfix <V11ainfix +V1c1Aainfix <=c0V11Aainfix <ainfix +V11c1ainfix +V1c1Aainfix <=c0ainfix +V11c1Aainfix <V11ainfix +V1c1Aainfix <=c0V11Aainfix <V11V1Aainfix <=c0V11Aainfix <V7V0Aainfix <=c0V7Iainfix =V12agetV10V11FAainfix <V11ainfix +V1c1Aainfix <=c0V11Iamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +V11c1V9Aamin_distasuffixV5ainfix +V7c1asuffixV4V19agetV10V19Iainfix <=V19V11Aainfix <=c0V19FAamin_distasuffixV5V7asuffixV4V20agetV10V20Iainfix <=V20V1Aainfix <V11V20FIainfix >=V11c0Aainfix >=ainfix -V1c1V11FFFIainfix >=ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V21agetV6V21Iainfix <=V21V1Aainfix <=c0V21FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
          <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.5.7" expl="for loop preservation" sum="890c1087e856e6784bea7f7fb6d782b2" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V7c-1c1asuffixV4V11agetV10V11Iainfix <=V11V1Aainfix <=c0V11FIamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +c0c-1c1V9Aamin_distasuffixV5ainfix +V7c1asuffixV4V12agetV10V12Iainfix <=V12ainfix +c0c-1Aainfix <=c0V12FAamin_distasuffixV5V7asuffixV4V13agetV10V13Iainfix <=V13V1Aainfix <ainfix +c0c-1V13FFFIainfix >=ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V14agetV6V14Iainfix <=V14V1Aainfix <=c0V14FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.5.7" expl="for loop preservation" sum="e67348b8cc9411584dcd5fc79bcb51ed" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V7c-1c1asuffixV4V11agetV10V11Iainfix <=V11V1Aainfix <=c0V11FIamin_distasuffixV5ainfix +V7c1asuffixV4ainfix +ainfix +c0c-1c1V9Aamin_distasuffixV5ainfix +V7c1asuffixV4V12agetV10V12Iainfix <=V12ainfix +c0c-1Aainfix <=c0V12FAamin_distasuffixV5V7asuffixV4V13agetV10V13Iainfix <=V13V1Aainfix <ainfix +c0c-1V13FFFIainfix >=ainfix -V1c1c0Iainfix =V8asetV6V1ainfix +agetV6V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V7c1asuffixV4V14agetV6V14Iainfix <=V14V1Aainfix <=c0V14FIainfix >=V7c0Aainfix >=ainfix -V0c1V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.03"/>
+         <result status="valid" time="0.02"/>
         </proof>
        </goal>
       </transf>
      </goal>
-     <goal name="WP_parameter distance.6" expl="precondition" sum="66f368b6b047a3a0a26224ef1c6c506b" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V7agetV6V7Iainfix <=V7V1Aainfix <=c0V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.6" expl="precondition" sum="54a149582064683a726b8e3b0b18672f" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V7agetV6V7Iainfix <=V7V1Aainfix <=c0V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+       <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.7" expl="normal postcondition" sum="0ecee843c99e1c903413c7ed8150429d" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV6c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V7agetV6V7Iainfix <=V7V1Aainfix <=c0V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.7" expl="normal postcondition" sum="caf2b7bd04b328cc5208a744df66851c" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV6c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V7agetV6V7Iainfix <=V7V1Aainfix <=c0V7FFIainfix >=ainfix -V0c1c0Iainfix >c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.8" expl="for loop initialization" sum="22677abb3494ce245a35b8ad386715bf" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix =agetaconstc0V6ainfix -V1V6Iainfix <V6c0Aainfix <=c0V6FIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.8" expl="for loop initialization" sum="cb54d62374c9e4503a8eb14c12ab0d15" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix =agetaconstc0V6ainfix -V1V6Iainfix <V6c0Aainfix <=c0V6FIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.9" expl="for loop preservation" sum="7c79fe48346041308ffbe873b5aca0c7" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix =agetV8V9ainfix -V1V9Iainfix <V9ainfix +V7c1Aainfix <=c0V9FIainfix =V8asetV6V7ainfix -V1V7FAainfix <V7ainfix +V1c1Aainfix <=c0V7Iainfix =agetV6V10ainfix -V1V10Iainfix <V10V7Aainfix <=c0V10FIainfix <=V7V1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
-      <transf name="split_goal" proved="true" expanded="true">
-       <goal name="WP_parameter distance.9.1" expl="for loop preservation" sum="43072d487fae532066ce52468729be3a" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V7ainfix +V1c1Aainfix <=c0V7Iainfix =agetV6V8ainfix -V1V8Iainfix <V8V7Aainfix <=c0V8FIainfix <=V7V1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.9" expl="for loop preservation" sum="4687d57419ae1e7e380c05ed32590bb7" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix =agetV8V9ainfix -V1V9Iainfix <V9ainfix +V7c1Aainfix <=c0V9FIainfix =V8asetV6V7ainfix -V1V7FAainfix <V7ainfix +V1c1Aainfix <=c0V7Iainfix =agetV6V10ainfix -V1V10Iainfix <V10V7Aainfix <=c0V10FIainfix <=V7V1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+      <transf name="split_goal" proved="true" expanded="false">
+       <goal name="WP_parameter distance.9.1" expl="for loop preservation" sum="19158c373209ee8d80a49b6df8dcc9c2" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V7ainfix +V1c1Aainfix <=c0V7Iainfix =agetV6V8ainfix -V1V8Iainfix <V8V7Aainfix <=c0V8FIainfix <=V7V1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.9.2" expl="for loop preservation" sum="60596c4c51f7b5944b196b73caa95f2d" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix =agetV8V9ainfix -V1V9Iainfix <V9ainfix +V7c1Aainfix <=c0V9FIainfix =V8asetV6V7ainfix -V1V7FIainfix <V7ainfix +V1c1Aainfix <=c0V7Iainfix =agetV6V10ainfix -V1V10Iainfix <V10V7Aainfix <=c0V10FIainfix <=V7V1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.9.2" expl="for loop preservation" sum="46592753b5540153ba96545159bcfef7" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix =agetV8V9ainfix -V1V9Iainfix <V9ainfix +V7c1Aainfix <=c0V9FIainfix =V8asetV6V7ainfix -V1V7FIainfix <V7ainfix +V1c1Aainfix <=c0V7Iainfix =agetV6V10ainfix -V1V10Iainfix <V10V7Aainfix <=c0V10FIainfix <=V7V1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
          <result status="valid" time="0.03"/>
         </proof>
        </goal>
       </transf>
      </goal>
-     <goal name="WP_parameter distance.10" expl="precondition" sum="c32b5bb92aa006791797cac1a9c1a5f4" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix =agetV6V7ainfix -V1V7Iainfix <V7ainfix +V1c1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.10" expl="precondition" sum="69e6f72cc0aa6f3f8a1c1d5abae58ac2" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix =agetV6V7ainfix -V1V7Iainfix <V7ainfix +V1c1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.11" expl="normal postcondition" sum="3bb84f4ea560aa03da294943cd3ee8ac" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV6c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix =agetV6V7ainfix -V1V7Iainfix <V7ainfix +V1c1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
-      <transf name="split_goal" proved="true" expanded="true">
-       <goal name="WP_parameter distance.11.1" expl="normal postcondition" sum="3bb84f4ea560aa03da294943cd3ee8ac" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV6c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix =agetV6V7ainfix -V1V7Iainfix <V7ainfix +V1c1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.11" expl="normal postcondition" sum="9e9313cf29a3a80e65f1ca86744de7fb" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV6c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix =agetV6V7ainfix -V1V7Iainfix <V7ainfix +V1c1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+      <transf name="split_goal" proved="true" expanded="false">
+       <goal name="WP_parameter distance.11.1" expl="normal postcondition" sum="9e9313cf29a3a80e65f1ca86744de7fb" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV6c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iainfix <ainfix -V0c1c0Iainfix =agetV6V7ainfix -V1V7Iainfix <V7ainfix +V1c1Aainfix <=c0V7FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.04"/>
+         <result status="valid" time="0.05"/>
         </proof>
        </goal>
       </transf>
      </goal>
-     <goal name="WP_parameter distance.12" expl="for loop initialization" sum="18ec0864fb86b0a3434bc020019c24c1" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix -V0c1c1asuffixV4V7agetV6V7Iainfix <=V7V1Aainfix <=c0V7FIainfix >=ainfix -V0c1c0Iainfix =agetV6V8ainfix -V1V8Iainfix <V8ainfix +V1c1Aainfix <=c0V8FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.12" expl="for loop initialization" sum="4c580212378d929d5c369c46cc8b88d0" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix -V0c1c1asuffixV4V7agetV6V7Iainfix <=V7V1Aainfix <=c0V7FIainfix >=ainfix -V0c1c0Iainfix =agetV6V8ainfix -V1V8Iainfix <V8ainfix +V1c1Aainfix <=c0V8FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-       <result status="valid" time="0.06"/>
+       <result status="valid" time="0.07"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.13" expl="for loop preservation" sum="af7d941a7e0cc4e4e5cd74be029995fd" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V12agetV11V12Iainfix <=V12V1Aainfix <=c0V12FIamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +c0c-1c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V13agetV11V13Iainfix <=V13ainfix +c0c-1Aainfix <=c0V13FAamin_distasuffixV5V8asuffixV4V14agetV11V14Iainfix <=V14V1Aainfix <ainfix +c0c-1V14FAiainfix =agetV3V8agetV2V15amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V15c-1c1V16Aamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV17V18Iainfix <=V18ainfix +V15c-1Aainfix <=c0V18FAamin_distasuffixV5V8asuffixV4V19agetV17V19Iainfix <=V19V1Aainfix <ainfix +V15c-1V19FIainfix =V17asetV11V15V10FAainfix <V15ainfix +V1c1Aainfix <=c0V15amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V15c-1c1V16Aamin_distasuffixV5ainfix +V8c1asuffixV4V21agetV20V21Iainfix <=V21ainfix +V15c-1Aainfix <=c0V21FAamin_distasuffixV5V8asuffixV4V22agetV20V22Iainfix <=V22V1Aainfix <ainfix +V15c-1V22FIainfix =V20asetV11V15ainfix +aminagetV11V15agetV11ainfix +V15c1c1FAainfix <V15ainfix +V1c1Aainfix <=c0V15Aainfix <ainfix +V15c1ainfix +V1c1Aainfix <=c0ainfix +V15c1Aainfix <V15ainfix +V1c1Aainfix <=c0V15Aainfix <V15V1Aainfix <=c0V15Aainfix <V8V0Aainfix <=c0V8Iainfix =V16agetV11V15FAainfix <V15ainfix +V1c1Aainfix <=c0V15Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V15c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V23agetV11V23Iainfix <=V23V15Aainfix <=c0V23FAamin_distasuffixV5V8asuffixV4V24agetV11V24Iainfix <=V24V1Aainfix <V15V24FIainfix >=V15c0Aainfix >=ainfix -V1c1V15FFFAamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix -V1c1c1agetV7V1Aamin_distasuffixV5ainfix +V8c1asuffixV4V25agetV9V25Iainfix <=V25ainfix -V1c1Aainfix <=c0V25FAamin_distasuffixV5V8asuffixV4V26agetV9V26Iainfix <=V26V1Aainfix <ainfix -V1c1V26FIainfix >=ainfix -V1c1c0Aamin_distasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V27agetV9V27Iainfix <=V27V1Aainfix <=c0V27FIainfix <ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FAainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V28agetV7V28Iainfix <=V28V1Aainfix <=c0V28FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V29ainfix -V1V29Iainfix <V29ainfix +V1c1Aainfix <=c0V29FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
-      <transf name="split_goal" proved="true" expanded="true">
-       <goal name="WP_parameter distance.13.1" expl="for loop preservation" sum="d009d3edbe03cedf1623a8677c8106cd" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V9agetV7V9Iainfix <=V9V1Aainfix <=c0V9FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V10ainfix -V1V10Iainfix <V10ainfix +V1c1Aainfix <=c0V10FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.13" expl="for loop preservation" sum="026e9d93a7e1c224de9a020b1e612acd" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V12agetV11V12Iainfix <=V12V1Aainfix <=c0V12FIamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +c0c-1c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V13agetV11V13Iainfix <=V13ainfix +c0c-1Aainfix <=c0V13FAamin_distasuffixV5V8asuffixV4V14agetV11V14Iainfix <=V14V1Aainfix <ainfix +c0c-1V14FAiainfix =agetV3V8agetV2V15amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V15c-1c1V16Aamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV17V18Iainfix <=V18ainfix +V15c-1Aainfix <=c0V18FAamin_distasuffixV5V8asuffixV4V19agetV17V19Iainfix <=V19V1Aainfix <ainfix +V15c-1V19FIainfix =V17asetV11V15V10FAainfix <V15ainfix +V1c1Aainfix <=c0V15amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V15c-1c1V16Aamin_distasuffixV5ainfix +V8c1asuffixV4V21agetV20V21Iainfix <=V21ainfix +V15c-1Aainfix <=c0V21FAamin_distasuffixV5V8asuffixV4V22agetV20V22Iainfix <=V22V1Aainfix <ainfix +V15c-1V22FIainfix =V20asetV11V15ainfix +aminagetV11V15agetV11ainfix +V15c1c1FAainfix <V15ainfix +V1c1Aainfix <=c0V15Aainfix <ainfix +V15c1ainfix +V1c1Aainfix <=c0ainfix +V15c1Aainfix <V15ainfix +V1c1Aainfix <=c0V15Aainfix <V15V1Aainfix <=c0V15Aainfix <V8V0Aainfix <=c0V8Iainfix =V16agetV11V15FAainfix <V15ainfix +V1c1Aainfix <=c0V15Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V15c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V23agetV11V23Iainfix <=V23V15Aainfix <=c0V23FAamin_distasuffixV5V8asuffixV4V24agetV11V24Iainfix <=V24V1Aainfix <V15V24FIainfix >=V15c0Aainfix >=ainfix -V1c1V15FFFAamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix -V1c1c1agetV7V1Aamin_distasuffixV5ainfix +V8c1asuffixV4V25agetV9V25Iainfix <=V25ainfix -V1c1Aainfix <=c0V25FAamin_distasuffixV5V8asuffixV4V26agetV9V26Iainfix <=V26V1Aainfix <ainfix -V1c1V26FIainfix >=ainfix -V1c1c0Aamin_distasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V27agetV9V27Iainfix <=V27V1Aainfix <=c0V27FIainfix <ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FAainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Aainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V28agetV7V28Iainfix <=V28V1Aainfix <=c0V28FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V29ainfix -V1V29Iainfix <V29ainfix +V1c1Aainfix <=c0V29FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+      <transf name="split_goal" proved="true" expanded="false">
+       <goal name="WP_parameter distance.13.1" expl="for loop preservation" sum="e3532d9125256175ceb8e5c817206376" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V9agetV7V9Iainfix <=V9V1Aainfix <=c0V9FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V10ainfix -V1V10Iainfix <V10ainfix +V1c1Aainfix <=c0V10FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.13.2" expl="for loop preservation" sum="b44bdcf4f1c706accce3c64a4390087f" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V9agetV7V9Iainfix <=V9V1Aainfix <=c0V9FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V10ainfix -V1V10Iainfix <V10ainfix +V1c1Aainfix <=c0V10FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.13.2" expl="for loop preservation" sum="1ae63865e9613ac15420fff952e3aa91" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V9agetV7V9Iainfix <=V9V1Aainfix <=c0V9FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V10ainfix -V1V10Iainfix <V10ainfix +V1c1Aainfix <=c0V10FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.13.3" expl="for loop preservation" sum="02aefcc18f2bc6ed080dd9db43f48d06" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V9agetV7V9Iainfix <=V9V1Aainfix <=c0V9FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V10ainfix -V1V10Iainfix <V10ainfix +V1c1Aainfix <=c0V10FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.13.3" expl="for loop preservation" sum="fb3bd3a2feb74535c8655635ef79fef0" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V9agetV7V9Iainfix <=V9V1Aainfix <=c0V9FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V10ainfix -V1V10Iainfix <V10ainfix +V1c1Aainfix <=c0V10FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.13.4" expl="for loop preservation" sum="4925e9033ca9cbd374c42be6f9374902" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V10agetV9V10Iainfix <=V10V1Aainfix <=c0V10FIainfix <ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V11agetV7V11Iainfix <=V11V1Aainfix <=c0V11FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V12ainfix -V1V12Iainfix <V12ainfix +V1c1Aainfix <=c0V12FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
-        <proof prover="z3" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.06"/>
-        </proof>
+       <goal name="WP_parameter distance.13.4" expl="for loop preservation" sum="e68c29ea0863ee158d0bfa2a56cd0936" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V10agetV9V10Iainfix <=V10V1Aainfix <=c0V10FIainfix <ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V11agetV7V11Iainfix <=V11V1Aainfix <=c0V11FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V12ainfix -V1V12Iainfix <V12ainfix +V1c1Aainfix <=c0V12FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+        <transf name="inline_goal" proved="true" expanded="false">
+         <goal name="WP_parameter distance.13.4.1" expl="for loop preservation" sum="f87ee310aaed8369b22c19feea52af5f" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <=agetV9V10V11IadistasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V10V11FAadistasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V10agetV9V10Iainfix =V10V1Oainfix <V10V1Aainfix =c0V10Oainfix <c0V10FIainfix <ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix =c0V1Oainfix <c0V1Iainfix <V1ainfix +V1c1Aainfix =c0V1Oainfix <c0V1Iainfix <V1ainfix +V1c1Aainfix =c0V1Oainfix <c0V1Iainfix <=agetV7V12V13IadistasuffixV5ainfix +V8c1asuffixV4V12V13FAadistasuffixV5ainfix +V8c1asuffixV4V12agetV7V12Iainfix =V12V1Oainfix <V12V1Aainfix =c0V12Oainfix <c0V12FIainfix <=c0V8Aainfix <=V8ainfix -V0c1FFIainfix <=c0ainfix -V0c1Iainfix =agetV6V14ainfix +V1aprefix -V14Iainfix <V14ainfix +V1c1Aainfix =c0V14Oainfix <c0V14FFIainfix =c0V1Oainfix <c0V1Iainfix <=c0ainfix +V1c1Iainfix <=c0V1Aainfix <=c0V0FFFF">
+          <proof prover="z3" timelimit="30" edited="" obsolete="false">
+           <result status="valid" time="0.52"/>
+          </proof>
+         </goal>
+        </transf>
        </goal>
-       <goal name="WP_parameter distance.13.5" expl="for loop preservation" sum="6bdbe13e9dd586420f3199ab5d880fa2" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix -V1c1c1agetV7V1Aamin_distasuffixV5ainfix +V8c1asuffixV4V10agetV9V10Iainfix <=V10ainfix -V1c1Aainfix <=c0V10FAamin_distasuffixV5V8asuffixV4V11agetV9V11Iainfix <=V11V1Aainfix <ainfix -V1c1V11FIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V12agetV7V12Iainfix <=V12V1Aainfix <=c0V12FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V13ainfix -V1V13Iainfix <V13ainfix +V1c1Aainfix <=c0V13FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.13.5" expl="for loop preservation" sum="1587441c8f04116367f025be41dcf7a6" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix -V1c1c1agetV7V1Aamin_distasuffixV5ainfix +V8c1asuffixV4V10agetV9V10Iainfix <=V10ainfix -V1c1Aainfix <=c0V10FAamin_distasuffixV5V8asuffixV4V11agetV9V11Iainfix <=V11V1Aainfix <ainfix -V1c1V11FIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V12agetV7V12Iainfix <=V12V1Aainfix <=c0V12FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V13ainfix -V1V13Iainfix <V13ainfix +V1c1Aainfix <=c0V13FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="4.59"/>
+         <result status="valid" time="13.05"/>
         </proof>
        </goal>
-       <goal name="WP_parameter distance.13.6" expl="for loop preservation" sum="3942c2e4de6f646ae6841c4d57654c23" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3iainfix =agetV3V8agetV2V12amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V12c-1c1V13Aamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV14V15Iainfix <=V15ainfix +V12c-1Aainfix <=c0V15FAamin_distasuffixV5V8asuffixV4V16agetV14V16Iainfix <=V16V1Aainfix <ainfix +V12c-1V16FIainfix =V14asetV11V12V10FAainfix <V12ainfix +V1c1Aainfix <=c0V12amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V12c-1c1V13Aamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV17V18Iainfix <=V18ainfix +V12c-1Aainfix <=c0V18FAamin_distasuffixV5V8asuffixV4V19agetV17V19Iainfix <=V19V1Aainfix <ainfix +V12c-1V19FIainfix =V17asetV11V12ainfix +aminagetV11V12agetV11ainfix +V12c1c1FAainfix <V12ainfix +V1c1Aainfix <=c0V12Aainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Aainfix <V12ainfix +V1c1Aainfix <=c0V12Aainfix <V12V1Aainfix <=c0V12Aainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FAainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V20agetV11V20Iainfix <=V20V12Aainfix <=c0V20FAamin_distasuffixV5V8asuffixV4V21agetV11V21Iainfix <=V21V1Aainfix <V12V21FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V22agetV7V22Iainfix <=V22V1Aainfix <=c0V22FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V23ainfix -V1V23Iainfix <V23ainfix +V1c1Aainfix <=c0V23FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
-        <transf name="split_goal" proved="true" expanded="true">
-         <goal name="WP_parameter distance.13.6.1" expl="for loop preservation" sum="f05ee215abf0219e2703812c14165121" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V13agetV11V13Iainfix <=V13V12Aainfix <=c0V13FAamin_distasuffixV5V8asuffixV4V14agetV11V14Iainfix <=V14V1Aainfix <V12V14FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV7V15Iainfix <=V15V1Aainfix <=c0V15FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V16ainfix -V1V16Iainfix <V16ainfix +V1c1Aainfix <=c0V16FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.13.6" expl="for loop preservation" sum="02af2ce9083e9c66697d91b76d1833fc" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3iainfix =agetV3V8agetV2V12amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V12c-1c1V13Aamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV14V15Iainfix <=V15ainfix +V12c-1Aainfix <=c0V15FAamin_distasuffixV5V8asuffixV4V16agetV14V16Iainfix <=V16V1Aainfix <ainfix +V12c-1V16FIainfix =V14asetV11V12V10FAainfix <V12ainfix +V1c1Aainfix <=c0V12amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V12c-1c1V13Aamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV17V18Iainfix <=V18ainfix +V12c-1Aainfix <=c0V18FAamin_distasuffixV5V8asuffixV4V19agetV17V19Iainfix <=V19V1Aainfix <ainfix +V12c-1V19FIainfix =V17asetV11V12ainfix +aminagetV11V12agetV11ainfix +V12c1c1FAainfix <V12ainfix +V1c1Aainfix <=c0V12Aainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Aainfix <V12ainfix +V1c1Aainfix <=c0V12Aainfix <V12V1Aainfix <=c0V12Aainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FAainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V20agetV11V20Iainfix <=V20V12Aainfix <=c0V20FAamin_distasuffixV5V8asuffixV4V21agetV11V21Iainfix <=V21V1Aainfix <V12V21FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V22agetV7V22Iainfix <=V22V1Aainfix <=c0V22FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V23ainfix -V1V23Iainfix <V23ainfix +V1c1Aainfix <=c0V23FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+        <transf name="split_goal" proved="true" expanded="false">
+         <goal name="WP_parameter distance.13.6.1" expl="for loop preservation" sum="27886f6f6bae3a3c55b91b93b6097951" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V13agetV11V13Iainfix <=V13V12Aainfix <=c0V13FAamin_distasuffixV5V8asuffixV4V14agetV11V14Iainfix <=V14V1Aainfix <V12V14FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV7V15Iainfix <=V15V1Aainfix <=c0V15FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V16ainfix -V1V16Iainfix <V16ainfix +V1c1Aainfix <=c0V16FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
            <result status="valid" time="0.02"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.2" expl="for loop preservation" sum="8e8b91bc77444d3a61565c4c5ed196da" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.2" expl="for loop preservation" sum="fe590b8ee57338733dfcd759330f0c9f" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-           <result status="valid" time="0.03"/>
+           <result status="valid" time="0.04"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.3" expl="for loop preservation" sum="68f01bfc90ab9dab8e39e5cc194d73ba" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.3" expl="for loop preservation" sum="fe3649e6dead45e506a61da0a5ef65ab" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-           <result status="valid" time="0.02"/>
+           <result status="valid" time="0.04"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.4" expl="for loop preservation" sum="e70c8ff8846d98fbc7438a3d26994dc8" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12Iainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.4" expl="for loop preservation" sum="4f35209bd0e007df26fa486dbd336ad3" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12Iainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
            <result status="valid" time="0.03"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.5" expl="for loop preservation" sum="31bc2c9553d93894df1c33a2b8c54ae6" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5V8asuffixV4V15agetV14V15Iainfix <=V15V1Aainfix <ainfix +V12c-1V15FIainfix =V14asetV11V12V10FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12Iainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV11V16Iainfix <=V16V12Aainfix <=c0V16FAamin_distasuffixV5V8asuffixV4V17agetV11V17Iainfix <=V17V1Aainfix <V12V17FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV7V18Iainfix <=V18V1Aainfix <=c0V18FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V19ainfix -V1V19Iainfix <V19ainfix +V1c1Aainfix <=c0V19FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.5" expl="for loop preservation" sum="d2a2bad8d3bfa0c63c8abb7560aa5d2e" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5V8asuffixV4V15agetV14V15Iainfix <=V15V1Aainfix <ainfix +V12c-1V15FIainfix =V14asetV11V12V10FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12Iainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV11V16Iainfix <=V16V12Aainfix <=c0V16FAamin_distasuffixV5V8asuffixV4V17agetV11V17Iainfix <=V17V1Aainfix <V12V17FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV7V18Iainfix <=V18V1Aainfix <=c0V18FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V19ainfix -V1V19Iainfix <V19ainfix +V1c1Aainfix <=c0V19FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="coq" timelimit="20" edited="edit_distance_WP_EditDistance_WP_parameter_distance_1.v" obsolete="false">
-           <result status="valid" time="0.84"/>
+           <result status="valid" time="1.00"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.6" expl="for loop preservation" sum="5fd710c81355838704937a9350ddd2a3" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4V15agetV14V15Iainfix <=V15ainfix +V12c-1Aainfix <=c0V15FIainfix =V14asetV11V12V10FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12Iainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV11V16Iainfix <=V16V12Aainfix <=c0V16FAamin_distasuffixV5V8asuffixV4V17agetV11V17Iainfix <=V17V1Aainfix <V12V17FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV7V18Iainfix <=V18V1Aainfix <=c0V18FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V19ainfix -V1V19Iainfix <V19ainfix +V1c1Aainfix <=c0V19FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.6" expl="for loop preservation" sum="c8c3d2bc75759b745b50f7996b5ed43b" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4V15agetV14V15Iainfix <=V15ainfix +V12c-1Aainfix <=c0V15FIainfix =V14asetV11V12V10FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12Iainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV11V16Iainfix <=V16V12Aainfix <=c0V16FAamin_distasuffixV5V8asuffixV4V17agetV11V17Iainfix <=V17V1Aainfix <V12V17FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV7V18Iainfix <=V18V1Aainfix <=c0V18FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V19ainfix -V1V19Iainfix <V19ainfix +V1c1Aainfix <=c0V19FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
            <result status="valid" time="0.04"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.7" expl="for loop preservation" sum="746b7e0c280424bbae1b73ad4d9a2b65" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V12c-1c1V13Iainfix =V14asetV11V12V10FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12Iainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV11V15Iainfix <=V15V12Aainfix <=c0V15FAamin_distasuffixV5V8asuffixV4V16agetV11V16Iainfix <=V16V1Aainfix <V12V16FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V17agetV7V17Iainfix <=V17V1Aainfix <=c0V17FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V18ainfix -V1V18Iainfix <V18ainfix +V1c1Aainfix <=c0V18FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.7" expl="for loop preservation" sum="2a234f90e2612564a1dba40a8c2cc2be" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V12c-1c1V13Iainfix =V14asetV11V12V10FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12Iainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV11V15Iainfix <=V15V12Aainfix <=c0V15FAamin_distasuffixV5V8asuffixV4V16agetV11V16Iainfix <=V16V1Aainfix <V12V16FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V17agetV7V17Iainfix <=V17V1Aainfix <=c0V17FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V18ainfix -V1V18Iainfix <V18ainfix +V1c1Aainfix <=c0V18FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-           <result status="valid" time="0.03"/>
+           <result status="valid" time="0.04"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.8" expl="for loop preservation" sum="950da5869d435191a418c461607c327e" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.8" expl="for loop preservation" sum="dc67c2d9caffcdcfecaed2320dfdaedb" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-           <result status="valid" time="0.02"/>
+           <result status="valid" time="0.04"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.9" expl="for loop preservation" sum="0d8e8ef8aa43aa53ea831ef7327165c3" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.9" expl="for loop preservation" sum="50aa371d5f12910b60cd6e7657a41cb2" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
            <result status="valid" time="0.03"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.10" expl="for loop preservation" sum="6ca44d456711451c05ce36cf06ebabac" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.10" expl="for loop preservation" sum="e9a6d0abf660d66f28a4729629dbbb63" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V14agetV11V14Iainfix <=V14V12Aainfix <=c0V14FAamin_distasuffixV5V8asuffixV4V15agetV11V15Iainfix <=V15V1Aainfix <V12V15FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV7V16Iainfix <=V16V1Aainfix <=c0V16FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V17ainfix -V1V17Iainfix <V17ainfix +V1c1Aainfix <=c0V17FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-           <result status="valid" time="0.02"/>
+           <result status="valid" time="0.03"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.11" expl="for loop preservation" sum="ccec34f13c891c12bbab90bbd8f07bcc" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5V8asuffixV4V15agetV14V15Iainfix <=V15V1Aainfix <ainfix +V12c-1V15FIainfix =V14asetV11V12ainfix +aminagetV11V12agetV11ainfix +V12c1c1FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV11V16Iainfix <=V16V12Aainfix <=c0V16FAamin_distasuffixV5V8asuffixV4V17agetV11V17Iainfix <=V17V1Aainfix <V12V17FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV7V18Iainfix <=V18V1Aainfix <=c0V18FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V19ainfix -V1V19Iainfix <V19ainfix +V1c1Aainfix <=c0V19FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.11" expl="for loop preservation" sum="0f6ed8c60e1785d7fdfaaa7757106c8c" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5V8asuffixV4V15agetV14V15Iainfix <=V15V1Aainfix <ainfix +V12c-1V15FIainfix =V14asetV11V12ainfix +aminagetV11V12agetV11ainfix +V12c1c1FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV11V16Iainfix <=V16V12Aainfix <=c0V16FAamin_distasuffixV5V8asuffixV4V17agetV11V17Iainfix <=V17V1Aainfix <V12V17FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV7V18Iainfix <=V18V1Aainfix <=c0V18FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V19ainfix -V1V19Iainfix <V19ainfix +V1c1Aainfix <=c0V19FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="coq" timelimit="20" edited="edit_distance_WP_EditDistance_WP_parameter_distance_2.v" obsolete="false">
-           <result status="valid" time="1.02"/>
+           <result status="valid" time="1.20"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.12" expl="for loop preservation" sum="3ed2c027f8d658fcf3e07a22184101e1" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4V15agetV14V15Iainfix <=V15ainfix +V12c-1Aainfix <=c0V15FIainfix =V14asetV11V12ainfix +aminagetV11V12agetV11ainfix +V12c1c1FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV11V16Iainfix <=V16V12Aainfix <=c0V16FAamin_distasuffixV5V8asuffixV4V17agetV11V17Iainfix <=V17V1Aainfix <V12V17FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV7V18Iainfix <=V18V1Aainfix <=c0V18FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V19ainfix -V1V19Iainfix <V19ainfix +V1c1Aainfix <=c0V19FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.12" expl="for loop preservation" sum="9d27777cf11e1b00165e014668287966" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4V15agetV14V15Iainfix <=V15ainfix +V12c-1Aainfix <=c0V15FIainfix =V14asetV11V12ainfix +aminagetV11V12agetV11ainfix +V12c1c1FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V16agetV11V16Iainfix <=V16V12Aainfix <=c0V16FAamin_distasuffixV5V8asuffixV4V17agetV11V17Iainfix <=V17V1Aainfix <V12V17FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V18agetV7V18Iainfix <=V18V1Aainfix <=c0V18FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V19ainfix -V1V19Iainfix <V19ainfix +V1c1Aainfix <=c0V19FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-           <result status="valid" time="0.04"/>
+           <result status="valid" time="0.05"/>
           </proof>
          </goal>
-         <goal name="WP_parameter distance.13.6.13" expl="for loop preservation" sum="c13f7295bd436f956b2412339c52d207" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V12c-1c1V13Iainfix =V14asetV11V12ainfix +aminagetV11V12agetV11ainfix +V12c1c1FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV11V15Iainfix <=V15V12Aainfix <=c0V15FAamin_distasuffixV5V8asuffixV4V16agetV11V16Iainfix <=V16V1Aainfix <V12V16FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V17agetV7V17Iainfix <=V17V1Aainfix <=c0V17FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V18ainfix -V1V18Iainfix <V18ainfix +V1c1Aainfix <=c0V18FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+         <goal name="WP_parameter distance.13.6.13" expl="for loop preservation" sum="b119793762b1e90dcc40b4e991d6af3b" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +V12c-1c1V13Iainfix =V14asetV11V12ainfix +aminagetV11V12agetV11ainfix +V12c1c1FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix <ainfix +V12c1ainfix +V1c1Aainfix <=c0ainfix +V12c1Iainfix <V12ainfix +V1c1Aainfix <=c0V12Iainfix =agetV3V8agetV2V12NIainfix <V12V1Aainfix <=c0V12Iainfix <V8V0Aainfix <=c0V8Iainfix =V13agetV11V12FIainfix <V12ainfix +V1c1Aainfix <=c0V12Iamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +V12c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV11V15Iainfix <=V15V12Aainfix <=c0V15FAamin_distasuffixV5V8asuffixV4V16agetV11V16Iainfix <=V16V1Aainfix <V12V16FIainfix >=V12c0Aainfix >=ainfix -V1c1V12FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V17agetV7V17Iainfix <=V17V1Aainfix <=c0V17FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V18ainfix -V1V18Iainfix <V18ainfix +V1c1Aainfix <=c0V18FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
           <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-           <result status="valid" time="0.03"/>
+           <result status="valid" time="0.04"/>
           </proof>
          </goal>
         </transf>
        </goal>
-       <goal name="WP_parameter distance.13.7" expl="for loop preservation" sum="6e74242d528e537ca658725785512266" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V12agetV11V12Iainfix <=V12V1Aainfix <=c0V12FIamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +c0c-1c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V13agetV11V13Iainfix <=V13ainfix +c0c-1Aainfix <=c0V13FAamin_distasuffixV5V8asuffixV4V14agetV11V14Iainfix <=V14V1Aainfix <ainfix +c0c-1V14FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV7V15Iainfix <=V15V1Aainfix <=c0V15FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V16ainfix -V1V16Iainfix <V16ainfix +V1c1Aainfix <=c0V16FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+       <goal name="WP_parameter distance.13.7" expl="for loop preservation" sum="c26b9c4df379b1166aee6064945c7f6d" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5ainfix +ainfix +V8c-1c1asuffixV4V12agetV11V12Iainfix <=V12V1Aainfix <=c0V12FIamin_distasuffixV5ainfix +V8c1asuffixV4ainfix +ainfix +c0c-1c1V10Aamin_distasuffixV5ainfix +V8c1asuffixV4V13agetV11V13Iainfix <=V13ainfix +c0c-1Aainfix <=c0V13FAamin_distasuffixV5V8asuffixV4V14agetV11V14Iainfix <=V14V1Aainfix <ainfix +c0c-1V14FFFIainfix >=ainfix -V1c1c0Iainfix =V9asetV7V1ainfix +agetV7V1c1FIainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iainfix <V1ainfix +V1c1Aainfix <=c0V1Iamin_distasuffixV5ainfix +V8c1asuffixV4V15agetV7V15Iainfix <=V15V1Aainfix <=c0V15FIainfix >=V8c0Aainfix >=ainfix -V0c1V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V16ainfix -V1V16Iainfix <V16ainfix +V1c1Aainfix <=c0V16FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
         <proof prover="cvc3" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.05"/>
+         <result status="valid" time="0.06"/>
         </proof>
         <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
-         <result status="valid" time="0.03"/>
+         <result status="valid" time="0.04"/>
         </proof>
        </goal>
       </transf>
      </goal>
-     <goal name="WP_parameter distance.14" expl="precondition" sum="463c47d3f59963fef73eb5bcd28e40aa" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V8agetV7V8Iainfix <=V8V1Aainfix <=c0V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V9ainfix -V1V9Iainfix <V9ainfix +V1c1Aainfix <=c0V9FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.14" expl="precondition" sum="c1cb8fc569d9fa8ca5362a003e2279dd" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3ainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V8agetV7V8Iainfix <=V8V1Aainfix <=c0V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V9ainfix -V1V9Iainfix <V9ainfix +V1c1Aainfix <=c0V9FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter distance.15" expl="normal postcondition" sum="82371112879afafab69b2118ca585ea9" proved="true" expanded="true" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV7c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V8agetV7V8Iainfix <=V8V1Aainfix <=c0V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V9ainfix -V1V9Iainfix <V9ainfix +V1c1Aainfix <=c0V9FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
+     <goal name="WP_parameter distance.15" expl="normal postcondition" sum="4e97b844e4f75130bc0a964fb195fe97" proved="true" expanded="false" shape="Lamk arrayV1V2Lamk arrayV0V3amin_distasuffixV5c0asuffixV4c0agetV7c0Iainfix <c0ainfix +V1c1Aainfix <=c0c0Iamin_distasuffixV5ainfix +ainfix +c0c-1c1asuffixV4V8agetV7V8Iainfix <=V8V1Aainfix <=c0V8FFIainfix >=ainfix -V0c1c0Iainfix =agetV6V9ainfix -V1V9Iainfix <V9ainfix +V1c1Aainfix <=c0V9FFIainfix <=c0V1Iainfix >=ainfix +V1c1c0Iainfix >=V1c0Aainfix >=V0c0FFFF">
       <proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+       <result status="valid" time="0.04"/>
       </proof>
      </goal>
     </transf>