[STATEMENT]
theorem skipping_ok:
  assumes j_bounds[simp]: "1 < j" "j \<le> length s"
    and mismatch: "s!(i-1) \<noteq> s!(j-1)"
    and greater_checked: "\<ff> s j \<le> i + 1"
    and "strict_border (take (i-1) s) (take (j-1) s)"
  shows "\<ff> s j \<le> \<ff> s (i-1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<ff> s j \<le> \<ff> s (i - 1) + 1
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<ff> s j \<le> \<ff> s (i - 1) + 1 \<Longrightarrow> False
[PROOF STEP]
assume "\<not>\<ff> s j \<le> \<ff> s (i-1) + 1"
[PROOF STATE]
proof (state)
this:
\<not> \<ff> s j \<le> \<ff> s (i - 1) + 1

goal (1 subgoal):
 1. \<not> \<ff> s j \<le> \<ff> s (i - 1) + 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<ff> s j \<le> \<ff> s (i - 1) + 1
[PROOF STEP]
have i_bounds: "0 < i" "i \<le> length s"
[PROOF STATE]
proof (prove)
using this:
\<not> \<ff> s j \<le> \<ff> s (i - 1) + 1

goal (1 subgoal):
 1. 0 < i &&& i \<le> length s
[PROOF STEP]
using greater_checked assms(5) take_Nil
[PROOF STATE]
proof (prove)
using this:
\<not> \<ff> s j \<le> \<ff> s (i - 1) + 1
\<ff> s j \<le> i + 1
strict_border (take (i - 1) s) (take (j - 1) s)
take ?n [] = []

goal (1 subgoal):
 1. 0 < i &&& i \<le> length s
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
0 < i
i \<le> length s

goal (1 subgoal):
 1. \<not> \<ff> s j \<le> \<ff> s (i - 1) + 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < i
i \<le> length s
[PROOF STEP]
have i_less_j: "i < j"
[PROOF STATE]
proof (prove)
using this:
0 < i
i \<le> length s

goal (1 subgoal):
 1. i < j
[PROOF STEP]
using assms(5) border_length_r_less nz_le_conv_less
[PROOF STATE]
proof (prove)
using this:
0 < i
i \<le> length s
strict_border (take (i - 1) s) (take (j - 1) s)
\<forall>xs. strict_border xs ?ys \<longrightarrow> length xs < length ?ys
\<lbrakk>0 < ?k; ?k \<le> ?m\<rbrakk> \<Longrightarrow> ?k - Suc 0 < ?m

goal (1 subgoal):
 1. i < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < j

goal (1 subgoal):
 1. \<not> \<ff> s j \<le> \<ff> s (i - 1) + 1 \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>\<ff> s j \<le> \<ff> s (i-1) + 1\<close> greater_checked
[PROOF STATE]
proof (chain)
picking this:
\<not> \<ff> s j \<le> \<ff> s (i - 1) + 1
\<ff> s j \<le> i + 1
[PROOF STEP]
consider
    (tested) "\<ff> s j = i + 1" \<comment> \<open>This contradicts @{thm mismatch}\<close> |
    (skipped) "\<ff> s (i-1) + 1 < \<ff> s j" "\<ff> s j \<le> i"
      \<comment> \<open>This contradicts @{thm \<ff>_is_max[of "i-1" s]}\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> \<ff> s j \<le> \<ff> s (i - 1) + 1
\<ff> s j \<le> i + 1

goal (1 subgoal):
 1. \<lbrakk>\<ff> s j = i + 1 \<Longrightarrow> thesis; \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<ff> s j = i + 1 \<Longrightarrow> ?thesis; \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<not> \<ff> s j \<le> \<ff> s (i - 1) + 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<ff> s j = i + 1 \<Longrightarrow> ?thesis; \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<ff> s j = i + 1 \<Longrightarrow> ?thesis; \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<ff> s j = i + 1 \<Longrightarrow> False
 2. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case tested
[PROOF STATE]
proof (state)
this:
\<ff> s j = i + 1

goal (2 subgoals):
 1. \<ff> s j = i + 1 \<Longrightarrow> False
 2. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<ff> s j = i + 1
[PROOF STEP]
have "\<ff> s j - 1 = i"
[PROOF STATE]
proof (prove)
using this:
\<ff> s j = i + 1

goal (1 subgoal):
 1. \<ff> s j - 1 = i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<ff> s j - 1 = i

goal (2 subgoals):
 1. \<ff> s j = i + 1 \<Longrightarrow> False
 2. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<ff> s j - 1 = i

goal (2 subgoals):
 1. \<ff> s j = i + 1 \<Longrightarrow> False
 2. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note border_positions[OF border_take_\<ff>[of s j, unfolded this]]
[PROOF STATE]
proof (state)
this:
\<forall>ia<length (take i s). take j s ! ia = take j s ! (length (take j s) - length (take i s) + ia)

goal (2 subgoals):
 1. \<ff> s j = i + 1 \<Longrightarrow> False
 2. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<ff> s j - 1 = i
\<forall>ia<length (take i s). take j s ! ia = take j s ! (length (take j s) - length (take i s) + ia)
[PROOF STEP]
have "take j s ! (i-1) = s!(j-1)"
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 1 = i
\<forall>ia<length (take i s). take j s ! ia = take j s ! (length (take j s) - length (take i s) + ia)

goal (1 subgoal):
 1. take j s ! (i - 1) = s ! (j - 1)
[PROOF STEP]
using i_bounds i_less_j
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 1 = i
\<forall>ia<length (take i s). take j s ! ia = take j s ! (length (take j s) - length (take i s) + ia)
0 < i
i \<le> length s
i < j

