Commit 7ef4d568 authored by MARCHE Claude's avatar MARCHE Claude

updated Coq proofs for KMP

parent a5e89797
......@@ -9,10 +9,10 @@
<prover id="4" name="CVC3" version="2.2" timelimit="10" memlimit="0"/>
<prover id="5" name="Z3" version="3.2" timelimit="3" memlimit="0"/>
<file name="../array.why">
<theory name="Test_simplify_array" sum="d2af9877f4bfd7d2092d8e6c8a390a5f" expanded="true">
<theory name="Test_simplify_array" sum="6cb2fd4ede8c2e597266ad5a6f4953c4" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -20,7 +20,7 @@
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -28,7 +28,7 @@
</goal>
<goal name="G3" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -36,7 +36,7 @@
</goal>
<goal name="G4" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......
(* This file is generated by Why3's Coq 8.4 driver *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -8,146 +8,145 @@ Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
Implicit Arguments mk_ref [[a]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).
Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
((length (make n v)) = n).
Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
((get (make n v) i) = v).
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
(* Why3 assumption *)
Definition matches (a1:(@array char char_WhyType)) (i1:Z) (a2:(@array
char char_WhyType)) (i2:Z) (n:Z): Prop := ((0%Z <= i1)%Z /\
(i1 <= ((length a1) - n)%Z)%Z) /\ (((0%Z <= i2)%Z /\
(i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%Z) -> ((get a1 (i1 + i)%Z) = (get a2 (i2 + i)%Z))).
Axiom matches_empty : forall (a1:(@array char char_WhyType)) (a2:(@array
char char_WhyType)) (i1:Z) (i2:Z), ((0%Z <= i1)%Z /\
(i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\ (i2 <= (length a2))%Z) ->
(matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2
n) -> ((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
Definition matches (a1:(array char)) (i1:Z) (a2:(array char)) (i2:Z)
(n:Z): Prop := ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
(((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((get a1 (i1 + i)%Z) = (get a2
(i2 + i)%Z))).
Axiom matches_empty : forall (a1:(array char)) (a2:(array char)) (i1:Z)
(i2:Z), ((0%Z <= i1)%Z /\ (i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\
(i2 <= (length a2))%Z) -> (matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
((i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z -> (((get a1 (i1 + n)%Z) = (get a2
(i2 + n)%Z)) -> (matches a1 i1 a2 i2 (n + 1%Z)%Z)))).
Axiom matches_contradiction_at_first : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z ->
((~ ((get a1 i1) = (get a2 i2))) -> ~ (matches a1 i1 a2 i2 n)).
Axiom matches_contradiction_at_first : forall (a1:(array char)) (a2:(array
char)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z -> ((~ ((get a1 i1) = (get a2
i2))) -> ~ (matches a1 i1 a2 i2 n)).
Axiom matches_contradiction_at_i : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z ->
(((0%Z <= i)%Z /\ (i < n)%Z) -> ((~ ((get a1 (i1 + i)%Z) = (get a2
(i2 + i)%Z))) -> ~ (matches a1 i1 a2 i2 n))).
Axiom matches_contradiction_at_i : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z -> (((0%Z <= i)%Z /\ (i < n)%Z) ->
((~ ((get a1 (i1 + i)%Z) = (get a2 (i2 + i)%Z))) -> ~ (matches a1 i1 a2 i2
n))).
Axiom matches_right_weakening : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1 i1
a2 i2 n) -> ((n' < n)%Z -> (matches a1 i1 a2 i2 n')).
Axiom matches_right_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1 i1 a2 i2 n) -> ((n' < n)%Z ->
(matches a1 i1 a2 i2 n')).
Axiom matches_left_weakening : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1
(i1 - (n - n')%Z)%Z a2 (i2 - (n - n')%Z)%Z n) -> ((n' < n)%Z -> (matches a1
i1 a2 i2 n')).
Axiom matches_left_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1 (i1 - (n - n')%Z)%Z a2
(i2 - (n - n')%Z)%Z n) -> ((n' < n)%Z -> (matches a1 i1 a2 i2 n')).
Axiom matches_sym : forall (a1:(@array char char_WhyType)) (a2:(@array
char char_WhyType)) (i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
(matches a2 i2 a1 i1 n).
Axiom matches_sym : forall (a1:(array char)) (a2:(array char)) (i1:Z) (i2:Z)
(n:Z), (matches a1 i1 a2 i2 n) -> (matches a2 i2 a1 i1 n).
Axiom matches_trans : forall (a1:(@array char char_WhyType)) (a2:(@array
char char_WhyType)) (a3:(@array char char_WhyType)) (i1:Z) (i2:Z) (i3:Z)
(n:Z), (matches a1 i1 a2 i2 n) -> ((matches a2 i2 a3 i3 n) -> (matches a1
i1 a3 i3 n)).
Axiom matches_trans : forall (a1:(array char)) (a2:(array char)) (a3:(array
char)) (i1:Z) (i2:Z) (i3:Z) (n:Z), (matches a1 i1 a2 i2 n) -> ((matches a2
i2 a3 i3 n) -> (matches a1 i1 a3 i3 n)).
(* Why3 assumption *)
Definition is_next (p:(@array char char_WhyType)) (j:Z) (n:Z): Prop :=
((0%Z <= n)%Z /\ (n < j)%Z) /\ ((matches p (j - n)%Z p 0%Z n) /\
forall (z:Z), ((n < z)%Z /\ (z < j)%Z) -> ~ (matches p (j - z)%Z p 0%Z z)).
Definition is_next (p:(array char)) (j:Z) (n:Z): Prop := ((0%Z <= n)%Z /\
(n < j)%Z) /\ ((matches p (j - n)%Z p 0%Z n) /\ forall (z:Z), ((n < z)%Z /\
(z < j)%Z) -> ~ (matches p (j - z)%Z p 0%Z z)).
Axiom next_iteration : forall (p:(@array char char_WhyType)) (a:(@array
char char_WhyType)) (i:Z) (j:Z) (n:Z), ((0%Z < j)%Z /\
(j < (length p))%Z) -> (((j <= i)%Z /\ (i <= (length a))%Z) -> ((matches a
(i - j)%Z p 0%Z j) -> ((is_next p j n) -> (matches a (i - n)%Z p 0%Z n)))).
Axiom next_iteration : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
(n:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((matches a (i - j)%Z p 0%Z j) -> ((is_next p j
n) -> (matches a (i - n)%Z p 0%Z n)))).
Axiom next_is_maximal : forall (p:(@array char char_WhyType)) (a:(@array
char char_WhyType)) (i:Z) (j:Z) (n:Z) (k:Z), ((0%Z < j)%Z /\
(j < (length p))%Z) -> (((j <= i)%Z /\ (i <= (length a))%Z) ->
((((i - j)%Z < k)%Z /\ (k < (i - n)%Z)%Z) -> ((matches a (i - j)%Z p 0%Z
j) -> ((is_next p j n) -> ~ (matches a k p 0%Z (length p)))))).
Axiom next_is_maximal : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
(n:Z) (k:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((((i - j)%Z < k)%Z /\ (k < (i - n)%Z)%Z) ->
((matches a (i - j)%Z p 0%Z j) -> ((is_next p j n) -> ~ (matches a k p 0%Z
(length p)))))).
Axiom next_1_0 : forall (p:(@array char char_WhyType)),
(1%Z <= (length p))%Z -> (is_next p 1%Z 0%Z).
Axiom next_1_0 : forall (p:(array char)), (1%Z <= (length p))%Z -> (is_next p
1%Z 0%Z).
(* Why3 goal *)
Theorem WP_parameter_initnext : forall (p:Z) (p1:(@map.Map.map Z _
char char_WhyType)), let p2 := (mk_array p p1) in (((0%Z <= p)%Z /\
(1%Z <= p)%Z) -> ((0%Z <= p)%Z -> ((0%Z <= p)%Z -> ((1%Z < p)%Z ->
(((0%Z <= 1%Z)%Z /\ (1%Z < p)%Z) -> forall (next:(@map.Map.map Z _ Z _)),
((0%Z <= p)%Z /\ (next = (map.Map.set (map.Map.const 0%Z:(@map.Map.map Z _
Z _)) 1%Z 0%Z))) -> forall (j:Z) (i:Z) (next1:(@map.Map.map Z _ Z _)),
(((0%Z <= j)%Z /\ ((j < i)%Z /\ (i <= p)%Z)) /\ ((matches p2 (i - j)%Z p2
0%Z j) /\ ((forall (z:Z), (((j + 1%Z)%Z < z)%Z /\ (z < (i + 1%Z)%Z)%Z) ->
~ (matches p2 ((i + 1%Z)%Z - z)%Z p2 0%Z z)) /\ forall (k:Z),
((0%Z < k)%Z /\ (k <= i)%Z) -> (is_next p2 k (map.Map.get next1 k))))) ->
((i < (p - 1%Z)%Z)%Z -> (((0%Z <= j)%Z /\ (j < p)%Z) -> (((0%Z <= i)%Z /\
(i < p)%Z) -> (((map.Map.get p1 i) = (map.Map.get p1 j)) -> forall (i1:Z),
(i1 = (i + 1%Z)%Z) -> forall (j1:Z), (j1 = (j + 1%Z)%Z) ->
(((0%Z <= p)%Z /\ ((0%Z <= i1)%Z /\ (i1 < p)%Z)) ->
forall (next2:(@map.Map.map Z _ Z _)), ((0%Z <= p)%Z /\
(next2 = (map.Map.set next1 i1 j1))) -> forall (z:Z),
Theorem WP_parameter_initnext : forall (p:Z) (p1:(map.Map.map Z char)),
let p2 := (mk_array p p1) in (((0%Z <= p)%Z /\ (1%Z <= p)%Z) ->
((0%Z <= p)%Z -> forall (next:Z) (next1:(map.Map.map Z Z)),
((0%Z <= next)%Z /\ ((next = p) /\ forall (i:Z), ((map.Map.get next1
i) = 0%Z))) -> ((1%Z < p)%Z -> (((0%Z <= 1%Z)%Z /\ (1%Z < next)%Z) ->
forall (next2:(map.Map.map Z Z)), ((0%Z <= next)%Z /\
(next2 = (map.Map.set next1 1%Z 0%Z))) -> forall (j:Z) (i:Z)
(next3:(map.Map.map Z Z)), (((0%Z <= j)%Z /\ ((j < i)%Z /\ (i <= p)%Z)) /\
((matches p2 (i - j)%Z p2 0%Z j) /\ ((forall (z:Z), (((j + 1%Z)%Z < z)%Z /\
(z < (i + 1%Z)%Z)%Z) -> ~ (matches p2 ((i + 1%Z)%Z - z)%Z p2 0%Z z)) /\
forall (k:Z), ((0%Z < k)%Z /\ (k <= i)%Z) -> (is_next p2 k
(map.Map.get next3 k))))) -> ((i < (p - 1%Z)%Z)%Z -> (((0%Z <= j)%Z /\
(j < p)%Z) -> (((0%Z <= i)%Z /\ (i < p)%Z) -> (((map.Map.get p1
i) = (map.Map.get p1 j)) -> forall (i1:Z), (i1 = (i + 1%Z)%Z) ->
forall (j1:Z), (j1 = (j + 1%Z)%Z) -> (((0%Z <= next)%Z /\ ((0%Z <= i1)%Z /\
(i1 < next)%Z)) -> forall (next4:(map.Map.map Z Z)), ((0%Z <= next)%Z /\
(next4 = (map.Map.set next3 i1 j1))) -> forall (z:Z),
(((j1 + 1%Z)%Z < z)%Z /\ (z < (i1 + 1%Z)%Z)%Z) -> ~ (matches p2
((i1 + 1%Z)%Z - z)%Z p2 0%Z z))))))))))).
(* Why3 intros p p1 p2 (h1,h2) h3 h4 h5 (h6,h7) next (h8,h9) j i next1
((h10,(h11,h12)),(h13,(h14,h15))) h16 (h17,h18) (h19,h20) h21 i1 h22
j1 h23 (h24,(h25,h26)) next2 (h27,h28) z (h29,h30). *)
(* YOU MAY EDIT THE PROOF BELOW *)
((i1 + 1%Z)%Z - z)%Z p2 0%Z z)))))))))).
intros n p1.
intro p3. unfold p3. clear p3.
intros _ _ _ hn _ _ _.
intros (_,hn) _ next next1 _ _ _ _ _.
intros j i next4 ((hj,hi),(h0,(h1,h2))).
intros hi' _ _ eq.
intros i1 hi1; subst i1.
......
(* This file is generated by Why3's Coq 8.4 driver *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -8,145 +8,145 @@ Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
Implicit Arguments mk_ref [[a]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).
Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
((length (make n v)) = n).
Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
((get (make n v) i) = v).
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
(* Why3 assumption *)
Definition matches (a1:(@array char char_WhyType)) (i1:Z) (a2:(@array
char char_WhyType)) (i2:Z) (n:Z): Prop := ((0%Z <= i1)%Z /\
(i1 <= ((length a1) - n)%Z)%Z) /\ (((0%Z <= i2)%Z /\
(i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%Z) -> ((get a1 (i1 + i)%Z) = (get a2 (i2 + i)%Z))).
Axiom matches_empty : forall (a1:(@array char char_WhyType)) (a2:(@array
char char_WhyType)) (i1:Z) (i2:Z), ((0%Z <= i1)%Z /\
(i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\ (i2 <= (length a2))%Z) ->
(matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2
n) -> ((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
Definition matches (a1:(array char)) (i1:Z) (a2:(array char)) (i2:Z)
(n:Z): Prop := ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
(((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((get a1 (i1 + i)%Z) = (get a2
(i2 + i)%Z))).
Axiom matches_empty : forall (a1:(array char)) (a2:(array char)) (i1:Z)
(i2:Z), ((0%Z <= i1)%Z /\ (i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\
(i2 <= (length a2))%Z) -> (matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
((i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z -> (((get a1 (i1 + n)%Z) = (get a2
(i2 + n)%Z)) -> (matches a1 i1 a2 i2 (n + 1%Z)%Z)))).
Axiom matches_contradiction_at_first : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z ->
((~ ((get a1 i1) = (get a2 i2))) -> ~ (matches a1 i1 a2 i2 n)).
Axiom matches_contradiction_at_first : forall (a1:(array char)) (a2:(array
char)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z -> ((~ ((get a1 i1) = (get a2
i2))) -> ~ (matches a1 i1 a2 i2 n)).
Axiom matches_contradiction_at_i : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z ->
(((0%Z <= i)%Z /\ (i < n)%Z) -> ((~ ((get a1 (i1 + i)%Z) = (get a2
(i2 + i)%Z))) -> ~ (matches a1 i1 a2 i2 n))).
Axiom matches_contradiction_at_i : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z -> (((0%Z <= i)%Z /\ (i < n)%Z) ->
((~ ((get a1 (i1 + i)%Z) = (get a2 (i2 + i)%Z))) -> ~ (matches a1 i1 a2 i2
n))).
Axiom matches_right_weakening : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1 i1
a2 i2 n) -> ((n' < n)%Z -> (matches a1 i1 a2 i2 n')).
Axiom matches_right_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1 i1 a2 i2 n) -> ((n' < n)%Z ->
(matches a1 i1 a2 i2 n')).
Axiom matches_left_weakening : forall (a1:(@array char char_WhyType))
(a2:(@array char char_WhyType)) (i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1
(i1 - (n - n')%Z)%Z a2 (i2 - (n - n')%Z)%Z n) -> ((n' < n)%Z -> (matches a1
i1 a2 i2 n')).
Axiom matches_left_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1 (i1 - (n - n')%Z)%Z a2
(i2 - (n - n')%Z)%Z n) -> ((n' < n)%Z -> (matches a1 i1 a2 i2 n')).
Axiom matches_sym : forall (a1:(@array char char_WhyType)) (a2:(@array
char char_WhyType)) (i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
(matches a2 i2 a1 i1 n).
Axiom matches_sym : forall (a1:(array char)) (a2:(array char)) (i1:Z) (i2:Z)
(n:Z), (matches a1 i1 a2 i2 n) -> (matches a2 i2 a1 i1 n).
Axiom matches_trans : forall (a1:(@array char char_WhyType)) (a2:(@array
char char_WhyType)) (a3:(@array char char_WhyType)) (i1:Z) (i2:Z) (i3:Z)
(n:Z), (matches a1 i1 a2 i2 n) -> ((matches a2 i2 a3 i3 n) -> (matches a1
i1 a3 i3 n)).
Axiom matches_trans : forall (a1:(array char)) (a2:(array char)) (a3:(array
char)) (i1:Z) (i2:Z) (i3:Z) (n:Z), (matches a1 i1 a2 i2 n) -> ((matches a2
i2 a3 i3 n) -> (matches a1 i1 a3 i3 n)).
(* Why3 assumption *)
Definition is_next (p:(@array char char_WhyType)) (j:Z) (n:Z): Prop :=
((0%Z <= n)%Z /\ (n < j)%Z) /\ ((matches p (j - n)%Z p 0%Z n) /\
forall (z:Z), ((n < z)%Z /\ (z < j)%Z) -> ~ (matches p (j - z)%Z p 0%Z z)).
Definition is_next (p:(array char)) (j:Z) (n:Z): Prop := ((0%Z <= n)%Z /\
(n < j)%Z) /\ ((matches p (j - n)%Z p 0%Z n) /\ forall (z:Z), ((n < z)%Z /\
(z < j)%Z) -> ~ (matches p (j - z)%Z p 0%Z z)).
Axiom next_iteration : forall (p:(@array char char_WhyType)) (a:(@array
char char_WhyType)) (i:Z) (j:Z) (n:Z), ((0%Z < j)%Z /\
(j < (length p))%Z) -> (((j <= i)%Z /\ (i <= (length a))%Z) -> ((matches a
(i - j)%Z p 0%Z j) -> ((is_next p j n) -> (matches a (i - n)%Z p 0%Z n)))).
Axiom next_iteration : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
(n:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((matches a (i - j)%Z p 0%Z j) -> ((is_next p j
n) -> (matches a (i - n)%Z p 0%Z n)))).
Axiom next_is_maximal : forall (p:(@array char char_WhyType)) (a:(@array
char char_WhyType)) (i:Z) (j:Z) (n:Z) (k:Z), ((0%Z < j)%Z /\
(j < (length p))%Z) -> (((j <= i)%Z /\ (i <= (length a))%Z) ->
((((i - j)%Z < k)%Z /\ (k < (i - n)%Z)%Z) -> ((matches a (i - j)%Z p 0%Z
j) -> ((is_next p j n) -> ~ (matches a k p 0%Z (length p)))))).
Axiom next_is_maximal : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
(n:Z) (k:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((((i - j)%Z < k)%Z /\ (k < (i - n)%Z)%Z) ->
((matches a (i - j)%Z p 0%Z j) -> ((is_next p j n) -> ~ (matches a k p 0%Z
(length p)))))).
Axiom next_1_0 : forall (p:(@array char char_WhyType)),
(1%Z <= (length p))%Z -> (is_next p 1%Z 0%Z).
Axiom next_1_0 : forall (p:(array char)), (1%Z <= (length p))%Z -> (is_next p
1%Z 0%Z).
(* Why3 goal *)
Theorem WP_parameter_initnext : forall (p:Z) (p1:(@map.Map.map Z _