diff --git a/examples/verifythis_fm2012_lcp.mlw b/examples/verifythis_fm2012_lcp.mlw index a9c1554a26e2a685be14d1959786e259cb4bf203..008b2762a4b401c9ccd4efeea130a58e6f77013f 100644 --- a/examples/verifythis_fm2012_lcp.mlw +++ b/examples/verifythis_fm2012_lcp.mlw @@ -71,6 +71,9 @@ comparison on arrays, a sorting routine, and LCP. The client code (LRS.java) uses these to solve the LRS problem. Verify that it does so correctly. + +(Based on code by Robert Sedgewick and Kevin Wayne.) + *) @@ -117,7 +120,7 @@ let lcp (a:array int) (x y:int) : int !l (** test harness for lcp *) -let test1 () = +let test () = let arr = Array.make 4 0 in arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5; let x = lcp arr 1 2 in @@ -273,13 +276,15 @@ module SuffixArray use import array.Array use import LCP use import PrefixSort +use map.MapInjection type suffixArray = { values : array int; suffixes : array int; } - -use map.MapInjection +invariant { self.values.length = self.suffixes.length /\ + permutation self.suffixes.elts self.suffixes.length /\ + sorted self.values self.suffixes } predicate inv(s:suffixArray) = s.values.length = s.suffixes.length /\ @@ -287,20 +292,20 @@ predicate inv(s:suffixArray) = sorted s.values s.suffixes let select (s:suffixArray) (i:int) : int - requires { inv s /\ 0 <= i < s.values.length } + requires { 0 <= i < s.values.length } ensures { result = s.suffixes[i] } = s.suffixes[i] -(* needed to establish invariant in function create *) - - use import array.ArrayPermut +use import array.ArrayPermut +(** needed to establish invariant in function create *) lemma permut_permutation : forall a1 a2:array int. permut a1 a2 -> permutation a1.elts a1.length -> permutation a2.elts a2.length +(** constructor of suffixArray structure *) let create (a:array int) : suffixArray - ensures { result.values = a /\ inv result } + ensures { result.values = a } = let n = a.length in let suf = Array.make n 0 in @@ -318,7 +323,7 @@ let lcp (s:suffixArray) (i:int) : int LCP.lcp s.values s.suffixes[i] s.suffixes[i-1] (* -let test2 () = +let test () = let arr = Array.make 4 0 in arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5; let sa = create arr in @@ -470,5 +475,3 @@ use import int.MinMax end - -(* Based on code by Robert Sedgewick and Kevin Wayne. *) diff --git a/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_10.v b/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_10.v index b293a0daf7e5fa39f25fa0f4de18ecbd8cc61951..27adc293142f72b8289486f069c52cdd94b9b8f6 100644 --- a/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_10.v +++ b/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_10.v @@ -1,4 +1,4 @@ -(* This file is generated by Why3's Coq driver *) +(* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. @@ -74,70 +74,81 @@ Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a n) -> ((range a n) -> (surjective a n)). (* Why3 assumption *) -Definition exchange {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a)) - (a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1 - i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\ - forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1 - k) = (map.Map.get a2 k))). +Definition is_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := + (0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\ + (((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\ + (i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))). -Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, - forall (a1:(map.Map.map Z a)), forall (i:Z) (j:Z), (exchange a1 - (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i - j). +(* Why3 assumption *) +Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := + (is_common_prefix a x y l) /\ forall (m:Z), (l < m)%Z -> + ~ (is_common_prefix a x y m). (* Why3 assumption *) -Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a) - -> (map.Map.map Z a) -> Z -> Z -> Prop := - | permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z), - (permut_sub a1 a1 l u) - | permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), - forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) - | permut_trans : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) - (a3:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> - ((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u)) - | permut_exchange : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), - forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> - (((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 - a2 l u))). - -Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, - forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l1:Z) (r1:Z) - (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> - ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). - -Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z - a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> - forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2 - i) = (map.Map.get a1 i)). - -Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, - forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), - (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> - exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a2 - i) = (map.Map.get a1 j)). +Definition lt (a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in + (((0%Z <= x)%Z /\ (x <= n)%Z) /\ (((0%Z <= y)%Z /\ (y <= n)%Z) /\ + exists l:Z, (is_common_prefix a x y l) /\ (((y + l)%Z < n)%Z /\ + (((x + l)%Z = n) \/ ((get a (x + l)%Z) < (get a (y + l)%Z))%Z)))). (* Why3 assumption *) -Definition exchange1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a)) - (i:Z) (j:Z): Prop := (exchange (elts a1) (elts a2) i j). +Definition le (a:(array Z)) (x:Z) (y:Z): Prop := (x = y) \/ (lt a x y). + +Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ + (x <= (length a))%Z) -> (le a x x). + +Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ + (x <= (length a))%Z) -> (is_longest_common_prefix a x x + ((length a) - x)%Z). + +Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z) + (l:Z), ((0%Z <= l)%Z /\ (((x + l)%Z < (length a))%Z /\ + (((y + l)%Z < (length a))%Z /\ ~ ((get a (x + l)%Z) = (get a + (y + l)%Z))))) -> ~ (is_common_prefix a x y (l + 1%Z)%Z). + +Axiom longest_common_prefix_succ : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), + ((is_common_prefix a x y l) /\ ~ (is_common_prefix a x y (l + 1%Z)%Z)) -> + (is_longest_common_prefix a x y l). + +Axiom le_trans : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ + (((0%Z <= z)%Z /\ (z <= (length a))%Z) /\ ((le a x y) /\ (le a y z))))) -> + (le a x z). (* Why3 assumption *) -Definition permut_sub1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array - a)) (l:Z) (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u). +Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ + (injective m u). + +(* Why3 assumption *) +Definition sorted_sub (a:(array Z)) (data:(map.Map.map Z Z)) (l:Z) + (u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ + (i2 < u)%Z) -> (le a (map.Map.get data i1) (map.Map.get data i2)). + +(* Why3 assumption *) +Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a + (elts data) 0%Z (length data)). + +(* Why3 assumption *) +Definition exchange {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a)) + (i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j). + +(* Why3 assumption *) +Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a)) + (l:Z) (u:Z): Prop := (map.MapPermut.permut_sub (elts a1) (elts a2) l u). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array - a)): Prop := ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) - 0%Z (length a1)). + a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub + (elts a1) (elts a2) 0%Z (length a1)). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array - a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) -> + a)) (a2:(array a)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (((length a1) = (length a2)) -> (((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))). -Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) +Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)), (permut a1 a2) -> (permut a2 a1). -Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) +Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). @@ -157,94 +168,11 @@ Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l - u) -> (permut_sub1 a1 a2 l u). + u) -> (permut_sub a1 a2 l u). Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2). -(* Why3 assumption *) -Definition is_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := - (0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\ - (((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\ - (i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))). - -Axiom common_prefix_eq : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ - (x <= (length a))%Z) -> (is_common_prefix a x x ((length a) - x)%Z). - -Axiom common_prefix_eq2 : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ - (x <= (length a))%Z) -> ~ (is_common_prefix a x x - (((length a) - x)%Z + 1%Z)%Z). - -Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z) - (l:Z), ((0%Z < l)%Z /\ (((x + l)%Z < (length a))%Z /\ - (((y + l)%Z < (length a))%Z /\ ~ ((get a (x + (l - 1%Z)%Z)%Z) = (get a - (y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l). - -(* Why3 assumption *) -Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := - (is_common_prefix a x y l) /\ ~ (is_common_prefix a x y (l + 1%Z)%Z). - -Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> - ((is_longest_common_prefix a x y l) -> (is_common_prefix a x y l)). - -Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> - ((is_longest_common_prefix a x y l) -> forall (i:Z), ((0%Z <= i)%Z /\ - (i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z))). - -Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ - (x <= (length a))%Z) -> (is_longest_common_prefix a x x - ((length a) - x)%Z). - -Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> - ((is_longest_common_prefix a x y l) -> (is_longest_common_prefix a y x l)). - -(* Why3 assumption *) -Definition le (a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in - (((0%Z <= x)%Z /\ (x <= n)%Z) /\ (((0%Z <= y)%Z /\ (y <= n)%Z) /\ - exists l:Z, (is_common_prefix a x y l) /\ (((x + l)%Z = n) \/ - (((x + l)%Z < n)%Z /\ (((y + l)%Z < n)%Z /\ ((get a (x + l)%Z) <= (get a - (y + l)%Z))%Z))))). - -Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ - (x <= (length a))%Z) -> (le a x x). - -Axiom le_trans : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ - (((0%Z <= z)%Z /\ (z <= (length a))%Z) /\ ((le a x y) /\ (le a y z))))) -> - (le a x z). - -Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ ~ (le a x - y))) -> (le a y x). - -(* Why3 assumption *) -Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ - (injective m u). - -(* Why3 assumption *) -Definition sorted_sub (a:(array Z)) (data:(map.Map.map Z Z)) (l:Z) - (u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ - (i2 < u)%Z) -> (le a (map.Map.get data i1) (map.Map.get data i2)). - -(* Why3 assumption *) -Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a - (elts data) 0%Z (length data)). - -Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 - a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2) - (length a2))). - -Axiom lcp_le_le_aux : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z), ((le a x - y) /\ (le a y z)) -> ((is_common_prefix a x z l) -> (is_common_prefix a y z - l)). - -Axiom lcp_le_le : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z) (m:Z), ((le a - x y) /\ (le a y z)) -> (((is_longest_common_prefix a x z l) /\ - (is_longest_common_prefix a y z m)) -> (l <= m)%Z). - (* Why3 assumption *) Inductive suffixArray := | mk_suffixArray : (array Z) -> (array Z) -> suffixArray. @@ -269,6 +197,21 @@ Definition inv (s:suffixArray): Prop := (elts (suffixes s)) (length (suffixes s))) /\ (sorted (values s) (suffixes s))). +Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 + a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2) + (length a2))). + +Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> + ((is_longest_common_prefix a x y l) -> (is_longest_common_prefix a y x l)). + +Axiom le_le_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z), + ((le a x y) /\ (le a y z)) -> ((is_common_prefix a x z l) -> + (is_common_prefix a y z l)). + +Axiom le_le_longest_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) + (l:Z) (m:Z), ((le a x y) /\ (le a y z)) -> (((is_longest_common_prefix a x + z l) /\ (is_longest_common_prefix a y z m)) -> (l <= m)%Z). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. @@ -277,12 +220,13 @@ Ltac ae := why3 "alt-ergo" timelimit 3. Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\ (0%Z < a)%Z) -> forall (sa:Z) (sa1:(map.Map.map Z Z)) (sa2:Z) (sa3:(map.Map.map Z Z)), - (((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z) /\ (((sa = a) /\ (sa1 = a1)) /\ (inv - (mk_suffixArray (mk_array sa sa1) (mk_array sa2 sa3))))) -> ((permutation - sa3 sa2) -> forall (solStart:Z), (solStart = 0%Z) -> forall (solLength:Z), - (solLength = 0%Z) -> forall (solStart2:Z), (solStart2 = a) -> - ((1%Z <= (a - 1%Z)%Z)%Z -> forall (solStart21:Z) (solLength1:Z) - (solStart1:Z), (((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\ + ((((sa = sa2) /\ ((permutation sa3 sa2) /\ (sorted_sub (mk_array sa sa1) + sa3 0%Z sa2))) /\ ((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z)) /\ ((sa = a) /\ + (sa1 = a1))) -> ((permutation sa3 sa2) -> forall (solStart:Z), + (solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) -> + forall (solStart2:Z), (solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z -> + forall (solStart21:Z) (solLength1:Z) (solStart1:Z), + (((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\ ((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ (((0%Z <= solStart21)%Z /\ (solStart21 <= a)%Z) /\ ((~ (solStart1 = solStart21)) /\ (is_longest_common_prefix a2 solStart1 solStart21 solLength1)))) /\ @@ -296,17 +240,21 @@ Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)), (x < y)%Z) /\ (y < a)%Z) -> exists j:Z, exists k:Z, ((0%Z <= j)%Z /\ (j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\ ((x = (map.Map.get sa3 j)) /\ (y = (map.Map.get sa3 k)))))))))). -intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 ((h3,h4),((h5,h6),h7)) h8 solStart h9 -solLength h10 solStart2 h11 h12 solStart21 solLength1 solStart1 -((((h13,h14),(h15,h16)),((h17,h18),(h19,h20))),h21) h22 h23 x y -((h24,h25),h26). +(* intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10 + solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1 + solStart1 ((((h15,h16),(h17,h18)),((h19,h20),(h21,h22))),h23) h24 h25 x y + ((h26,h27),h28). *) +intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10 + solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1 + solStart1 ((((h15,h16),(h17,h18)),((h19,h20),(h21,h22))),h23) h24 h25 x y + ((h26,h27),h28). assert (h: sa2 = a) by ae. -subst sa2. -red in h22. +subst sa2 sa. +red in h24. assert (ha : (0 <= x < a)%Z) by omega. -destruct (h22 _ ha) as (j & h30 & h31). +destruct (h24 _ ha) as (j & h30 & h31). assert (hb : (0 <= y < a)%Z) by omega. -destruct (h22 _ hb) as (k & k32 & h33). +destruct (h24 _ hb) as (k & k32 & h33). exists j. exists k. ae. diff --git a/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_11.v b/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_11.v index 974968b44cea7438359d28e9bff6daa8e0d6c4ed..178342e9346ed17b290ec2cc212375acca94c701 100644 --- a/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_11.v +++ b/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_11.v @@ -1,4 +1,4 @@ -(* This file is generated by Why3's Coq driver *) +(* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. @@ -74,70 +74,81 @@ Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a n) -> ((range a n) -> (surjective a n)). (* Why3 assumption *) -Definition exchange {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a)) - (a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1 - i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\ - forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1 - k) = (map.Map.get a2 k))). +Definition is_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := + (0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\ + (((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\ + (i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))). -Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, - forall (a1:(map.Map.map Z a)), forall (i:Z) (j:Z), (exchange a1 - (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i - j). +(* Why3 assumption *) +Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := + (is_common_prefix a x y l) /\ forall (m:Z), (l < m)%Z -> + ~ (is_common_prefix a x y m). (* Why3 assumption *) -Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a) - -> (map.Map.map Z a) -> Z -> Z -> Prop := - | permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z), - (permut_sub a1 a1 l u) - | permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), - forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) - | permut_trans : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) - (a3:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> - ((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u)) - | permut_exchange : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), - forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> - (((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 - a2 l u))). - -Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, - forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l1:Z) (r1:Z) - (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> - ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). - -Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z - a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> - forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2 - i) = (map.Map.get a1 i)). - -Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, - forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), - (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> - exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a2 - i) = (map.Map.get a1 j)). +Definition lt (a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in + (((0%Z <= x)%Z /\ (x <= n)%Z) /\ (((0%Z <= y)%Z /\ (y <= n)%Z) /\ + exists l:Z, (is_common_prefix a x y l) /\ (((y + l)%Z < n)%Z /\ + (((x + l)%Z = n) \/ ((get a (x + l)%Z) < (get a (y + l)%Z))%Z)))). (* Why3 assumption *) -Definition exchange1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a)) - (i:Z) (j:Z): Prop := (exchange (elts a1) (elts a2) i j). +Definition le (a:(array Z)) (x:Z) (y:Z): Prop := (x = y) \/ (lt a x y). + +Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ + (x <= (length a))%Z) -> (le a x x). + +Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ + (x <= (length a))%Z) -> (is_longest_common_prefix a x x + ((length a) - x)%Z). + +Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z) + (l:Z), ((0%Z <= l)%Z /\ (((x + l)%Z < (length a))%Z /\ + (((y + l)%Z < (length a))%Z /\ ~ ((get a (x + l)%Z) = (get a + (y + l)%Z))))) -> ~ (is_common_prefix a x y (l + 1%Z)%Z). + +Axiom longest_common_prefix_succ : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), + ((is_common_prefix a x y l) /\ ~ (is_common_prefix a x y (l + 1%Z)%Z)) -> + (is_longest_common_prefix a x y l). + +Axiom le_trans : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ + (((0%Z <= z)%Z /\ (z <= (length a))%Z) /\ ((le a x y) /\ (le a y z))))) -> + (le a x z). (* Why3 assumption *) -Definition permut_sub1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array - a)) (l:Z) (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u). +Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ + (injective m u). + +(* Why3 assumption *) +Definition sorted_sub (a:(array Z)) (data:(map.Map.map Z Z)) (l:Z) + (u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ + (i2 < u)%Z) -> (le a (map.Map.get data i1) (map.Map.get data i2)). + +(* Why3 assumption *) +Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a + (elts data) 0%Z (length data)). + +(* Why3 assumption *) +Definition exchange {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a)) + (i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j). + +(* Why3 assumption *) +Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a)) + (l:Z) (u:Z): Prop := (map.MapPermut.permut_sub (elts a1) (elts a2) l u). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array - a)): Prop := ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) - 0%Z (length a1)). + a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub + (elts a1) (elts a2) 0%Z (length a1)). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array - a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) -> + a)) (a2:(array a)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (((length a1) = (length a2)) -> (((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))). -Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) +Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)), (permut a1 a2) -> (permut a2 a1). -Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) +Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). @@ -157,94 +168,11 @@ Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l - u) -> (permut_sub1 a1 a2 l u). + u) -> (permut_sub a1 a2 l u). Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2). -(* Why3 assumption *) -Definition is_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := - (0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\ - (((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\ - (i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))). - -Axiom common_prefix_eq : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ - (x <= (length a))%Z) -> (is_common_prefix a x x ((length a) - x)%Z). - -Axiom common_prefix_eq2 : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ - (x <= (length a))%Z) -> ~ (is_common_prefix a x x - (((length a) - x)%Z + 1%Z)%Z). - -Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z) - (l:Z), ((0%Z < l)%Z /\ (((x + l)%Z < (length a))%Z /\ - (((y + l)%Z < (length a))%Z /\ ~ ((get a (x + (l - 1%Z)%Z)%Z) = (get a - (y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l). - -(* Why3 assumption *) -Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := - (is_common_prefix a x y l) /\ ~ (is_common_prefix a x y (l + 1%Z)%Z). - -Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> - ((is_longest_common_prefix a x y l) -> (is_common_prefix a x y l)). - -Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> - ((is_longest_common_prefix a x y l) -> forall (i:Z), ((0%Z <= i)%Z /\ - (i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z))). - -Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ - (x <= (length a))%Z) -> (is_longest_common_prefix a x x - ((length a) - x)%Z). - -Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> - ((is_longest_common_prefix a x y l) -> (is_longest_common_prefix a y x l)). - -(* Why3 assumption *) -Definition le (a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in - (((0%Z <= x)%Z /\ (x <= n)%Z) /\ (((0%Z <= y)%Z /\ (y <= n)%Z) /\ - exists l:Z, (is_common_prefix a x y l) /\ (((x + l)%Z = n) \/ - (((x + l)%Z < n)%Z /\ (((y + l)%Z < n)%Z /\ ((get a (x + l)%Z) <= (get a - (y + l)%Z))%Z))))). - -Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ - (x <= (length a))%Z) -> (le a x x). - -Axiom le_trans : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ - (((0%Z <= z)%Z /\ (z <= (length a))%Z) /\ ((le a x y) /\ (le a y z))))) -> - (le a x z). - -Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ - (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ ~ (le a x - y))) -> (le a y x). - -(* Why3 assumption *) -Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ - (injective m u). - -(* Why3 assumption *) -Definition sorted_sub (a:(array Z)) (data:(map.Map.map Z Z)) (l:Z) - (u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ - (i2 < u)%Z) -> (le a (map.Map.get data i1) (map.Map.get data i2)). - -(* Why3 assumption *) -Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a - (elts data) 0%Z (length data)). - -Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 - a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2) - (length a2))). - -Axiom lcp_le_le_aux : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z), ((le a x - y) /\ (le a y z)) -> ((is_common_prefix a x z l) -> (is_common_prefix a y z - l)). - -Axiom lcp_le_le : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z) (m:Z), ((le a - x y) /\ (le a y z)) -> (((is_longest_common_prefix a x z l) /\ - (is_longest_common_prefix a y z m)) -> (l <= m)%Z). - (* Why3 assumption *) Inductive suffixArray := | mk_suffixArray : (array Z) -> (array Z) -> suffixArray. @@ -269,6 +197,21 @@ Definition inv (s:suffixArray): Prop := (elts (suffixes s)) (length (suffixes s))) /\ (sorted (values s) (suffixes s))). +Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 + a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2) + (length a2))). + +Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> + ((is_longest_common_prefix a x y l) -> (is_longest_common_prefix a y x l)). + +Axiom le_le_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z), + ((le a x y) /\ (le a y z)) -> ((is_common_prefix a x z l) -> + (is_common_prefix a y z l)). + +Axiom le_le_longest_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) + (l:Z) (m:Z), ((le a x y) /\ (le a y z)) -> (((is_longest_common_prefix a x + z l) /\ (is_longest_common_prefix a y z m)) -> (l <= m)%Z). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. @@ -277,32 +220,39 @@ Ltac ae := why3 "alt-ergo" timelimit 3. Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\ (0%Z < a)%Z) -> forall (sa:Z) (sa1:(map.Map.map Z Z)) (sa2:Z) (sa3:(map.Map.map Z Z)), - (((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z) /\ (((sa = a) /\ (sa1 = a1)) /\ (inv - (mk_suffixArray (mk_array sa sa1) (mk_array sa2 sa3))))) -> ((permutation - sa3 sa2) -> forall (solStart:Z), (solStart = 0%Z) -> forall (solLength:Z), - (solLength = 0%Z) -> forall (solStart2:Z), (solStart2 = a) -> - ((1%Z <= (a - 1%Z)%Z)%Z -> forall (solStart21:Z) (solLength1:Z) - (solStart1:Z), (((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\ - ((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ (((0%Z <= solStart21)%Z /\ - (solStart21 <= a)%Z) /\ ((~ (solStart1 = solStart21)) /\ - (is_longest_common_prefix a2 solStart1 solStart21 solLength1)))) /\ - forall (j:Z) (k:Z) (l:Z), ((((0%Z <= j)%Z /\ (j < k)%Z) /\ - (k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) /\ (is_longest_common_prefix a2 - (map.Map.get sa3 j) (map.Map.get sa3 k) l)) -> (l <= solLength1)%Z) -> - ((surjective sa3 sa2) -> ((forall (j:Z) (k:Z) (l:Z), (((0%Z <= j)%Z /\ - (j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\ - (is_longest_common_prefix a2 (map.Map.get sa3 j) (map.Map.get sa3 k) - l)))) -> (l <= solLength1)%Z) -> ((forall (x:Z) (y:Z), (((0%Z <= x)%Z /\ - (x < y)%Z) /\ (y < a)%Z) -> exists j:Z, exists k:Z, ((0%Z <= j)%Z /\ - (j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\ - ((x = (map.Map.get sa3 j)) /\ (y = (map.Map.get sa3 k)))))) -> forall (x:Z) - (y:Z) (l:Z), ((((0%Z <= x)%Z /\ (x < y)%Z) /\ (y < a)%Z) /\ - (is_longest_common_prefix a2 x y l)) -> (l <= solLength1)%Z)))))). + ((((sa = sa2) /\ ((permutation sa3 sa2) /\ (sorted_sub (mk_array sa sa1) + sa3 0%Z sa2))) /\ ((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z)) /\ ((sa = a) /\ + (sa1 = a1))) -> ((permutation sa3 sa2) -> forall (solStart:Z), + (solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) -> + forall (solStart2:Z), (solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z -> + forall (solStart21:Z) (solLength1:Z) (solStart1:Z), forall (i:Z), + ((1%Z <= i)%Z /\ (i <= (a - 1%Z)%Z)%Z) -> ((((((0%Z <= solLength1)%Z /\ + (solLength1 <= a)%Z) /\ ((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ + (((0%Z <= solStart21)%Z /\ (solStart21 <= a)%Z) /\ + ((~ (solStart1 = solStart21)) /\ (is_longest_common_prefix a2 solStart1 + solStart21 solLength1)))) /\ forall (j:Z) (k:Z) (l:Z), ((((0%Z <= j)%Z /\ + (j < k)%Z) /\ (k < i)%Z) /\ (is_longest_common_prefix a2 (map.Map.get sa3 + j) (map.Map.get sa3 k) l)) -> (l <= solLength1)%Z) -> (((inv + (mk_suffixArray (mk_array sa sa1) (mk_array sa2 sa3))) /\ ((0%Z < i)%Z /\ + (i < sa)%Z)) -> forall (l:Z), (is_longest_common_prefix (mk_array sa sa1) + (map.Map.get sa3 (i - 1%Z)%Z) (map.Map.get sa3 i) l) -> ((forall (j:Z), + ((0%Z <= j)%Z /\ (j < i)%Z) -> (le a2 (map.Map.get sa3 j) (map.Map.get sa3 + i))) -> ((forall (j:Z) (m:Z), (((0%Z <= j)%Z /\ (j < i)%Z) /\ + (is_longest_common_prefix a2 (map.Map.get sa3 j) (map.Map.get sa3 i) m)) -> + (m <= l)%Z) -> forall (j:Z) (k:Z) (m:Z), ((((0%Z <= j)%Z /\ (j < k)%Z) /\ + (k < (i - 1%Z)%Z)%Z) /\ (is_longest_common_prefix a2 (map.Map.get sa3 j) + (map.Map.get sa3 k) m)) -> (m <= solLength1)%Z))))))). +intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10 + solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1 + solStart1 i (h15,h16) ((((h17,h18),(h19,h20)),((h21,h22),(h23,h24))),h25) + (h26,(h27,h28)) l h29 h30 h31 j k m (((h32,h33),h34),h35). +(* intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 ((h3,h4),((h5,h6),h7)) h8 solStart h9 solLength h10 solStart2 h11 h12 solStart21 solLength1 solStart1 ((((h13,h14),(h15,h16)),((h17,h18),(h19,h20))),h21) h22 h23 h24 x y l (h25,h28). elim (h24 _ _ h25). +*) ae. Qed. diff --git a/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_12.v b/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_12.v new file mode 100644 index 0000000000000000000000000000000000000000..964eabf7ad47a77e8addccd108f4fcba13b51a5d --- /dev/null +++ b/examples/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_12.v @@ -0,0 +1,254 @@ +(* This file is generated by Why3's Coq 8.4 driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. +Require int.MinMax. +Require map.Map. +Require map.MapPermut. + +(* Why3 assumption *) +Definition unit := unit. + +(* Why3 assumption *) +Inductive ref (a:Type) {a_WT:WhyType a} := + | 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]]. + +(* Why3 assumption *) +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) -> 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]]. + +(* Why3 assumption *) +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)): Z := + match v with + | (mk_array x x1) => x + end. + +(* Why3 assumption *) +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)) (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) := + (mk_array n (map.Map.const v:(map.Map.map Z a))). + +(* Why3 assumption *) +Definition injective (a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z), + ((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < n)%Z) -> + ((~ (i = j)) -> ~ ((map.Map.get a i) = (map.Map.get a j)))). + +(* Why3 assumption *) +Definition surjective (a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z), + ((0%Z <= i)%Z /\ (i < n)%Z) -> exists j:Z, ((0%Z <= j)%Z /\ (j < n)%Z) /\ + ((map.Map.get a j) = i). + +(* Why3 assumption *) +Definition range (a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z), + ((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (map.Map.get a i))%Z /\ + ((map.Map.get a i) < n)%Z). + +Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a + n) -> ((range a n) -> (surjective a n)). + +(* Why3 assumption *) +Definition is_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := + (0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\ + (((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\ + (i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))). + +(* Why3 assumption *) +Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := + (is_common_prefix a x y l) /\ forall (m:Z), (l < m)%Z -> + ~ (is_common_prefix a x y m). + +(* Why3 assumption *) +Definition lt (a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in + (((0%Z <= x)%Z /\ (x <= n)%Z) /\ (((0%Z <= y)%Z /\ (y <= n)%Z) /\ + exists l:Z, (is_common_prefix a x y l) /\ (((y + l)%Z < n)%Z /\ + (((x + l)%Z = n) \/ ((get a (x + l)%Z) < (get a (y + l)%Z))%Z)))). + +(* Why3 assumption *) +Definition le (a:(array Z)) (x:Z) (y:Z): Prop := (x = y) \/ (lt a x y). + +Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ + (x <= (length a))%Z) -> (le a x x). + +Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ + (x <= (length a))%Z) -> (is_longest_common_prefix a x x + ((length a) - x)%Z). + +Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z) + (l:Z), ((0%Z <= l)%Z /\ (((x + l)%Z < (length a))%Z /\ + (((y + l)%Z < (length a))%Z /\ ~ ((get a (x + l)%Z) = (get a + (y + l)%Z))))) -> ~ (is_common_prefix a x y (l + 1%Z)%Z). + +Axiom longest_common_prefix_succ : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), + ((is_common_prefix a x y l) /\ ~ (is_common_prefix a x y (l + 1%Z)%Z)) -> + (is_longest_common_prefix a x y l). + +Axiom le_trans : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ + (((0%Z <= z)%Z /\ (z <= (length a))%Z) /\ ((le a x y) /\ (le a y z))))) -> + (le a x z). + +(* Why3 assumption *) +Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ + (injective m u). + +(* Why3 assumption *) +Definition sorted_sub (a:(array Z)) (data:(map.Map.map Z Z)) (l:Z) + (u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ + (i2 < u)%Z) -> (le a (map.Map.get data i1) (map.Map.get data i2)). + +(* Why3 assumption *) +Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a + (elts data) 0%Z (length data)). + +(* Why3 assumption *) +Definition exchange {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a)) + (i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j). + +(* Why3 assumption *) +Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a)) + (l:Z) (u:Z): Prop := (map.MapPermut.permut_sub (elts a1) (elts a2) l u). + +(* Why3 assumption *) +Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array + a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub + (elts a1) (elts a2) 0%Z (length a1)). + +Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array + a)) (a2:(array a)) (i:Z) (j:Z), (exchange a1 a2 i j) -> + (((length a1) = (length a2)) -> (((0%Z <= i)%Z /\ (i < (length a1))%Z) -> + (((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))). + +Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) + (a2:(array a)), (permut a1 a2) -> (permut a2 a1). + +Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) + (a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut + a1 a3)). + +(* Why3 assumption *) +Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a)) + (a2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ + (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)). + +(* Why3 assumption *) +Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array + a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). + +(* Why3 assumption *) +Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array + a)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z + (length a1)). + +Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a}, + forall (a1:(array a)) (a2:(array a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l + u) -> (permut_sub a1 a2 l u). + +Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array + a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2). + +(* Why3 assumption *) +Inductive suffixArray := + | mk_suffixArray : (array Z) -> (array Z) -> suffixArray. +Axiom suffixArray_WhyType : WhyType suffixArray. +Existing Instance suffixArray_WhyType. + +(* Why3 assumption *) +Definition suffixes (v:suffixArray): (array Z) := + match v with + | (mk_suffixArray x x1) => x1 + end. + +(* Why3 assumption *) +Definition values (v:suffixArray): (array Z) := + match v with + | (mk_suffixArray x x1) => x + end. + +(* Why3 assumption *) +Definition inv (s:suffixArray): Prop := + ((length (values s)) = (length (suffixes s))) /\ ((permutation + (elts (suffixes s)) (length (suffixes s))) /\ (sorted (values s) + (suffixes s))). + +Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 + a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2) + (length a2))). + +Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> + ((is_longest_common_prefix a x y l) -> (is_longest_common_prefix a y x l)). + +Axiom le_le_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z), + ((le a x y) /\ (le a y z)) -> ((is_common_prefix a x z l) -> + (is_common_prefix a y z l)). + +Axiom le_le_longest_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) + (l:Z) (m:Z), ((le a x y) /\ (le a y z)) -> (((is_longest_common_prefix a x + z l) /\ (is_longest_common_prefix a y z m)) -> (l <= m)%Z). + + +Require Import Why3. +Ltac ae := why3 "alt-ergo" timelimit 3. + +(* Why3 goal *) +Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)), + let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\ (0%Z < a)%Z) -> + forall (sa:Z) (sa1:(map.Map.map Z Z)) (sa2:Z) (sa3:(map.Map.map Z Z)), + ((((sa = sa2) /\ ((permutation sa3 sa2) /\ (sorted_sub (mk_array sa sa1) + sa3 0%Z sa2))) /\ ((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z)) /\ ((sa = a) /\ + (sa1 = a1))) -> ((permutation sa3 sa2) -> forall (solStart:Z), + (solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) -> + forall (solStart2:Z), (solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z -> + forall (solStart21:Z) (solLength1:Z) (solStart1:Z), + (((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\ + ((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ (((0%Z <= solStart21)%Z /\ + (solStart21 <= a)%Z) /\ ((~ (solStart1 = solStart21)) /\ + (is_longest_common_prefix a2 solStart1 solStart21 solLength1)))) /\ + forall (j:Z) (k:Z) (l:Z), ((((0%Z <= j)%Z /\ (j < k)%Z) /\ + (k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) /\ (is_longest_common_prefix a2 + (map.Map.get sa3 j) (map.Map.get sa3 k) l)) -> (l <= solLength1)%Z) -> + ((surjective sa3 sa2) -> ((forall (j:Z) (k:Z) (l:Z), (((0%Z <= j)%Z /\ + (j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\ + (is_longest_common_prefix a2 (map.Map.get sa3 j) (map.Map.get sa3 k) + l)))) -> (l <= solLength1)%Z) -> ((forall (x:Z) (y:Z), (((0%Z <= x)%Z /\ + (x < y)%Z) /\ (y < a)%Z) -> exists j:Z, exists k:Z, ((0%Z <= j)%Z /\ + (j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\ + ((x = (map.Map.get sa3 j)) /\ (y = (map.Map.get sa3 k)))))) -> forall (x:Z) + (y:Z) (l:Z), ((((0%Z <= x)%Z /\ (x < y)%Z) /\ (y < a)%Z) /\ + (is_longest_common_prefix a2 x y l)) -> (l <= solLength1)%Z)))))). +intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10 +solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1 solStart1 +((((h15,h16),(h17,h18)),((h19,h20),(h21,h22))),h23) h24 h25 h26 x y l +(h27,h30). +elim (h26 _ _ h27). +ae. +Qed. + + diff --git a/examples/verifythis_fm2012_lcp/why3session.xml b/examples/verifythis_fm2012_lcp/why3session.xml index 109b81b4c596ba1a1a28c5543960fb7b7c9388da..1f4d0631fc5718cc11c1061facff36d40cba5459 100644 --- a/examples/verifythis_fm2012_lcp/why3session.xml +++ b/examples/verifythis_fm2012_lcp/why3session.xml @@ -48,17 +48,17 @@ + expanded="false"> @@ -2153,13 +3705,13 @@ + shape="ainfix =agetV3V2agetV3V2Aainfix <V2V1Aainfix <=c0V2Iainfix <V2V0Aainfix <=c0V2Aainfix <=c0V1Aainfix <=c0V0Aasorted_subamk arrayV0V4V3c0V1AapermutationV3V1Aainfix =V0V1FF"> + shape="ainfix =V2V2Aasorted_subV2V4c0V0AapermutationV4V0Aainfix =V0V0Iapermutamk arrayV0V3amk arrayV0V4Aasorted_subV2V4c0V0Aainfix <=c0V0FAarangeV3V0Aainfix =V0V0Aainfix <=c0V0Iainfix =agetV3V5V5Iainfix <V5ainfix +ainfix -V0c1c1Aainfix <=c0V5FAainfix =agetV7V8V8Iainfix <V8ainfix +V6c1Aainfix <=c0V8FIainfix =V7asetV3V6V6Aainfix <=c0V0FAainfix <V6V0Aainfix <=c0V6Aainfix <=c0V0Iainfix =agetV3V9V9Iainfix <V9V6Aainfix <=c0V9FIainfix <=V6ainfix -V0c1Aainfix <=c0V6FFAainfix =agetaconstc0V10V10Iainfix <V10c0Aainfix <=c0V10FIainfix <=c0ainfix -V0c1Aainfix =V2V2Aasorted_subV2V11c0V0AapermutationV11V0Aainfix =V0V0Iapermutamk arrayV0aconstc0amk arrayV0V11Aasorted_subV2V11c0V0Aainfix <=c0V0FAarangeaconstc0V0Aainfix =V0V0Iainfix >c0ainfix -V0c1Iainfix <=c0V0Aainfix >=V0c0Iainfix <=c0V0Lamk arrayV0V1FF"> + + shape="asorted_subV2V4c0V0AapermutationV4V0Aainfix =V0V0Iapermutamk arrayV0V3amk arrayV0V4Aasorted_subV2V4c0V0Aainfix <=c0V0FIarangeV3V0Aainfix =V0V0Aainfix <=c0V0Iainfix =agetV3V5V5Iainfix <V5ainfix +ainfix -V0c1c1Aainfix <=c0V5FFIainfix <=c0ainfix -V0c1Iainfix <=c0V0Iainfix >=V0c0Iainfix <=c0V0Lamk arrayV0V1FF"> + + @@ -5663,12 +7255,12 @@ + shape="ais_longest_common_prefixamk arrayV0V4agetV3ainfix -V2c1agetV3V2V7Iais_longest_common_prefixamk arrayV0V4V6V5V7FAainfix <=V5V0Aainfix <=c0V5Aainfix <=V6V0Aainfix <=c0V6LagetV3V2Aainfix <V2V1Aainfix <=c0V2LagetV3ainfix -V2c1Aainfix <ainfix -V2c1V1Aainfix <=c0ainfix -V2c1Iainfix <V2V0Aainfix <c0V2Aainvamk suffixArrayamk arrayV0V4amk arrayV1V3Aainfix <=c0V1Aainfix <=c0V0Aasorted_subamk arrayV0V4V3c0V1AapermutationV3V1Aainfix =V0V1FF"> + shape="ainfix <=V6V0Aainfix <=c0V6LagetV3V2Iainfix <V2V1Aainfix <=c0V2LagetV3ainfix -V2c1Iainfix <ainfix -V2c1V1Aainfix <=c0ainfix -V2c1Iainfix <V2V0Aainfix <c0V2Aainvamk suffixArrayamk arrayV0V4amk arrayV1V3Aainfix <=c0V1Aainfix <=c0V0Aasorted_subamk arrayV0V4V3c0V1AapermutationV3V1Aainfix =V0V1FF"> + shape="ainfix =V11agetV6V13Aainfix =V10agetV6V12Aainfix =V12V13NAainfix <V13V0Aainfix <=c0V13Aainfix <V12V0Aainfix <=c0V12EIainfix <V11V0Aainfix <V10V11Aainfix <=c0V10FIainfix >=V8V16Iais_longest_common_prefixV2agetV6V14agetV6V15V16Aainfix =V14V15NAainfix <V15V0Aainfix <=c0V15Aainfix <V14V0Aainfix <=c0V14FIasurjectiveV6V5Iainfix >c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF"> + shape="ais_longest_common_prefixV2V7V9V8Aainfix =V7V9NAainfix <=V9V0Aainfix <=c0V9Iainfix =V11agetV6V13Aainfix =V10agetV6V12Aainfix =V12V13NAainfix <V13V0Aainfix <=c0V13Aainfix <V12V0Aainfix <=c0V12EIainfix <V11V0Aainfix <V10V11Aainfix <=c0V10FIainfix >=V8V16Iais_longest_common_prefixV2agetV6V14agetV6V15V16Aainfix =V14V15NAainfix <V15V0Aainfix <=c0V15Aainfix <V14V0Aainfix <=c0V14FIasurjectiveV6V5Iainfix >c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF"> + + - - + shape="ainfix <=V8V0Aainfix <=c0V8Iainfix <=c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF"> + shape="ainfix <=V7V0Aainfix <=c0V7Iainfix <=c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF"> + + - - + shape="ainfix >=V8V12Iais_longest_common_prefixV2agetV6V10agetV6V11V12Aainfix <V11c1Aainfix <V10V11Aainfix <=c0V10FIainfix <=c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF"> + shape="ainfix <V13V3Aainfix <c0V13Iainfix >=V11V16Iais_longest_common_prefixV2agetV6V14agetV6V15V16Aainfix <V15V13Aainfix <V14V15Aainfix <=c0V14FAais_longest_common_prefixV2V12V10V11Aainfix =V12V10NAainfix <=V10V0Aainfix <=c0V10Aainfix <=V12V0Aainfix <=c0V12Aainfix <=V11V0Aainfix <=c0V11Iainfix <=V13ainfix -V0c1Aainfix <=c1V13FFIainfix <=c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF"> + shape="aleV2agetV6V15agetV6V13Iainfix <V15V13Aainfix <=c0V15FIais_longest_common_prefixamk arrayV3V4agetV6ainfix -V13c1agetV6V13V14FIainfix <V13V3Aainfix <c0V13Aainvamk suffixArrayamk arrayV3V4amk arrayV5V6Iainfix >=V11V18Iais_longest_common_prefixV2agetV6V16agetV6V17V18Aainfix <V17V13Aainfix <V16V17Aainfix <=c0V16FAais_longest_common_prefixV2V12V10V11Aainfix =V12V10NAainfix <=V10V0Aainfix <=c0V10Aainfix <=V12V0Aainfix <=c0V12Aainfix <=V11V0Aainfix <=c0V11Iainfix <=V13ainfix -V0c1Aainfix <=c1V13FFIainfix <=c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF"> + shape="ainfix <=V16V14Iais_longest_common_prefixV2agetV6V15agetV6V13V16Aainfix <V15V13Aainfix <=c0V15FIaleV2agetV6V17agetV6V13Iainfix <V17V13Aainfix <=c0V17FIais_longest_common_prefixamk arrayV3V4agetV6ainfix -V13c1agetV6V13V14FIainfix <V13V3Aainfix <c0V13Aainvamk suffixArrayamk arrayV3V4amk arrayV5V6Iainfix >=V11V20Iais_longest_common_prefixV2agetV6V18agetV6V19V20Aainfix <V19V13Aainfix <V18V19Aainfix <=c0V18FAais_longest_common_prefixV2V12V10V11Aainfix =V12V10NAainfix <=V10V0Aainfix <=c0V10Aainfix <=V12V0Aainfix <=c0V12Aainfix <=V11V0Aainfix <=c0V11Iainfix <=V13ainfix -V0c1Aainfix <=c1V13FFIainfix <=c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF"> + shape="ainfix >=V11V17Iais_longest_common_prefixV2agetV6V15agetV6V16V17Aainfix <V16ainfix -V13c1Aainfix <V15V16Aainfix <=c0V15FIainfix <=V19V14Iais_longest_common_prefixV2agetV6V18agetV6V13V19Aainfix <V18V13Aainfix <=c0V18FIaleV2agetV6V20agetV6V13Iainfix <V20V13Aainfix <=c0V20FIais_longest_common_prefixamk arrayV3V4agetV6ainfix -V13c1agetV6V13V14FIainfix <V13V3Aainfix <c0V13Aainvamk suffixArrayamk arrayV3V4amk arrayV5V6Iainfix >=V11V23Iais_longest_common_prefixV2agetV6V21agetV6V22V23Aainfix <V22V13Aainfix <V21V22Aainfix <=c0V21FAais_longest_common_prefixV2V12V10V11Aainfix =V12V10NAainfix <=V10V0Aainfix <=c0V10Aainfix <=V12V0Aainfix <=c0V12Aainfix <=V11V0Aainfix <=c0V11Iainfix <=V13ainfix -V0c1Aainfix <=c1V13FFIainfix <=c1ainfix -V0c1Iainfix =V9V0FIainfix =V8c0FIainfix =V7c0FIapermutationV6V5Iainfix =V4V1Aainfix =V3V0Aainfix <=c0V5Aainfix <=c0V3Aasorted_subamk arrayV3V4V6c0V5AapermutationV6V5Aainfix =V3V5FIainfix >V0c0Aainfix <=c0V0Lamk arrayV0V1FF">