(* Title: HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Author: Stefan Berghofer Copyright: secunet Security Networks AG *) theory Longest_Increasing_Subsequence imports SPARK begin text ‹ Set of all increasing subsequences in a prefix of an array › definition iseq :: "(nat ⇒ 'a::linorder) ⇒ nat ⇒ nat set set" where "iseq xs l = {is. (∀i∈is. i < l) ∧ (∀i∈is. ∀j∈is. i ≤ j ⟶ xs i ≤ xs j)}" text ‹ Length of longest increasing subsequence in a prefix of an array › definition liseq :: "(nat ⇒ 'a::linorder) ⇒ nat ⇒ nat" where "liseq xs i = Max (card ` iseq xs i)" text ‹ Length of longest increasing subsequence ending at a particular position › definition liseq' :: "(nat ⇒ 'a::linorder) ⇒ nat ⇒ nat" where "liseq' xs i = Max (card ` (iseq xs (Suc i) ∩ {is. Max is = i}))" lemma iseq_finite: "finite (iseq xs i)" apply (simp add: iseq_def) apply (rule finite_subset [OF _ finite_Collect_subsets [of "{j. j < i}"]]) apply auto done lemma iseq_finite': "is ∈ iseq xs i ⟹ finite is" by (auto simp add: iseq_def bounded_nat_set_is_finite) lemma iseq_singleton: "i < l ⟹ {i} ∈ iseq xs l" by (simp add: iseq_def) lemma iseq_trivial: "{} ∈ iseq xs i" by (simp add: iseq_def) lemma iseq_nonempty: "iseq xs i ≠ {}" by (auto intro: iseq_trivial) lemma liseq'_ge1: "1 ≤ liseq' xs x" apply (simp add: liseq'_def) apply (subgoal_tac "iseq xs (Suc x) ∩ {is. Max is = x} ≠ {}") apply (simp add: Max_ge_iff iseq_finite) apply (rule_tac x="{x}" in bexI) apply (auto intro: iseq_singleton) done lemma liseq_expand: assumes R: "⋀is. liseq xs i = card is ⟹ is ∈ iseq xs i ⟹ (⋀js. js ∈ iseq xs i ⟹ card js ≤ card is) ⟹ P" shows "P" proof - have "Max (card ` iseq xs i) ∈ card ` iseq xs i" by (rule Max_in) (simp_all add: iseq_finite iseq_nonempty) then obtain js where js: "liseq xs i = card js" and "js ∈ iseq xs i" by (rule imageE) (simp add: liseq_def) moreover { fix js' assume "js' ∈ iseq xs i" then have "card js' ≤ card js" by (simp add: js [symmetric] liseq_def iseq_finite iseq_trivial) } ultimately show ?thesis by (rule R) qed lemma liseq'_expand: assumes R: "⋀is. liseq' xs i = card is ⟹ is ∈ iseq xs (Suc i) ⟹ finite is ⟹ Max is = i ⟹ (⋀js. js ∈ iseq xs (Suc i) ⟹ Max js = i ⟹ card js ≤ card is) ⟹ is ≠ {} ⟹ P" shows "P" proof - have "Max (card ` (iseq xs (Suc i) ∩ {is. Max is = i})) ∈ card ` (iseq xs (Suc i) ∩ {is. Max is = i})" by (auto simp add: iseq_finite intro!: iseq_singleton Max_in) then obtain js where js: "liseq' xs i = card js" and "js ∈ iseq xs (Suc i)" and "finite js" and "Max js = i" by (auto simp add: liseq'_def intro: iseq_finite') moreover { fix js' assume "js' ∈ iseq xs (Suc i)" "Max js' = i" then have "card js' ≤ card js" by (auto simp add: js [symmetric] liseq'_def iseq_finite intro!: iseq_singleton) } note max = this moreover have "card {i} ≤ card js" by (rule max) (simp_all add: iseq_singleton) then have "js ≠ {}" by auto ultimately show ?thesis by (rule R) qed lemma liseq'_ge: "j = card js ⟹ js ∈ iseq xs (Suc i) ⟹ Max js = i ⟹ js ≠ {} ⟹ j ≤ liseq' xs i" by (simp add: liseq'_def iseq_finite) lemma liseq'_eq: "j = card js ⟹ js ∈ iseq xs (Suc i) ⟹ Max js = i ⟹ js ≠ {} ⟹ (⋀js'. js' ∈ iseq xs (Suc i) ⟹ Max js' = i ⟹ finite js' ⟹ js' ≠ {} ⟹ card js' ≤ card js) ⟹ j = liseq' xs i" by (fastforce simp add: liseq'_def iseq_finite intro: Max_eqI [symmetric]) lemma liseq_ge: "j = card js ⟹ js ∈ iseq xs i ⟹ j ≤ liseq xs i" by (auto simp add: liseq_def iseq_finite) lemma liseq_eq: "j = card js ⟹ js ∈ iseq xs i ⟹ (⋀js'. js' ∈ iseq xs i ⟹ finite js' ⟹ js' ≠ {} ⟹ card js' ≤ card js) ⟹ j = liseq xs i" by (fastforce simp add: liseq_def iseq_finite intro: Max_eqI [symmetric]) lemma max_notin: "finite xs ⟹ Max xs < x ⟹ x ∉ xs" by (cases "xs = {}") auto lemma iseq_insert: "xs (Max is) ≤ xs i ⟹ is ∈ iseq xs i ⟹ is ∪ {i} ∈ iseq xs (Suc i)" apply (frule iseq_finite') apply (cases "is = {}") apply (auto simp add: iseq_def) apply (rule order_trans [of _ "xs (Max is)"]) apply auto apply (thin_tac "∀a∈is. a < i") apply (drule_tac x=ia in bspec) apply assumption apply (drule_tac x="Max is" in bspec) apply (auto intro: Max_in) done lemma iseq_diff: "is ∈ iseq xs (Suc (Max is)) ⟹ is - {Max is} ∈ iseq xs (Suc (Max (is - {Max is})))" apply (frule iseq_finite') apply (simp add: iseq_def less_Suc_eq_le) done lemma iseq_butlast: assumes "js ∈ iseq xs (Suc i)" and "js ≠ {}" and "Max js ≠ i" shows "js ∈ iseq xs i" proof - from assms have fin: "finite js" by (simp add: iseq_finite') with assms have "Max js ∈ js" by auto with assms have "Max js < i" by (auto simp add: iseq_def) with fin assms have "∀j∈js. j < i" by simp with assms show ?thesis by (simp add: iseq_def) qed lemma iseq_mono: "is ∈ iseq xs i ⟹ i ≤ j ⟹ is ∈ iseq xs j" by (auto simp add: iseq_def) lemma diff_nonempty: assumes "1 < card is" shows "is - {i} ≠ {}" proof - from assms have fin: "finite is" by (auto intro: card_ge_0_finite) with assms fin have "card is - 1 ≤ card (is - {i})" by (simp add: card_Diff_singleton_if) with assms have "0 < card (is - {i})" by simp then show ?thesis by (simp add: card_gt_0_iff) qed lemma Max_diff: assumes "1 < card is" shows "Max (is - {Max is}) < Max is" proof - from assms have "finite is" by (auto intro: card_ge_0_finite) moreover from assms have "is - {Max is} ≠ {}" by (rule diff_nonempty) ultimately show ?thesis using assms apply (auto simp add: not_less) apply (subgoal_tac "a ≤ Max is") apply auto done qed lemma iseq_nth: "js ∈ iseq xs l ⟹ 1 < card js ⟹ xs (Max (js - {Max js})) ≤ xs (Max js)" apply (auto simp add: iseq_def) apply (subgoal_tac "Max (js - {Max js}) ∈ js") apply (thin_tac "∀i∈js. i < l") apply (drule_tac x="Max (js - {Max js})" in bspec) apply assumption apply (drule_tac x="Max js" in bspec) using card_gt_0_iff [of js] apply simp using Max_diff [of js] apply simp using Max_in [of "js - {Max js}", OF _ diff_nonempty] card_gt_0_iff [of js] apply auto done lemma card_leq1_singleton: assumes "finite xs" "xs ≠ {}" "card xs ≤ 1" obtains x where "xs = {x}" using assms by induct simp_all lemma longest_iseq1: "liseq' xs i = Max ({0} ∪ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}) + 1" proof - have "Max ({0} ∪ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}) = liseq' xs i - 1" proof (rule Max_eqI) fix y assume "y ∈ {0} ∪ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}" then show "y ≤ liseq' xs i - 1" proof assume "y ∈ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}" then obtain j where j: "j < i" "xs j ≤ xs i" "y = liseq' xs j" by auto have "liseq' xs j + 1 ≤ liseq' xs i" proof (rule liseq'_expand) fix "is" assume H: "liseq' xs j = card is" "is ∈ iseq xs (Suc j)" "finite is" "Max is = j" "is ≠ {}" from H j have "card is + 1 = card (is ∪ {i})" by (simp add: card_insert max_notin) moreover { from H j have "xs (Max is) ≤ xs i" by simp moreover from ‹j < i› have "Suc j ≤ i" by simp with ‹is ∈ iseq xs (Suc j)› have "is ∈ iseq xs i" by (rule iseq_mono) ultimately have "is ∪ {i} ∈ iseq xs (Suc i)" by (rule iseq_insert) } moreover from H j have "Max (is ∪ {i}) = i" by simp moreover have "is ∪ {i} ≠ {}" by simp ultimately have "card is + 1 ≤ liseq' xs i" by (rule liseq'_ge) with H show ?thesis by simp qed with j show "y ≤ liseq' xs i - 1" by simp qed simp next have "liseq' xs i ≤ 1 ∨ (∃j. liseq' xs i - 1 = liseq' xs j ∧ j < i ∧ xs j ≤ xs i)" proof (rule liseq'_expand) fix "is" assume H: "liseq' xs i = card is" "is ∈ iseq xs (Suc i)" "finite is" "Max is = i" "is ≠ {}" assume R: "⋀js. js ∈ iseq xs (Suc i) ⟹ Max js = i ⟹ card js ≤ card is" show ?thesis proof (cases "card is ≤ 1") case True with H show ?thesis by simp next case False then have "1 < card is" by simp then have "Max (is - {Max is}) < Max is" by (rule Max_diff) from ‹is ∈ iseq xs (Suc i)› ‹1 < card is› have "xs (Max (is - {Max is})) ≤ xs (Max is)" by (rule iseq_nth) have "card is - 1 = liseq' xs (Max (is - {i}))" proof (rule liseq'_eq) from ‹Max is = i› [symmetric] ‹finite is› ‹is ≠ {}› show "card is - 1 = card (is - {i})" by simp next from ‹is ∈ iseq xs (Suc i)› ‹Max is = i› [symmetric] show "is - {i} ∈ iseq xs (Suc (Max (is - {i})))" by simp (rule iseq_diff) next from ‹1 < card is› show "is - {i} ≠ {}" by (rule diff_nonempty) next fix js assume "js ∈ iseq xs (Suc (Max (is - {i})))" "Max js = Max (is - {i})" "finite js" "js ≠ {}" from ‹xs (Max (is - {Max is})) ≤ xs (Max is)› ‹Max js = Max (is - {i})› ‹Max is = i› have "xs (Max js) ≤ xs i" by simp moreover from ‹Max is = i› ‹Max (is - {Max is}) < Max is› have "Suc (Max (is - {i})) ≤ i" by simp with ‹js ∈ iseq xs (Suc (Max (is - {i})))› have "js ∈ iseq xs i" by (rule iseq_mono) ultimately have "js ∪ {i} ∈ iseq xs (Suc i)" by (rule iseq_insert) moreover from ‹js ≠ {}› ‹finite js› ‹Max js = Max (is - {i})› ‹Max is = i› [symmetric] ‹Max (is - {Max is}) < Max is› have "Max (js ∪ {i}) = i" by simp ultimately have "card (js ∪ {i}) ≤ card is" by (rule R) moreover from ‹Max is = i› [symmetric] ‹finite js› ‹Max (is - {Max is}) < Max is› ‹Max js = Max (is - {i})› have "i ∉ js" by (simp add: max_notin) with ‹finite js› have "card (js ∪ {i}) = card ((js ∪ {i}) - {i}) + 1" by simp ultimately show "card js ≤ card (is - {i})" using ‹i ∉ js› ‹Max is = i› [symmetric] ‹is ≠ {}› ‹finite is› by simp qed simp with H ‹Max (is - {Max is}) < Max is› ‹xs (Max (is - {Max is})) ≤ xs (Max is)› show ?thesis by auto qed qed then show "liseq' xs i - 1 ∈ {0} ∪ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}" by simp qed simp moreover have "1 ≤ liseq' xs i" by (rule liseq'_ge1) ultimately show ?thesis by simp qed lemma longest_iseq2': "liseq xs i < liseq' xs i ⟹ liseq xs (Suc i) = liseq' xs i" apply (rule_tac xs=xs and i=i in liseq'_expand) apply simp apply (rule liseq_eq [symmetric]) apply (rule refl) apply assumption apply (case_tac "Max js' = i") apply simp apply (drule_tac js=js' in iseq_butlast) apply assumption+ apply (drule_tac js=js' in liseq_ge [OF refl]) apply simp done lemma longest_iseq2: "liseq xs i < liseq' xs i ⟹ liseq xs i + 1 = liseq' xs i" apply (rule_tac xs=xs and i=i in liseq'_expand) apply simp apply (rule_tac xs=xs and i=i in liseq_expand) apply (drule_tac s="Max is" in sym) apply simp apply (case_tac "card is ≤ 1") apply simp apply (drule iseq_diff) apply (drule_tac i="Suc (Max (is - {Max is}))" and j="Max is" in iseq_mono) apply (simp add: less_eq_Suc_le [symmetric]) apply (rule Max_diff) apply simp apply (drule_tac x="is - {Max is}" in meta_spec, drule meta_mp, assumption) apply simp done lemma longest_iseq3: "liseq xs j = liseq' xs i ⟹ xs i ≤ xs j ⟹ i < j ⟹ liseq xs (Suc j) = liseq xs j + 1" apply (rule_tac xs=xs and i=j in liseq_expand) apply simp apply (rule_tac xs=xs and i=i in liseq'_expand) apply simp apply (rule_tac js="isa ∪ {j}" in liseq_eq [symmetric]) apply (simp add: card_insert card_Diff_singleton_if max_notin) apply (rule iseq_insert) apply simp apply (erule iseq_mono) apply simp apply (case_tac "j = Max js'") apply simp apply (drule iseq_diff) apply (drule_tac x="js' - {j}" in meta_spec) apply (drule meta_mp) apply simp apply (case_tac "card js' ≤ 1") apply (erule_tac xs=js' in card_leq1_singleton) apply assumption+ apply (simp add: iseq_trivial) apply (erule iseq_mono) apply (simp add: less_eq_Suc_le [symmetric]) apply (rule Max_diff) apply simp apply (rule le_diff_iff [THEN iffD1, of 1]) apply (simp add: card_0_eq [symmetric] del: card_0_eq) apply (simp add: card_insert) apply (subgoal_tac "card (js' - {j}) = card js' - 1") apply (simp add: card_insert card_Diff_singleton_if max_notin) apply (frule_tac A=js' in Max_in) apply assumption apply (simp add: card_Diff_singleton_if) apply (drule_tac js=js' in iseq_butlast) apply assumption apply (erule not_sym) apply (drule_tac x=js' in meta_spec) apply (drule meta_mp) apply assumption apply (simp add: card_insert_disjoint max_notin) done lemma longest_iseq4: "liseq xs j = liseq' xs i ⟹ xs i ≤ xs j ⟹ i < j ⟹ liseq' xs j = liseq' xs i + 1" apply (rule_tac xs=xs and i=j in liseq_expand) apply simp apply (rule_tac xs=xs and i=i in liseq'_expand) apply simp apply (rule_tac js="isa ∪ {j}" in liseq'_eq [symmetric]) apply (simp add: card_insert card_Diff_singleton_if max_notin) apply (rule iseq_insert) apply simp apply (erule iseq_mono) apply simp apply simp apply simp apply (drule_tac s="Max js'" in sym) apply simp apply (drule iseq_diff) apply (drule_tac x="js' - {j}" in meta_spec) apply (drule meta_mp) apply simp apply (case_tac "card js' ≤ 1") apply (erule_tac xs=js' in card_leq1_singleton) apply assumption+ apply (simp add: iseq_trivial) apply (erule iseq_mono) apply (simp add: less_eq_Suc_le [symmetric]) apply (rule Max_diff) apply simp apply (rule le_diff_iff [THEN iffD1, of 1]) apply (simp add: card_0_eq [symmetric] del: card_0_eq) apply (simp add: card_insert) apply (subgoal_tac "card (js' - {j}) = card js' - 1") apply (simp add: card_insert card_Diff_singleton_if max_notin) apply (frule_tac A=js' in Max_in) apply assumption apply (simp add: card_Diff_singleton_if) done lemma longest_iseq5: "liseq' xs i ≤ liseq xs i ⟹ liseq xs (Suc i) = liseq xs i" apply (rule_tac i=i and xs=xs in liseq'_expand) apply simp apply (rule_tac xs=xs and i=i in liseq_expand) apply simp apply (rule liseq_eq [symmetric]) apply (rule refl) apply (erule iseq_mono) apply simp apply (case_tac "Max js' = i") apply (drule_tac x=js' in meta_spec) apply simp apply (drule iseq_butlast, assumption, assumption) apply simp done lemma liseq_empty: "liseq xs 0 = 0" apply (rule_tac js="{}" in liseq_eq [symmetric]) apply simp apply (rule iseq_trivial) apply (simp add: iseq_def) done lemma liseq'_singleton: "liseq' xs 0 = 1" by (simp add: longest_iseq1 [of _ 0]) lemma liseq_singleton: "liseq xs (Suc 0) = Suc 0" by (simp add: longest_iseq2' liseq_empty liseq'_singleton) lemma liseq'_Suc_unfold: "A j ≤ x ⟹ (insert 0 {liseq' A j' |j'. j' < Suc j ∧ A j' ≤ x}) = (insert 0 {liseq' A j' |j'. j' < j ∧ A j' ≤ x}) ∪ {liseq' A j}" by (auto simp add: less_Suc_eq) lemma liseq'_Suc_unfold': "¬ (A j ≤ x) ⟹ {liseq' A j' |j'. j' < Suc j ∧ A j' ≤ x} = {liseq' A j' |j'. j' < j ∧ A j' ≤ x}" by (auto simp add: less_Suc_eq) lemma iseq_card_limit: assumes "is ∈ iseq A i" shows "card is ≤ i" proof - from assms have "is ⊆ {0..<i}" by (auto simp add: iseq_def) with finite_atLeastLessThan have "card is ≤ card {0..<i}" by (rule card_mono) with card_atLeastLessThan show ?thesis by simp qed lemma liseq_limit: "liseq A i ≤ i" by (rule_tac xs=A and i=i in liseq_expand) (simp add: iseq_card_limit) lemma liseq'_limit: "liseq' A i ≤ i + 1" by (rule_tac xs=A and i=i in liseq'_expand) (simp add: iseq_card_limit) definition max_ext :: "(nat ⇒ 'a::linorder) ⇒ nat ⇒ nat ⇒ nat" where "max_ext A i j = Max ({0} ∪ {liseq' A j' |j'. j' < j ∧ A j' ≤ A i})" lemma max_ext_limit: "max_ext A i j ≤ j" apply (auto simp add: max_ext_def) apply (drule Suc_leI) apply (cut_tac i=j' and A=A in liseq'_limit) apply simp done text ‹Proof functions› abbreviation (input) "arr_conv a ≡ (λn. a (int n))" lemma idx_conv_suc: "0 ≤ i ⟹ nat (i + 1) = nat i + 1" by simp abbreviation liseq_ends_at' :: "(int ⇒ 'a::linorder) ⇒ int ⇒ int" where "liseq_ends_at' A i ≡ int (liseq' (λl. A (int l)) (nat i))" abbreviation liseq_prfx' :: "(int ⇒ 'a::linorder) ⇒ int ⇒ int" where "liseq_prfx' A i ≡ int (liseq (λl. A (int l)) (nat i))" abbreviation max_ext' :: "(int ⇒ 'a::linorder) ⇒ int ⇒ int ⇒ int" where "max_ext' A i j ≡ int (max_ext (λl. A (int l)) (nat i) (nat j))" spark_proof_functions liseq_ends_at = "liseq_ends_at' :: (int ⇒ int) ⇒ int ⇒ int" liseq_prfx = "liseq_prfx' :: (int ⇒ int) ⇒ int ⇒ int" max_ext = "max_ext' :: (int ⇒ int) ⇒ int ⇒ int ⇒ int" text ‹The verification conditions› spark_open "liseq/liseq_length" spark_vc procedure_liseq_length_5 by (simp_all add: liseq_singleton liseq'_singleton) spark_vc procedure_liseq_length_6 proof - from H1 H2 H3 H4 have eq: "liseq (arr_conv a) (nat i) = liseq' (arr_conv a) (nat pmax)" by simp from H14 H3 H4 have pmax1: "arr_conv a (nat pmax) ≤ arr_conv a (nat i)" by simp from H3 H4 have pmax2: "nat pmax < nat i" by simp { fix i2 assume i2: "0 ≤ i2" "i2 ≤ i" have "(l(i := l pmax + 1)) i2 = int (liseq' (arr_conv a) (nat i2))" proof (cases "i2 = i") case True from eq pmax1 pmax2 have "liseq' (arr_conv a) (nat i) = liseq' (arr_conv a) (nat pmax) + 1" by (rule longest_iseq4) with True H1 H3 H4 show ?thesis by simp next case False with H1 i2 show ?thesis by simp qed } then show ?C1 by simp from eq pmax1 pmax2 have "liseq (arr_conv a) (Suc (nat i)) = liseq (arr_conv a) (nat i) + 1" by (rule longest_iseq3) with H2 H3 H4 show ?C2 by (simp add: idx_conv_suc) qed spark_vc procedure_liseq_length_7 proof - from H1 show ?C1 by (simp add: max_ext_def longest_iseq1 [of _ "nat i"]) from H6 have m: "max_ext (arr_conv a) (nat i) (nat i) + 1 = liseq' (arr_conv a) (nat i)" by (simp add: max_ext_def longest_iseq1 [of _ "nat i"]) with H2 H18 have gt: "liseq (arr_conv a) (nat i) < liseq' (arr_conv a) (nat i)" by simp then have "liseq' (arr_conv a) (nat i) = liseq (arr_conv a) (nat i) + 1" by (rule longest_iseq2 [symmetric]) with H2 m show ?C2 by simp from gt have "liseq (arr_conv a) (Suc (nat i)) = liseq' (arr_conv a) (nat i)" by (rule longest_iseq2') with m H6 show ?C3 by (simp add: idx_conv_suc) qed spark_vc procedure_liseq_length_8 proof - { fix i2 assume i2: "0 ≤ i2" "i2 ≤ i" have "(l(i := max_ext' a i i + 1)) i2 = int (liseq' (arr_conv a) (nat i2))" proof (cases "i2 = i") case True with H1 show ?thesis by (simp add: max_ext_def longest_iseq1 [of _ "nat i"]) next case False with H1 i2 show ?thesis by simp qed } then show ?C1 by simp from H2 H6 H18 have "liseq' (arr_conv a) (nat i) ≤ liseq (arr_conv a) (nat i)" by (simp add: max_ext_def longest_iseq1 [of _ "nat i"]) then have "liseq (arr_conv a) (Suc (nat i)) = liseq (arr_conv a) (nat i)" by (rule longest_iseq5) with H2 H6 show ?C2 by (simp add: idx_conv_suc) qed spark_vc procedure_liseq_length_12 by (simp add: max_ext_def) spark_vc procedure_liseq_length_13 using H1 H6 H13 H21 H22 by (simp add: max_ext_def idx_conv_suc liseq'_Suc_unfold max_def del: Max_less_iff) spark_vc procedure_liseq_length_14 using H1 H6 H13 H21 by (cases "a j ≤ a i") (simp_all add: max_ext_def idx_conv_suc liseq'_Suc_unfold liseq'_Suc_unfold') spark_vc procedure_liseq_length_19 using H3 H4 H5 H8 H9 apply (rule_tac y="int (nat i)" in order_trans) apply (cut_tac A="arr_conv a" and i="nat i" and j="nat i" in max_ext_limit) apply simp_all done spark_vc procedure_liseq_length_23 using H2 H3 H4 H7 H8 H11 apply (rule_tac y="int (nat i)" in order_trans) apply (cut_tac A="arr_conv a" and i="nat i" in liseq_limit) apply simp_all done spark_vc procedure_liseq_length_29 using H2 H3 H8 H13 by (simp add: add1_zle_eq [symmetric]) spark_end end