goal (1 subgoal):
 1. take j s ! (i - 1) = s ! (j - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take j s ! (i - 1) = s ! (j - 1)

goal (2 subgoals):
 1. \<ff> s j = i + 1 \<Longrightarrow> False
 2. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>i < j\<close>
[PROOF STATE]
proof (chain)
picking this:
i < j
take j s ! (i - 1) = s ! (j - 1)
[PROOF STEP]
have "s!(i-1) = s!(j-1)"
[PROOF STATE]
proof (prove)
using this:
i < j
take j s ! (i - 1) = s ! (j - 1)

goal (1 subgoal):
 1. s ! (i - 1) = s ! (j - 1)
[PROOF STEP]
by (simp add: less_imp_diff_less)
[PROOF STATE]
proof (state)
this:
s ! (i - 1) = s ! (j - 1)

goal (2 subgoals):
 1. \<ff> s j = i + 1 \<Longrightarrow> False
 2. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with mismatch
[PROOF STATE]
proof (chain)
picking this:
s ! (i - 1) \<noteq> s ! (j - 1)
s ! (i - 1) = s ! (j - 1)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
s ! (i - 1) \<noteq> s ! (j - 1)
s ! (i - 1) = s ! (j - 1)

goal (1 subgoal):
 1. False
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case skipped
[PROOF STATE]
proof (state)
this:
\<ff> s (i - 1) + 1 < \<ff> s j
\<ff> s j \<le> i

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?border = "take (i-1) s"
      \<comment> \<open>This border of @{term \<open>take (j-1) s\<close>} could not be extended to a border of @{term \<open>take j s\<close>} due to the mismatch.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?impossible = "take (\<ff> s j - 2) s"
      \<comment> \<open>A strict border longer than @{term \<open>intrinsic_border ?border\<close>}, a contradiction.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "length (take j s) = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (take j s) = j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (take j s) = j

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<ff> s j - 2 < i - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<ff> s j - 2 < i - 1
[PROOF STEP]
using skipped
[PROOF STATE]
proof (prove)
using this:
\<ff> s (i - 1) + 1 < \<ff> s j
\<ff> s j \<le> i

goal (1 subgoal):
 1. \<ff> s j - 2 < i - 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<ff> s j - 2 < i - 1

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<ff> s j - 2 < i - 1
[PROOF STEP]
have less_s: "\<ff> s j - 2 < length s" "i - 1 < length s"
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 2 < i - 1

goal (1 subgoal):
 1. \<ff> s j - 2 < length s &&& i - 1 < length s
[PROOF STEP]
using \<open>i < j\<close> j_bounds(2)
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 2 < i - 1
i < j
j \<le> length s

goal (1 subgoal):
 1. \<ff> s j - 2 < length s &&& i - 1 < length s
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
\<ff> s j - 2 < length s
i - 1 < length s

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<ff> s j - 2 < length s
i - 1 < length s
[PROOF STEP]
have strict: "length ?impossible < length ?border"
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 2 < length s
i - 1 < length s

goal (1 subgoal):
 1. length (take (\<ff> s j - 2) s) < length (take (i - 1) s)
[PROOF STEP]
using \<open>\<ff> s j - 2 < i - 1\<close>
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 2 < length s
i - 1 < length s
\<ff> s j - 2 < i - 1

goal (1 subgoal):
 1. length (take (\<ff> s j - 2) s) < length (take (i - 1) s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (take (\<ff> s j - 2) s) < length (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (take (\<ff> s j - 2) s) < length (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
length (take (\<ff> s j - 2) s) < length (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "prefix ?impossible (take j s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (take (\<ff> s j - 2) s) (take j s)
[PROOF STEP]
using prefix_length_prefix take_is_prefix
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prefix ?ps ?xs; prefix ?qs ?xs; length ?ps \<le> length ?qs\<rbrakk> \<Longrightarrow> prefix ?ps ?qs
prefix (take ?n ?xs) ?xs

goal (1 subgoal):
 1. prefix (take (\<ff> s j - 2) s) (take j s)
[PROOF STEP]
by (metis (no_types, lifting) \<open>length (take j s) = j\<close> j_bounds(2) diff_le_self j_le_\<ff>_le length_take less_s(1) min_simps(2) order_trans)
[PROOF STATE]
proof (state)
this:
prefix (take (\<ff> s j - 2) s) (take j s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prefix (take (\<ff> s j - 2) s) (take j s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "prefix ?border (take j s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (take (i - 1) s) (take j s)
[PROOF STEP]
by (metis (no_types, lifting) \<open>length (take j s) = j\<close> diff_le_self i_less_j le_trans length_take less_or_eq_imp_le less_s(2) min_simps(2) prefix_length_prefix take_is_prefix)
[PROOF STATE]
proof (state)
this:
prefix (take (i - 1) s) (take j s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prefix (take (\<ff> s j - 2) s) (take j s)
prefix (take (i - 1) s) (take j s)
[PROOF STEP]
have "prefix ?impossible ?border"
[PROOF STATE]
proof (prove)
using this:
prefix (take (\<ff> s j - 2) s) (take j s)
prefix (take (i - 1) s) (take j s)

goal (1 subgoal):
 1. prefix (take (\<ff> s j - 2) s) (take (i - 1) s)
[PROOF STEP]
using strict less_imp_le_nat prefix_length_prefix
[PROOF STATE]
proof (prove)
using this:
prefix (take (\<ff> s j - 2) s) (take j s)
prefix (take (i - 1) s) (take j s)
length (take (\<ff> s j - 2) s) < length (take (i - 1) s)
?m < ?n \<Longrightarrow> ?m \<le> ?n
\<lbrakk>prefix ?ps ?xs; prefix ?qs ?xs; length ?ps \<le> length ?qs\<rbrakk> \<Longrightarrow> prefix ?ps ?qs

goal (1 subgoal):
 1. prefix (take (\<ff> s j - 2) s) (take (i - 1) s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prefix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
prefix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prefix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
prefix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "suffix (take (\<ff> s j - 1) s) (take j s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix (take (\<ff> s j - 1) s) (take j s)
[PROOF STEP]
using border_take_\<ff>
[PROOF STATE]
proof (prove)
using this:
border (take (\<ff> ?s ?i - 1) ?s) (take ?i ?s)

goal (1 subgoal):
 1. suffix (take (\<ff> s j - 1) s) (take j s)
[PROOF STEP]
by (auto simp: border_def)
[PROOF STATE]
proof (state)
this:
suffix (take (\<ff> s j - 1) s) (take j s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note suffix_butlast[OF this]
[PROOF STATE]
proof (state)
this:
suffix (butlast (take (\<ff> s j - 1) s)) (butlast (take j s))

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
suffix (butlast (take (\<ff> s j - 1) s)) (butlast (take j s))
[PROOF STEP]
have "suffix ?impossible (take (j-1) s)"
[PROOF STATE]
proof (prove)
using this:
suffix (butlast (take (\<ff> s j - 1) s)) (butlast (take j s))

goal (1 subgoal):
 1. suffix (take (\<ff> s j - 2) s) (take (j - 1) s)
[PROOF STEP]
by (metis One_nat_def j_bounds(2) butlast_take diff_diff_left \<ff>_le len_greater_imp_nonempty less_or_eq_imp_le less_s(2) one_add_one)
[PROOF STATE]
proof (state)
this:
suffix (take (\<ff> s j - 2) s) (take (j - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
suffix (take (\<ff> s j - 2) s) (take (j - 1) s)
[PROOF STEP]
have "suffix ?impossible (take (j-1) s)" "suffix ?border (take (j-1) s)"
[PROOF STATE]
proof (prove)
using this:
suffix (take (\<ff> s j - 2) s) (take (j - 1) s)

goal (1 subgoal):
 1. suffix (take (\<ff> s j - 2) s) (take (j - 1) s) &&& suffix (take (i - 1) s) (take (j - 1) s)
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
suffix (take (\<ff> s j - 2) s) (take (j - 1) s)
strict_border (take (i - 1) s) (take (j - 1) s)

goal (1 subgoal):
 1. suffix (take (\<ff> s j - 2) s) (take (j - 1) s) &&& suffix (take (i - 1) s) (take (j - 1) s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
suffix (take (\<ff> s j - 2) s) (take (j - 1) s)
suffix (take (i - 1) s) (take (j - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from suffix_length_suffix[OF this strict[THEN less_imp_le]]
[PROOF STATE]
proof (chain)
picking this:
suffix (take (\<ff> s j - 2) s) (take (i - 1) s)
[PROOF STEP]
have "suffix ?impossible ?border"
[PROOF STATE]
proof (prove)
using this:
suffix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. suffix (take (\<ff> s j - 2) s) (take (i - 1) s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
suffix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
suffix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (take (\<ff> s j - 2) s) < length (take (i - 1) s)
prefix (take (\<ff> s j - 2) s) (take (i - 1) s)
suffix (take (\<ff> s j - 2) s) (take (i - 1) s)
[PROOF STEP]
have "strict_border ?impossible ?border"
[PROOF STATE]
proof (prove)
using this:
length (take (\<ff> s j - 2) s) < length (take (i - 1) s)
prefix (take (\<ff> s j - 2) s) (take (i - 1) s)
suffix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. strict_border (take (\<ff> s j - 2) s) (take (i - 1) s)
[PROOF STEP]
unfolding strict_border_def[unfolded border_def]
[PROOF STATE]
proof (prove)
using this:
length (take (\<ff> s j - 2) s) < length (take (i - 1) s)
prefix (take (\<ff> s j - 2) s) (take (i - 1) s)
suffix (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. (prefix (take (\<ff> s j - 2) s) (take (i - 1) s) \<and> suffix (take (\<ff> s j - 2) s) (take (i - 1) s)) \<and> length (take (\<ff> s j - 2) s) < length (take (i - 1) s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
strict_border (take (\<ff> s j - 2) s) (take (i - 1) s)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note \<ff>_is_max[of "i-1" s, OF _ this]
[PROOF STATE]
proof (state)
this:
i - 1 \<le> length s \<Longrightarrow> length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i - 1 \<le> length s \<Longrightarrow> length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)
[PROOF STEP]
have "length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i-1)"
[PROOF STATE]
proof (prove)
using this:
i - 1 \<le> length s \<Longrightarrow> length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)

goal (1 subgoal):
 1. length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)
[PROOF STEP]
using less_imp_le_nat less_s(2)
[PROOF STATE]
proof (prove)
using this:
i - 1 \<le> length s \<Longrightarrow> length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)
?m < ?n \<Longrightarrow> ?m \<le> ?n
i - 1 < length s

goal (1 subgoal):
 1. length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)
[PROOF STEP]
have "\<ff> s j - 1 \<le> \<ff> s (i-1)"
[PROOF STATE]
proof (prove)
using this:
length (take (\<ff> s j - 2) s) + 1 \<le> \<ff> s (i - 1)

goal (1 subgoal):
 1. \<ff> s j - 1 \<le> \<ff> s (i - 1)
[PROOF STEP]
by (simp add: less_s(1))
[PROOF STATE]
proof (state)
this:
\<ff> s j - 1 \<le> \<ff> s (i - 1)

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<ff> s j - 1 \<le> \<ff> s (i - 1)
[PROOF STEP]
have "\<ff> s j \<le> \<ff> s (i-1) + 1"
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 1 \<le> \<ff> s (i - 1)

goal (1 subgoal):
 1. \<ff> s j \<le> \<ff> s (i - 1) + 1
[PROOF STEP]
using le_diff_conv
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 1 \<le> \<ff> s (i - 1)
(?j - ?k \<le> ?i) = (?j \<le> ?i + ?k)

goal (1 subgoal):
 1. \<ff> s j \<le> \<ff> s (i - 1) + 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<ff> s j \<le> \<ff> s (i - 1) + 1

goal (1 subgoal):
 1. \<lbrakk>\<ff> s (i - 1) + 1 < \<ff> s j; \<ff> s j \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with skipped(1)
[PROOF STATE]
proof (chain)
picking this:
\<ff> s (i - 1) + 1 < \<ff> s j
\<ff> s j \<le> \<ff> s (i - 1) + 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<ff> s (i - 1) + 1 < \<ff> s j
\<ff> s j \<le> \<ff> s (i - 1) + 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extend_border:
  assumes "j \<le> length s"
  assumes "s!(i-1) = s!(j-1)"
  assumes "strict_border (take (i-1) s) (take (j-1) s)"
  assumes "\<ff> s j \<le> i + 1"
  shows "\<ff> s j = i + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
strict_border (take (i - 1) s) (take (j - 1) s)
[PROOF STEP]
have pos_in_range: "i - 1 < length s " "length (take (i-1) s) = i - 1"
[PROOF STATE]
proof (prove)
using this:
strict_border (take (i - 1) s) (take (j - 1) s)

goal (1 subgoal):
 1. i - 1 < length s &&& length (take (i - 1) s) = i - 1
[PROOF STEP]
using border_length_r_less min_less_iff_conj
[PROOF STATE]
proof (prove)
using this:
strict_border (take (i - 1) s) (take (j - 1) s)
\<forall>xs. strict_border xs ?ys \<longrightarrow> length xs < length ?ys
(?z < min ?x ?y) = (?z < ?x \<and> ?z < ?y)

goal (1 subgoal):
 1. i - 1 < length s &&& length (take (i - 1) s) = i - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i - 1 < length s
length (take (i - 1) s) = i - 1

goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
with strict_border_step[THEN iffD1, OF assms(3)]
[PROOF STATE]
proof (chain)
picking this:
strict_border (take (i - 1) s @ [take (j - 1) s ! length (take (i - 1) s)]) (take (j - 1) s @ [take (j - 1) s ! length (take (i - 1) s)])
i - 1 < length s
length (take (i - 1) s) = i - 1
[PROOF STEP]
have "strict_border (take (i-1) s @ [s!(i-1)]) (take (j-1) s @ [s!(i-1)])"
[PROOF STATE]
proof (prove)
using this:
strict_border (take (i - 1) s @ [take (j - 1) s ! length (take (i - 1) s)]) (take (j - 1) s @ [take (j - 1) s ! length (take (i - 1) s)])
i - 1 < length s
length (take (i - 1) s) = i - 1

goal (1 subgoal):
 1. strict_border (take (i - 1) s @ [s ! (i - 1)]) (take (j - 1) s @ [s ! (i - 1)])
[PROOF STEP]
by (metis assms(3) border_length_r_less length_take min_less_iff_conj nth_take)
[PROOF STATE]
proof (state)
this:
strict_border (take (i - 1) s @ [s ! (i - 1)]) (take (j - 1) s @ [s ! (i - 1)])

goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
with pos_in_range
[PROOF STATE]
proof (chain)
picking this:
i - 1 < length s
length (take (i - 1) s) = i - 1
strict_border (take (i - 1) s @ [s ! (i - 1)]) (take (j - 1) s @ [s ! (i - 1)])
[PROOF STEP]
have "strict_border (take i s) (take (j-1) s @ [s!(i-1)])"
[PROOF STATE]
proof (prove)
using this:
i - 1 < length s
length (take (i - 1) s) = i - 1
strict_border (take (i - 1) s @ [s ! (i - 1)]) (take (j - 1) s @ [s ! (i - 1)])

goal (1 subgoal):
 1. strict_border (take i s) (take (j - 1) s @ [s ! (i - 1)])
[PROOF STEP]
by (metis Suc_eq_plus1 Suc_pred add.left_neutral border_bot.bot.not_eq_extremum border_order.less_asym neq0_conv take_0 take_Suc_conv_app_nth)
[PROOF STATE]
proof (state)
this:
strict_border (take i s) (take (j - 1) s @ [s ! (i - 1)])

goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
strict_border (take i s) (take (j - 1) s @ [s ! (i - 1)])
[PROOF STEP]
have "strict_border (take i s) (take (j-1) s @ [s!(j-1)])"
[PROOF STATE]
proof (prove)
using this:
strict_border (take i s) (take (j - 1) s @ [s ! (i - 1)])

goal (1 subgoal):
 1. strict_border (take i s) (take (j - 1) s @ [s ! (j - 1)])
[PROOF STEP]
by (simp only: \<open>s!(i-1) = s!(j-1)\<close>)
[PROOF STATE]
proof (state)
this:
strict_border (take i s) (take (j - 1) s @ [s ! (j - 1)])

goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
strict_border (take i s) (take (j - 1) s @ [s ! (j - 1)])
[PROOF STEP]
have "strict_border (take i s) (take j s)"
[PROOF STATE]
proof (prove)
using this:
strict_border (take i s) (take (j - 1) s @ [s ! (j - 1)])

goal (1 subgoal):
 1. strict_border (take i s) (take j s)
[PROOF STEP]
by (metis One_nat_def Suc_pred assms(1,3) diff_le_self less_le_trans neq0_conv nz_le_conv_less strict_border_imp_nonempty take_Suc_conv_app_nth take_eq_Nil)
[PROOF STATE]
proof (state)
this:
strict_border (take i s) (take j s)

goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
with \<ff>_is_max[OF assms(1) this]
[PROOF STATE]
proof (chain)
picking this:
length (take i s) + 1 \<le> \<ff> s j
strict_border (take i s) (take j s)
[PROOF STEP]
have "\<ff> s j \<ge> i + 1"
[PROOF STATE]
proof (prove)
using this:
length (take i s) + 1 \<le> \<ff> s j
strict_border (take i s) (take j s)

goal (1 subgoal):
 1. i + 1 \<le> \<ff> s j
[PROOF STEP]
using Suc_leI
[PROOF STATE]
proof (prove)
using this:
length (take i s) + 1 \<le> \<ff> s j
strict_border (take i s) (take j s)
?m < ?n \<Longrightarrow> Suc ?m \<le> ?n

goal (1 subgoal):
 1. i + 1 \<le> \<ff> s j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
i + 1 \<le> \<ff> s j

goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
with \<open>\<ff> s j \<le> i + 1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<ff> s j \<le> i + 1
i + 1 \<le> \<ff> s j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<ff> s j \<le> i + 1
i + 1 \<le> \<ff> s j

goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
using le_antisym
[PROOF STATE]
proof (prove)
using this:
\<ff> s j \<le> i + 1
i + 1 \<le> \<ff> s j
\<lbrakk>?m \<le> ?n; ?n \<le> ?m\<rbrakk> \<Longrightarrow> ?m = ?n

goal (1 subgoal):
 1. \<ff> s j = i + 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<ff> s j = i + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_\<ff>s_correct: "compute_\<ff>s s \<le> compute_\<ff>s_SPEC s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compute_\<ff>s s \<le> compute_\<ff>s_SPEC s
[PROOF STEP]
unfolding compute_\<ff>s_SPEC_def compute_\<ff>s_def I_out_cb_def I_in_cb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let \<ff>s = replicate (length s + 1) 0; i = 0; j = 1 in WHILE\<^sub>T\<^bsup>\<lambda>(\<ff>s, i, j). length s + 1 = length \<ff>s \<and> (\<forall>jj<j. \<ff>s ! jj = \<ff> s jj) \<and> \<ff>s ! (j - 1) = i \<and> 0 < j\<^esup> (\<lambda>(\<ff>s, uu_, j). j < length \<ff>s) (\<lambda>(\<ff>s, i, j). WHILE\<^sub>T\<^bsup>\<lambda>i. if j = 1 then i = 0 else strict_border (take (i - 1) s) (take (j - 1) s) \<and> \<ff> s j \<le> i + 1\<^esup> (\<lambda>i. 0 < i \<and> s ! (i - 1) \<noteq> s ! (j - 1)) (\<lambda>i. ASSERT (i - 1 < length \<ff>s) \<bind> (\<lambda>_. Let (\<ff>s ! (i - 1)) RETURN)) i \<bind> (\<lambda>i. let i = i + 1 in ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. let \<ff>s = \<ff>s[j := i]; j = j + 1 in RETURN (\<ff>s, i, j)))) (\<ff>s, i, j) \<bind> (\<lambda>(\<ff>s, uu_, uu_). RETURN \<ff>s)) \<le> SPEC (\<lambda>\<ff>s. length \<ff>s = length s + 1 \<and> (\<forall>j\<le>length s. \<ff>s ! j = \<ff> s j))
[PROOF STEP]
apply (simp, refine_vcg
    WHILEIT_rule[where R="measure (\<lambda>(\<ff>s,i,j). length s + 1 - j)"]
    WHILEIT_rule[where R="measure id"] \<comment> \<open>@{term \<open>i::nat\<close>} decreases with every iteration.\<close>
    )
[PROOF STATE]
proof (prove)
goal (22 subgoals):
 1. wf (measure (\<lambda>(\<ff>s, i, j). length s + 1 - j))
 2. \<And>x1 x2 x1a x2a. \<lbrakk>x2 = (x1a, x2a); (0 # replicate (length s) 0, 0, Suc 0) = (x1, x2)\<rbrakk> \<Longrightarrow> Suc (length s) = length x1
 3. \<And>x1 x2 x1a x2a jj. \<lbrakk>x2 = (x1a, x2a); (0 # replicate (length s) 0, 0, Suc 0) = (x1, x2); jj < x2a\<rbrakk> \<Longrightarrow> x1 ! jj = \<ff> s jj
 4. \<And>x1 x2 x1a x2a. \<lbrakk>x2 = (x1a, x2a); (0 # replicate (length s) 0, 0, Suc 0) = (x1, x2)\<rbrakk> \<Longrightarrow> x1 ! (x2a - Suc 0) = x1a
 5. \<And>x1 x2 x1a x2a. \<lbrakk>x2 = (x1a, x2a); (0 # replicate (length s) 0, 0, Suc 0) = (x1, x2)\<rbrakk> \<Longrightarrow> 0 < x2a
 6. \<And>sa a b aa ba. \<lbrakk>case sa of (\<ff>s, ab) \<Rightarrow> Suc (length s) = length \<ff>s \<and> (case ab of (i, j) \<Rightarrow> (\<forall>jj<j. \<ff>s ! jj = \<ff> s jj) \<and> \<ff>s ! (j - Suc 0) = i \<and> 0 < j); case sa of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; sa = (a, b); b = (aa, ba)\<rbrakk> \<Longrightarrow> wf (measure id)
 7. \<And>sa a b aa ba. \<lbrakk>case sa of (\<ff>s, ab) \<Rightarrow> Suc (length s) = length \<ff>s \<and> (case ab of (i, j) \<Rightarrow> (\<forall>jj<j. \<ff>s ! jj = \<ff> s jj) \<and> \<ff>s ! (j - Suc 0) = i \<and> 0 < j); case sa of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; sa = (a, b); b = (aa, ba); ba = Suc 0\<rbrakk> \<Longrightarrow> aa = 0
 8. \<And>sa a b aa ba. \<lbrakk>case sa of (\<ff>s, ab) \<Rightarrow> Suc (length s) = length \<ff>s \<and> (case ab of (i, j) \<Rightarrow> (\<forall>jj<j. \<ff>s ! jj = \<ff> s jj) \<and> \<ff>s ! (j - Suc 0) = i \<and> 0 < j); case sa of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; sa = (a, b); b = (aa, ba); ba \<noteq> Suc 0\<rbrakk> \<Longrightarrow> strict_border (take (aa - Suc 0) s) (take (ba - Suc 0) s)
 9. \<And>sa a b aa ba. \<lbrakk>case sa of (\<ff>s, ab) \<Rightarrow> Suc (length s) = length \<ff>s \<and> (case ab of (i, j) \<Rightarrow> (\<forall>jj<j. \<ff>s ! jj = \<ff> s jj) \<and> \<ff>s ! (j - Suc 0) = i \<and> 0 < j); case sa of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; sa = (a, b); b = (aa, ba); ba \<noteq> Suc 0\<rbrakk> \<Longrightarrow> \<ff> s ba \<le> Suc aa
 10. \<And>sa a b aa ba saa. \<lbrakk>case sa of (\<ff>s, ab) \<Rightarrow> Suc (length s) = length \<ff>s \<and> (case ab of (i, j) \<Rightarrow> (\<forall>jj<j. \<ff>s ! jj = \<ff> s jj) \<and> \<ff>s ! (j - Suc 0) = i \<and> 0 < j); case sa of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; sa = (a, b); b = (aa, ba); (ba = Suc 0 \<longrightarrow> saa = 0) \<and> (ba \<noteq> Suc 0 \<longrightarrow> strict_border (take (saa - Suc 0) s) (take (ba - Suc 0) s) \<and> \<ff> s ba \<le> Suc saa); 0 < saa \<and> s ! (saa - Suc 0) \<noteq> s ! (ba - Suc 0)\<rbrakk> \<Longrightarrow> saa - Suc 0 < length a
A total of 22 subgoals...
[PROOF STEP]
apply (vc_solve, fold One_nat_def)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>ab baa. \<lbrakk>baa < length ab; baa \<noteq> 1; Suc (length s) = length ab; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> strict_border (take (\<ff> s (baa - 1) - 1) s) (take (baa - 1) s)
 2. \<And>ab baa. \<lbrakk>baa < length ab; baa \<noteq> 1; Suc (length s) = length ab; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> \<ff> s baa \<le> Suc (\<ff> s (baa - 1))
 3. \<And>ab baa sa. \<lbrakk>baa < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> sa - 1 < length ab
 4. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> strict_border (take (ab ! (sa - 1) - 1) s) (take (baa - 1) s)
 5. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> \<ff> s baa \<le> Suc (ab ! (sa - 1))
 6. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> ab ! (sa - 1) < sa
 7. \<And>ab baa sa jj. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; jj < Suc baa; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> ab[baa := Suc sa] ! jj = \<ff> s jj
 8. \<And>ab baa sa. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> length ab - Suc baa < length ab - baa
[PROOF STEP]
subgoal for b j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < length b; j \<noteq> 1; Suc (length s) = length b; \<forall>jj<j. b ! jj = \<ff> s jj; 0 < j\<rbrakk> \<Longrightarrow> strict_border (take (\<ff> s (j - 1) - 1) s) (take (j - 1) s)
[PROOF STEP]
by (rule strict_border_take_\<ff>, auto)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>ab baa. \<lbrakk>baa < length ab; baa \<noteq> 1; Suc (length s) = length ab; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> \<ff> s baa \<le> Suc (\<ff> s (baa - 1))
 2. \<And>ab baa sa. \<lbrakk>baa < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> sa - 1 < length ab
 3. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> strict_border (take (ab ! (sa - 1) - 1) s) (take (baa - 1) s)
 4. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> \<ff> s baa \<le> Suc (ab ! (sa - 1))
 5. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> ab ! (sa - 1) < sa
 6. \<And>ab baa sa jj. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; jj < Suc baa; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> ab[baa := Suc sa] ! jj = \<ff> s jj
 7. \<And>ab baa sa. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> length ab - Suc baa < length ab - baa
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>baa_ < length ab_; baa_ \<noteq> 1; Suc (length s) = length ab_; \<forall>jj<baa_. ab_ ! jj = \<ff> s jj; 0 < baa_\<rbrakk> \<Longrightarrow> \<ff> s baa_ \<le> Suc (\<ff> s (baa_ - 1))
[PROOF STEP]
by (metis Suc_eq_plus1 \<ff>_step_bound less_Suc_eq_le)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>ab baa sa. \<lbrakk>baa < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> sa - 1 < length ab
 2. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> strict_border (take (ab ! (sa - 1) - 1) s) (take (baa - 1) s)
 3. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> \<ff> s baa \<le> Suc (ab ! (sa - 1))
 4. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> ab ! (sa - 1) < sa
 5. \<And>ab baa sa jj. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; jj < Suc baa; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> ab[baa := Suc sa] ! jj = \<ff> s jj
 6. \<And>ab baa sa. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> length ab - Suc baa < length ab - baa
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>baa_ < length ab_; Suc (length s) = length ab_; baa_ \<noteq> 1; 0 < sa_; s ! (sa_ - 1) \<noteq> s ! (baa_ - 1); \<forall>jj<baa_. ab_ ! jj = \<ff> s jj; 0 < baa_; strict_border (take (sa_ - 1) s) (take (baa_ - 1) s); \<ff> s baa_ \<le> Suc sa_\<rbrakk> \<Longrightarrow> sa_ - 1 < length ab_
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> strict_border (take (ab ! (sa - 1) - 1) s) (take (baa - 1) s)
 2. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> \<ff> s baa \<le> Suc (ab ! (sa - 1))
 3. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> ab ! (sa - 1) < sa
 4. \<And>ab baa sa jj. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; jj < Suc baa; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> ab[baa := Suc sa] ! jj = \<ff> s jj
 5. \<And>ab baa sa. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> length ab - Suc baa < length ab - baa
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>baa_ < length ab_; sa_ - 1 < length ab_; baa_ \<noteq> 1; Suc (length s) = length ab_; strict_border (take (sa_ - 1) s) (take (baa_ - 1) s); \<ff> s baa_ \<le> Suc sa_; 0 < sa_; s ! (sa_ - 1) \<noteq> s ! (baa_ - 1); \<forall>jj<baa_. ab_ ! jj = \<ff> s jj; 0 < baa_\<rbrakk> \<Longrightarrow> strict_border (take (ab_ ! (sa_ - 1) - 1) s) (take (baa_ - 1) s)
[PROOF STEP]
by (metis (no_types, lifting) One_nat_def Suc_lessD Suc_pred border_length_r_less \<ff>_strict_borderI length_take less_Suc_eq less_Suc_eq_le min.absorb2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; baa \<noteq> 1; Suc (length s) = length ab; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> \<ff> s baa \<le> Suc (ab ! (sa - 1))
 2. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> ab ! (sa - 1) < sa
 3. \<And>ab baa sa jj. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; jj < Suc baa; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> ab[baa := Suc sa] ! jj = \<ff> s jj
 4. \<And>ab baa sa. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> length ab - Suc baa < length ab - baa
[PROOF STEP]
subgoal for b j i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < length b; i - 1 < length b; j \<noteq> 1; Suc (length s) = length b; strict_border (take (i - 1) s) (take (j - 1) s); \<ff> s j \<le> Suc i; 0 < i; s ! (i - 1) \<noteq> s ! (j - 1); \<forall>jj<j. b ! jj = \<ff> s jj; 0 < j\<rbrakk> \<Longrightarrow> \<ff> s j \<le> Suc (b ! (i - 1))
[PROOF STEP]
by (metis (no_types, lifting) One_nat_def Suc_diff_1 Suc_eq_plus1 Suc_leI border_take_lengths less_Suc_eq_le less_antisym skipping_ok strict_border_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ab baa sa. \<lbrakk>baa < length ab; sa - 1 < length ab; Suc (length s) = length ab; baa \<noteq> 1; 0 < sa; s ! (sa - 1) \<noteq> s ! (baa - 1); \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa; strict_border (take (sa - 1) s) (take (baa - 1) s); \<ff> s baa \<le> Suc sa\<rbrakk> \<Longrightarrow> ab ! (sa - 1) < sa
 2. \<And>ab baa sa jj. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; jj < Suc baa; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> ab[baa := Suc sa] ! jj = \<ff> s jj
 3. \<And>ab baa sa. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> length ab - Suc baa < length ab - baa
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>baa_ < length ab_; sa_ - 1 < length ab_; Suc (length s) = length ab_; baa_ \<noteq> 1; 0 < sa_; s ! (sa_ - 1) \<noteq> s ! (baa_ - 1); \<forall>jj<baa_. ab_ ! jj = \<ff> s jj; 0 < baa_; strict_border (take (sa_ - 1) s) (take (baa_ - 1) s); \<ff> s baa_ \<le> Suc sa_\<rbrakk> \<Longrightarrow> ab_ ! (sa_ - 1) < sa_
[PROOF STEP]
by (metis Suc_diff_1 border_take_lengths j_le_\<ff>_le less_Suc_eq_le strict_border_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ab baa sa jj. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; jj < Suc baa; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> ab[baa := Suc sa] ! jj = \<ff> s jj
 2. \<And>ab baa sa. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> length ab - Suc baa < length ab - baa
[PROOF STEP]
subgoal for b j i jj
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = 0 \<or> s ! (i - 1) = s ! (j - 1); j < length b; jj < Suc j; Suc (length s) = length b; j = 1 \<longrightarrow> i = 0; j \<noteq> 1 \<longrightarrow> strict_border (take (i - 1) s) (take (j - 1) s) \<and> \<ff> s j \<le> Suc i; \<forall>jj<j. b ! jj = \<ff> s jj; 0 < j\<rbrakk> \<Longrightarrow> b[j := Suc i] ! jj = \<ff> s jj
[PROOF STEP]
by (metis Suc_eq_plus1 Suc_eq_plus1_left add.right_neutral extend_border \<ff>_eq_0_iff_j_eq_0 j_le_\<ff>_le le_zero_eq less_Suc_eq less_Suc_eq_le nth_list_update_eq nth_list_update_neq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ab baa sa. \<lbrakk>sa = 0 \<or> s ! (sa - 1) = s ! (baa - 1); baa < length ab; Suc (length s) = length ab; baa = 1 \<longrightarrow> sa = 0; baa \<noteq> 1 \<longrightarrow> strict_border (take (sa - 1) s) (take (baa - 1) s) \<and> \<ff> s baa \<le> Suc sa; \<forall>jj<baa. ab ! jj = \<ff> s jj; 0 < baa\<rbrakk> \<Longrightarrow> length ab - Suc baa < length ab - baa
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sa_ = 0 \<or> s ! (sa_ - 1) = s ! (baa_ - 1); baa_ < length ab_; Suc (length s) = length ab_; baa_ = 1 \<longrightarrow> sa_ = 0; baa_ \<noteq> 1 \<longrightarrow> strict_border (take (sa_ - 1) s) (take (baa_ - 1) s) \<and> \<ff> s baa_ \<le> Suc sa_; \<forall>jj<baa_. ab_ ! jj = \<ff> s jj; 0 < baa_\<rbrakk> \<Longrightarrow> length ab_ - Suc baa_ < length ab_ - baa_
[PROOF STEP]
by linarith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compute_\<ff>s_inner_bounds:
  assumes "I_out_cb s (\<ff>s,ix,j)"
  assumes "j < length \<ff>s"
  assumes "I_in_cb s j i"
  shows "i-1 < length s" "j-1 < length s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i - 1 < length s &&& j - 1 < length s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
I_out_cb s (\<ff>s, ix, j)
j < length \<ff>s
I_in_cb s j i

goal (1 subgoal):
 1. i - 1 < length s &&& j - 1 < length s
[PROOF STEP]
by (auto simp: I_out_cb_def I_in_cb_def split: if_splits)


[STATEMENT]
lemma compute_butlast_\<ff>s_refine[refine]:
  assumes "(s,s') \<in> br butlast ((\<noteq>) [])"
  shows "compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s_SPEC s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s_SPEC s')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s_SPEC s')
[PROOF STEP]
have "compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s s')
[PROOF STEP]
unfolding compute_butlast_\<ff>s_def compute_\<ff>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let \<ff>s = replicate (length s) 0; i = 0; j = 1 in WHILE\<^sub>T\<^bsup>I_out_cb (butlast s)\<^esup> (\<lambda>(b, i, j). j < length b) (\<lambda>(\<ff>s, i, j). ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_cb (butlast s) j\<^esup> (\<lambda>i. 0 < i \<and> s ! (i - 1) \<noteq> s ! (j - 1)) (\<lambda>i. ASSERT (i - 1 < length \<ff>s) \<bind> (\<lambda>_. Let (\<ff>s ! (i - 1)) RETURN)) i \<bind> (\<lambda>i. let i = i + 1 in ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. let \<ff>s = \<ff>s[j := i]; j = j + 1 in RETURN (\<ff>s, i, j))))) (\<ff>s, i, j) \<bind> (\<lambda>(\<ff>s, uu_, uu_). RETURN \<ff>s)) \<le> \<Down> Id (let \<ff>s = replicate (length s' + 1) 0; i = 0; j = 1 in WHILE\<^sub>T\<^bsup>I_out_cb s'\<^esup> (\<lambda>(\<ff>s, uu_, j). j < length \<ff>s) (\<lambda>(\<ff>s, i, j). WHILE\<^sub>T\<^bsup>I_in_cb s' j\<^esup> (\<lambda>i. 0 < i \<and> s' ! (i - 1) \<noteq> s' ! (j - 1)) (\<lambda>i. ASSERT (i - 1 < length \<ff>s) \<bind> (\<lambda>_. Let (\<ff>s ! (i - 1)) RETURN)) i \<bind> (\<lambda>i. let i = i + 1 in ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. let \<ff>s = \<ff>s[j := i]; j = j + 1 in RETURN (\<ff>s, i, j)))) (\<ff>s, i, j) \<bind> (\<lambda>(\<ff>s, uu_, uu_). RETURN \<ff>s))
[PROOF STEP]
apply (refine_rcg)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. I_out_cb s' (replicate (length s' + 1) 0, 0, 1) \<Longrightarrow> ((replicate (length s) 0, 0, 1), replicate (length s' + 1) 0, 0, 1) \<in> ?R'3
 2. \<And>x x'. \<lbrakk>(x, x') \<in> ?R'3; I_out_cb s' x'\<rbrakk> \<Longrightarrow> I_out_cb (butlast s) x
 3. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> ?R'3; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x = (x1, x2); x2b = (x1c, x2c); x' = (x1b, x2b)\<rbrakk> \<Longrightarrow> (x2a < length x1) = (x2c < length x1b)
 4. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> ?R'3; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b)\<rbrakk> \<Longrightarrow> x2c < length x1b
 5. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> ?R'3; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; I_in_cb s' x2a x1a\<rbrakk> \<Longrightarrow> (x1c, x1a) \<in> ?R'110 x x' x1 x2 x1a x2a x1b x2b x1c x2c
 6. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> ?R'3; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> ?R'110 x x' x1 x2 x1a x2a x1b x2b x1c x2c; I_in_cb s' x2a x'a\<rbrakk> \<Longrightarrow> I_in_cb (butlast s) x2c xa
 7. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> ?R'3; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> ?R'110 x x' x1 x2 x1a x2a x1b x2b x1c x2c; I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a\<rbrakk> \<Longrightarrow> (0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1)) = (0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1))
 8. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> ?R'3; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> ?R'110 x x' x1 x2 x1a x2a x1b x2b x1c x2c; 0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1); 0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1); I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a; x'a - 1 < length x1\<rbrakk> \<Longrightarrow> xa - 1 < length x1b
 9. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> ?R'3; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> ?R'110 x x' x1 x2 x1a x2a x1b x2b x1c x2c; 0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1); 0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1); I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a; x'a - 1 < length x1; xa - 1 < length x1b\<rbrakk> \<Longrightarrow> (x1b ! (xa - 1), x1 ! (x'a - 1)) \<in> ?R'110 x x' x1 x2 x1a x2a x1b x2b x1c x2c
 10. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c i ia. \<lbrakk>(x, x') \<in> ?R'3; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (i, ia) \<in> ?R'110 x x' x1 x2 x1a x2a x1b x2b x1c x2c; x2a < length x1; x2c < length x1b\<rbrakk> \<Longrightarrow> ((x1b[x2c := i + 1], i + 1, x2c + 1), x1[x2a := ia + 1], ia + 1, x2a + 1) \<in> ?R'3
A total of 11 subgoals...
[PROOF STEP]
apply (refine_dref_type)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. I_out_cb s' (replicate (length s' + 1) 0, 0, 1) \<Longrightarrow> ((replicate (length s) 0, 0, 1), replicate (length s' + 1) 0, 0, 1) \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel
 2. \<And>x x'. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; I_out_cb s' x'\<rbrakk> \<Longrightarrow> I_out_cb (butlast s) x
 3. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x = (x1, x2); x2b = (x1c, x2c); x' = (x1b, x2b)\<rbrakk> \<Longrightarrow> (x2a < length x1) = (x2c < length x1b)
 4. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b)\<rbrakk> \<Longrightarrow> x2c < length x1b
 5. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; I_in_cb s' x2a x1a\<rbrakk> \<Longrightarrow> (x1c, x1a) \<in> nat_rel
 6. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> nat_rel; I_in_cb s' x2a x'a\<rbrakk> \<Longrightarrow> I_in_cb (butlast s) x2c xa
 7. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> nat_rel; I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a\<rbrakk> \<Longrightarrow> (0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1)) = (0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1))
 8. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> nat_rel; 0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1); 0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1); I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a; x'a - 1 < length x1\<rbrakk> \<Longrightarrow> xa - 1 < length x1b
 9. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> nat_rel; 0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1); 0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1); I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a; x'a - 1 < length x1; xa - 1 < length x1b\<rbrakk> \<Longrightarrow> (x1b ! (xa - 1), x1 ! (x'a - 1)) \<in> nat_rel
 10. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c i ia. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (i, ia) \<in> nat_rel; x2a < length x1; x2c < length x1b\<rbrakk> \<Longrightarrow> ((x1b[x2c := i + 1], i + 1, x2c + 1), x1[x2a := ia + 1], ia + 1, x2a + 1) \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel
A total of 11 subgoals...
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(s, s') \<in> br butlast ((\<noteq>) [])

goal (11 subgoals):
 1. I_out_cb s' (replicate (length s' + 1) 0, 0, 1) \<Longrightarrow> ((replicate (length s) 0, 0, 1), replicate (length s' + 1) 0, 0, 1) \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel
 2. \<And>x x'. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; I_out_cb s' x'\<rbrakk> \<Longrightarrow> I_out_cb (butlast s) x
 3. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x = (x1, x2); x2b = (x1c, x2c); x' = (x1b, x2b)\<rbrakk> \<Longrightarrow> (x2a < length x1) = (x2c < length x1b)
 4. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b)\<rbrakk> \<Longrightarrow> x2c < length x1b
 5. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; I_in_cb s' x2a x1a\<rbrakk> \<Longrightarrow> (x1c, x1a) \<in> nat_rel
 6. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> nat_rel; I_in_cb s' x2a x'a\<rbrakk> \<Longrightarrow> I_in_cb (butlast s) x2c xa
 7. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> nat_rel; I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a\<rbrakk> \<Longrightarrow> (0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1)) = (0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1))
 8. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> nat_rel; 0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1); 0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1); I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a; x'a - 1 < length x1\<rbrakk> \<Longrightarrow> xa - 1 < length x1b
 9. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (xa, x'a) \<in> nat_rel; 0 < xa \<and> s ! (xa - 1) \<noteq> s ! (x2c - 1); 0 < x'a \<and> s' ! (x'a - 1) \<noteq> s' ! (x2a - 1); I_in_cb (butlast s) x2c xa; I_in_cb s' x2a x'a; x'a - 1 < length x1; xa - 1 < length x1b\<rbrakk> \<Longrightarrow> (x1b ! (xa - 1), x1 ! (x'a - 1)) \<in> nat_rel
 10. \<And>x x' x1 x2 x1a x2a x1b x2b x1c x2c i ia. \<lbrakk>(x, x') \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel; case x of (b, i, j) \<Rightarrow> j < length b; case x' of (\<ff>s, uu_, j) \<Rightarrow> j < length \<ff>s; I_out_cb (butlast s) x; I_out_cb s' x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x2c < length x1b; (i, ia) \<in> nat_rel; x2a < length x1; x2c < length x1b\<rbrakk> \<Longrightarrow> ((x1b[x2c := i + 1], i + 1, x2c + 1), x1[x2a := ia + 1], ia + 1, x2a + 1) \<in> \<langle>nat_rel\<rangle>list_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r nat_rel
A total of 11 subgoals...
[PROOF STEP]
apply (vc_solve simp: in_br_conv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>I_out_cb (butlast s) (0 # replicate (length s - Suc 0) 0, 0, Suc 0); s' = butlast s; [] \<noteq> s\<rbrakk> \<Longrightarrow> replicate (length s) 0 = 0 # replicate (length s - Suc 0) 0
 2. \<And>x1 x1a x2a x'a. \<lbrakk>x2a < length x1; I_out_cb (butlast s) (x1, x1a, x2a); I_in_cb (butlast s) x2a x'a; s' = butlast s; [] \<noteq> s\<rbrakk> \<Longrightarrow> (0 < x'a \<and> s ! (x'a - Suc 0) \<noteq> s ! (x2a - Suc 0)) = (0 < x'a \<and> butlast s ! (x'a - Suc 0) \<noteq> butlast s ! (x2a - Suc 0))
[PROOF STEP]
apply (metis Suc_pred length_greater_0_conv replicate_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x1a x2a x'a. \<lbrakk>x2a < length x1; I_out_cb (butlast s) (x1, x1a, x2a); I_in_cb (butlast s) x2a x'a; s' = butlast s; [] \<noteq> s\<rbrakk> \<Longrightarrow> (0 < x'a \<and> s ! (x'a - Suc 0) \<noteq> s ! (x2a - Suc 0)) = (0 < x'a \<and> butlast s ! (x'a - Suc 0) \<noteq> butlast s ! (x2a - Suc 0))
[PROOF STEP]
by (metis One_nat_def compute_\<ff>s_inner_bounds nth_butlast)
[PROOF STATE]
proof (state)
this:
compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s s')

goal (1 subgoal):
 1. compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s_SPEC s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s s')

goal (1 subgoal):
 1. compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s_SPEC s')
[PROOF STEP]
note compute_\<ff>s_correct
[PROOF STATE]
proof (state)
this:
compute_\<ff>s ?s \<le> compute_\<ff>s_SPEC ?s

goal (1 subgoal):
 1. compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s_SPEC s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
compute_butlast_\<ff>s s \<le> compute_\<ff>s_SPEC s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
compute_butlast_\<ff>s s \<le> compute_\<ff>s_SPEC s'

goal (1 subgoal):
 1. compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s_SPEC s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
compute_butlast_\<ff>s s \<le> \<Down> Id (compute_\<ff>s_SPEC s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kmp2_refine: "kmp2 s t \<le> kmp1 s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp2 s t \<le> kmp1 s t
[PROOF STEP]
apply (rule refine_IdD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp2 s t \<le> \<Down> Id (kmp1 s t)
[PROOF STEP]
unfolding kmp2_def kmp1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (s \<noteq> []) \<bind> (\<lambda>_. let i = 0; j = 0; pos = None in compute_butlast_\<ff>s s \<bind> (\<lambda>\<ff>s. WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t \<and> pos = None) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). let j = j + 1 in if j = length s then RETURN (j, Some i) else RETURN (j, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. let i = i + (j - \<ff>s ! j + 1); j = max 0 (\<ff>s ! j - 1) in RETURN (i, j, None)) else RETURN (i, j, Some i)))) (i, j, pos) \<bind> (\<lambda>(uu_, uu_, pos). RETURN pos))) \<le> \<Down> Id (ASSERT (s \<noteq> []) \<bind> (\<lambda>_. let i = 0; j = 0; pos = None in compute_\<ff>s_SPEC (butlast s) \<bind> (\<lambda>\<ff>s. WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). let j = j + 1 in if j = length s then RETURN (j, Some i) else RETURN (j, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. let i = i + (j - \<ff>s ! j + 1); j = max 0 (\<ff>s ! j - 1) in RETURN (i, j, None)) else RETURN (i, j, Some i)))) (i, j, pos) \<bind> (\<lambda>(uu_, uu_, pos). RETURN pos))))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<lbrakk>s \<noteq> []; s \<noteq> []\<rbrakk> \<Longrightarrow> (s, butlast s) \<in> br butlast ((\<noteq>) [])
 2. \<And>\<ff>s \<ff>sa. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; I_outer s t (0, 0, None)\<rbrakk> \<Longrightarrow> ((0, 0, None), 0, 0, None) \<in> ?R'9 \<ff>s \<ff>sa
 3. \<And>\<ff>s \<ff>sa x x'. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> ?R'9 \<ff>s \<ff>sa; I_outer s t x'\<rbrakk> \<Longrightarrow> I_outer s t x
 4. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> ?R'9 \<ff>s \<ff>sa; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x = (x1, x2); x2b = (x1c, x2c); x' = (x1b, x2b)\<rbrakk> \<Longrightarrow> (x1 + length s \<le> length t \<and> x2a = None) = (x1b + length s \<le> length t \<and> x2c = None)
 5. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> ?R'9 \<ff>s \<ff>sa; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t\<rbrakk> \<Longrightarrow> x1b + length s \<le> length t
 6. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> ?R'9 \<ff>s \<ff>sa; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t\<rbrakk> \<Longrightarrow> x2c = None
 7. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> ?R'9 \<ff>s \<ff>sa; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t \<and> x2c = None; I_in_na s t x1 (x1a, x2a)\<rbrakk> \<Longrightarrow> ((x1c, x2c), x1a, x2a) \<in> ?R'118 \<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c
 8. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> ?R'9 \<ff>s \<ff>sa; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t \<and> x2c = None; (xa, x'a) \<in> ?R'118 \<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c; I_in_na s t x1 x'a\<rbrakk> \<Longrightarrow> I_in_na s t x1b xa
 9. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> ?R'9 \<ff>s \<ff>sa; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t \<and> x2c = None; (xa, x'a) \<in> ?R'118 \<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c; I_in_na s t x1b xa; I_in_na s t x1 x'a; xa = (x1d, x2d); x'a = (x1e, x2e)\<rbrakk> \<Longrightarrow> (t ! (x1b + x1d) = s ! x1d \<and> x2d = None) = (t ! (x1 + x1e) = s ! x1e \<and> x2e = None)
 10. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> ?R'9 \<ff>s \<ff>sa; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t \<and> x2c = None; (xa, x'a) \<in> ?R'118 \<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c; case xa of (j, pos) \<Rightarrow> t ! (x1b + j) = s ! j \<and> pos = None; case x'a of (j, pos) \<Rightarrow> t ! (x1 + j) = s ! j \<and> pos = None; I_in_na s t x1b xa; I_in_na s t x1 x'a; x'a = (x1d, x2d); xa = (x1e, x2e)\<rbrakk> \<Longrightarrow> (x1e + 1 = length s) = (x1d + 1 = length s)
A total of 17 subgoals...
[PROOF STEP]
apply refine_dref_type
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<lbrakk>s \<noteq> []; s \<noteq> []\<rbrakk> \<Longrightarrow> (s, butlast s) \<in> br butlast ((\<noteq>) [])
 2. \<And>\<ff>s \<ff>sa. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; I_outer s t (0, 0, None)\<rbrakk> \<Longrightarrow> ((0, 0, None), 0, 0, None) \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel
 3. \<And>\<ff>s \<ff>sa x x'. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; I_outer s t x'\<rbrakk> \<Longrightarrow> I_outer s t x
 4. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x = (x1, x2); x2b = (x1c, x2c); x' = (x1b, x2b)\<rbrakk> \<Longrightarrow> (x1 + length s \<le> length t \<and> x2a = None) = (x1b + length s \<le> length t \<and> x2c = None)
 5. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t\<rbrakk> \<Longrightarrow> x1b + length s \<le> length t
 6. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t\<rbrakk> \<Longrightarrow> x2c = None
 7. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t \<and> x2c = None; I_in_na s t x1 (x1a, x2a)\<rbrakk> \<Longrightarrow> ((x1c, x2c), x1a, x2a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel
 8. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t \<and> x2c = None; (xa, x'a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; I_in_na s t x1 x'a\<rbrakk> \<Longrightarrow> I_in_na s t x1b xa
 9. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t \<and> x2c = None; (xa, x'a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; I_in_na s t x1b xa; I_in_na s t x1 x'a; xa = (x1d, x2d); x'a = (x1e, x2e)\<rbrakk> \<Longrightarrow> (t ! (x1b + x1d) = s ! x1d \<and> x2d = None) = (t ! (x1 + x1e) = s ! x1e \<and> x2e = None)
 10. \<And>\<ff>s \<ff>sa x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; (\<ff>s, \<ff>sa) \<in> Id; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t \<and> x2c = None; (xa, x'a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case xa of (j, pos) \<Rightarrow> t ! (x1b + j) = s ! j \<and> pos = None; case x'a of (j, pos) \<Rightarrow> t ! (x1 + j) = s ! j \<and> pos = None; I_in_na s t x1b xa; I_in_na s t x1 x'a; x'a = (x1d, x2d); xa = (x1e, x2e)\<rbrakk> \<Longrightarrow> (x1e + 1 = length s) = (x1d + 1 = length s)
A total of 17 subgoals...
[PROOF STEP]
apply (vc_solve simp: in_br_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma kmp2_correct: "s \<noteq> []
  \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
assume "s \<noteq> []"
[PROOF STATE]
proof (state)
this:
s \<noteq> []

goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
have "kmp2 s t \<le> kmp1 s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp2 s t \<le> kmp1 s t
[PROOF STEP]
by (fact kmp2_refine)
[PROOF STATE]
proof (state)
this:
kmp2 s t \<le> kmp1 s t

goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
kmp2 s t \<le> kmp1 s t

goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
have "... \<le> kmp s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp1 s t \<le> kmp s t
[PROOF STEP]
by (fact kmp1_refine)
[PROOF STATE]
proof (state)
this:
kmp1 s t \<le> kmp s t

goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
kmp1 s t \<le> kmp s t

goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
have "... \<le> kmp_SPEC s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp s t \<le> kmp_SPEC s t
[PROOF STEP]
by (fact kmp_correct[OF \<open>s \<noteq> []\<close>])
[PROOF STATE]
proof (state)
this:
kmp s t \<le> kmp_SPEC s t

goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
kmp2 s t \<le> kmp_SPEC s t

goal (1 subgoal):
 1. kmp2 s t \<le> kmp_SPEC s t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
kmp2 s t \<le> kmp_SPEC s t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kmp3_correct: "kmp3 s t \<le> kmp_SPEC s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp3 s t \<le> kmp_SPEC s t
[PROOF STEP]
unfolding kmp3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if s = [] then RETURN (Some 0) else kmp2 s t) \<le> kmp_SPEC s t
[PROOF STEP]
by (simp add: kmp2_correct) (simp add: kmp_SPEC_def)


[STATEMENT]
lemma eq_id_param: "((=), (=)) \<in> Id \<rightarrow> Id \<rightarrow> Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=), (=)) \<in> Id \<rightarrow> Id \<rightarrow> bool_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma kmp_inner_in_bound:
  assumes "i + length s \<le> length t"
  assumes "I_in_na s t i (j,None)"
  shows "i + j < length t" "j < length s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + j < length t &&& j < length s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i + length s \<le> length t
I_in_na s t i (j, None)

goal (1 subgoal):
 1. i + j < length t &&& j < length s
[PROOF STEP]
by (auto simp: I_in_na_def)


[STATEMENT]
lemma kmp3_correct':
  "(uncurry kmp3, uncurry kmp_SPEC) \<in> Id \<times>\<^sub>r Id \<rightarrow>\<^sub>f \<langle>Id\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uncurry kmp3, uncurry kmp_SPEC) \<in> Id \<times>\<^sub>r Id \<rightarrow>\<^sub>f \<langle>Id\<rangle>nres_rel
[PROOF STEP]
apply (intro frefI nres_relI; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. kmp3 a b \<le> kmp_SPEC a b
[PROOF STEP]
apply (fact kmp3_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem kmp_impl_correct:
  "< arl_assn id_assn s si * arl_assn id_assn t ti >
       kmp_impl si ti
   <\<lambda>r. arl_assn id_assn s si * arl_assn id_assn t ti * \<up>(
      case r of None \<Rightarrow>  \<nexists>i. sublist_at s t i
              | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
    )>\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <arl_assn id_assn s si * arl_assn id_assn t ti> kmp_impl si ti <\<lambda>r. arl_assn id_assn s si * arl_assn id_assn t ti * \<up> (case r of None \<Rightarrow> \<nexists>i. sublist_at s t i | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii))>\<^sub>t
[PROOF STEP]
by (sep_auto
    simp: pure_def kmp_SPEC_def
    split: option.split
    heap:  kmp_impl_correct'[THEN hfrefD, THEN hn_refineD, of "(s,t)" "(si,ti)", simplified])


[STATEMENT]
lemma translation_length_nonneg [simp, mono_intros]:
  "translation_length f \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> translation_length f
[PROOF STEP]
unfolding translation_length_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Inf {dist x (f x) |x. True}
[PROOF STEP]
by (rule cInf_greatest, auto)


[STATEMENT]
lemma translation_length_le [mono_intros]:
  "translation_length f \<le> dist x (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. translation_length f \<le> dist x (f x)
[PROOF STEP]
unfolding translation_length_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {dist x (f x) |x. True} \<le> dist x (f x)
[PROOF STEP]
apply (rule cInf_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist x (f x) \<in> {dist x (f x) |x. True}
 2. bdd_below {dist x (f x) |x. True}
[PROOF STEP]
by (auto intro: bdd_belowI[of _ 0])


[STATEMENT]
lemma stable_translation_length_nonneg [simp]:
  "stable_translation_length f \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> stable_translation_length f
[PROOF STEP]
unfolding stable_translation_length_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Inf {translation_length (f ^^ n) / real n |n. 0 < n}
[PROOF STEP]
by (rule cInf_greatest, auto)


[STATEMENT]
lemma stable_translation_length_le_translation_length [mono_intros]:
  "n * stable_translation_length f \<le> translation_length (f^^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n * stable_translation_length f \<le> translation_length (f ^^ n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real n * stable_translation_length f \<le> translation_length (f ^^ n)
[PROOF STEP]
have *: "stable_translation_length f \<le> translation_length (f^^n)/n" if "n > 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_translation_length f \<le> translation_length (f ^^ n) / real n
[PROOF STEP]
unfolding stable_translation_length_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {translation_length (f ^^ n) / real n |n. 0 < n} \<le> translation_length (f ^^ n) / real n
[PROOF STEP]
apply (rule cInf_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. translation_length (f ^^ n) / real n \<in> {translation_length (f ^^ n) / real n |n. 0 < n}
 2. bdd_below {translation_length (f ^^ n) / real n |n. 0 < n}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (2 subgoals):
 1. translation_length (f ^^ n) / real n \<in> {translation_length (f ^^ n) / real n |n. 0 < n}
 2. bdd_below {translation_length (f ^^ n) / real n |n. 0 < n}
[PROOF STEP]
by (auto intro: bdd_belowI[of _ 0])
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> stable_translation_length f \<le> translation_length (f ^^ ?n) / real ?n

goal (1 subgoal):
 1. real n * stable_translation_length f \<le> translation_length (f ^^ n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n * stable_translation_length f \<le> translation_length (f ^^ n)
[PROOF STEP]
apply (cases "n = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> real n * stable_translation_length f \<le> translation_length (f ^^ n)
 2. n \<noteq> 0 \<Longrightarrow> real n * stable_translation_length f \<le> translation_length (f ^^ n)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> stable_translation_length f \<le> translation_length (f ^^ ?n) / real ?n

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> real n * stable_translation_length f \<le> translation_length (f ^^ n)
 2. n \<noteq> 0 \<Longrightarrow> real n * stable_translation_length f \<le> translation_length (f ^^ n)
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
real n * stable_translation_length f \<le> translation_length (f ^^ n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma semicontraction_iterates:
  fixes f::"('a::metric_space) \<Rightarrow> 'a"
  assumes "1-lipschitz_on UNIV f"
  shows "1-lipschitz_on UNIV (f^^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1-lipschitz_on UNIV (f ^^ n)
[PROOF STEP]
by (induction n, auto intro!: lipschitz_onI lipschitz_on_compose2[of 1 UNIV _ 1 f, simplified] lipschitz_on_subset[OF assms])


[STATEMENT]
lemma stable_translation_length_inv:
  assumes "isometry f"
  shows "stable_translation_length (inv f) = stable_translation_length f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_translation_length (inv f) = stable_translation_length f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stable_translation_length (inv f) = stable_translation_length f
[PROOF STEP]
have *: "dist basepoint (((inv f)^^n) basepoint) = dist basepoint ((f^^n) basepoint)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) basepoint) = dist basepoint ((f ^^ n) basepoint)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) basepoint) = dist basepoint ((f ^^ n) basepoint)
[PROOF STEP]
have "basepoint = (f^^n) (((inv f)^^n) basepoint)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basepoint = (f ^^ n) ((inv f ^^ n) basepoint)
[PROOF STEP]
by (metis assms comp_apply fn_o_inv_fn_is_id isometry_inverse(2))
[PROOF STATE]
proof (state)
this:
basepoint = (f ^^ n) ((inv f ^^ n) basepoint)

goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) basepoint) = dist basepoint ((f ^^ n) basepoint)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basepoint = (f ^^ n) ((inv f ^^ n) basepoint)
[PROOF STEP]
have "dist basepoint ((f^^n) basepoint) = dist ((f^^n) (((inv f)^^n) basepoint)) ((f^^n) basepoint)"
[PROOF STATE]
proof (prove)
using this:
basepoint = (f ^^ n) ((inv f ^^ n) basepoint)

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) = dist ((f ^^ n) ((inv f ^^ n) basepoint)) ((f ^^ n) basepoint)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist basepoint ((f ^^ n) basepoint) = dist ((f ^^ n) ((inv f ^^ n) basepoint)) ((f ^^ n) basepoint)

goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) basepoint) = dist basepoint ((f ^^ n) basepoint)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist basepoint ((f ^^ n) basepoint) = dist ((f ^^ n) ((inv f ^^ n) basepoint)) ((f ^^ n) basepoint)

goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) basepoint) = dist basepoint ((f ^^ n) basepoint)
[PROOF STEP]
have "... = dist (((inv f)^^n) basepoint) basepoint"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((f ^^ n) ((inv f ^^ n) basepoint)) ((f ^^ n) basepoint) = dist ((inv f ^^ n) basepoint) basepoint
[PROOF STEP]
unfolding isometryD(2)[OF isometry_iterates[OF assms]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((inv f ^^ n) basepoint) basepoint = dist ((inv f ^^ n) basepoint) basepoint
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist ((f ^^ n) ((inv f ^^ n) basepoint)) ((f ^^ n) basepoint) = dist ((inv f ^^ n) basepoint) basepoint

goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) basepoint) = dist basepoint ((f ^^ n) basepoint)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist basepoint ((f ^^ n) basepoint) = dist ((inv f ^^ n) basepoint) basepoint
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist basepoint ((f ^^ n) basepoint) = dist ((inv f ^^ n) basepoint) basepoint

goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) basepoint) = dist basepoint ((f ^^ n) basepoint)
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist basepoint ((inv f ^^ n) basepoint) = dist basepoint ((f ^^ n) basepoint)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist basepoint ((inv f ^^ ?n) basepoint) = dist basepoint ((f ^^ ?n) basepoint)

goal (1 subgoal):
 1. stable_translation_length (inv f) = stable_translation_length f
[PROOF STEP]
have "(\<lambda>n. dist basepoint ((f^^n) basepoint)/n) \<longlonglongrightarrow> stable_translation_length f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length f
[PROOF STEP]
using stable_translation_length_as_pointwise_limit[OF isometryD(4)[OF assms]]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist ?x ((f ^^ n) ?x) / real n) \<longlonglongrightarrow> stable_translation_length f

goal (1 subgoal):
 1. (\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length f

goal (1 subgoal):
 1. stable_translation_length (inv f) = stable_translation_length f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length f

goal (1 subgoal):
 1. stable_translation_length (inv f) = stable_translation_length f
[PROOF STEP]
have "(\<lambda>n. dist basepoint ((f^^n) basepoint)/n) \<longlonglongrightarrow> stable_translation_length (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length (inv f)
[PROOF STEP]
unfolding *[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist basepoint ((inv f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length (inv f)
[PROOF STEP]
using stable_translation_length_as_pointwise_limit[OF isometryD(4)[OF isometry_inverse(1)[OF assms]]]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist ?x ((inv f ^^ n) ?x) / real n) \<longlonglongrightarrow> stable_translation_length (inv f)

goal (1 subgoal):
 1. (\<lambda>n. dist basepoint ((inv f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length (inv f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length (inv f)

goal (1 subgoal):
 1. stable_translation_length (inv f) = stable_translation_length f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length f
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length (inv f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length f
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length (inv f)

goal (1 subgoal):
 1. stable_translation_length (inv f) = stable_translation_length f
[PROOF STEP]
using LIMSEQ_unique
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length f
(\<lambda>n. dist basepoint ((f ^^ n) basepoint) / real n) \<longlonglongrightarrow> stable_translation_length (inv f)
\<lbrakk>?X \<longlonglongrightarrow> ?a; ?X \<longlonglongrightarrow> ?b\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. stable_translation_length (inv f) = stable_translation_length f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stable_translation_length (inv f) = stable_translation_length f

goal:
No subgoals!
[PROOF STEP]
qed