# Theory Traces

```section ‹Trace Theory›

theory Traces
imports "Basics/Word_Prefixes"
begin

locale traces =
fixes ind :: "'item ⇒ 'item ⇒ bool"
assumes independence_symmetric[sym]: "ind a b ⟹ ind b a"
begin

abbreviation Ind :: "'item set ⇒ 'item set ⇒ bool"
where "Ind A B ≡ ∀ a ∈ A. ∀ b ∈ B. ind a b"

inductive eq_swap :: "'item list ⇒ 'item list ⇒ bool" (infix "=⇩S" 50)
where swap: "ind a b ⟹ u @ [a] @ [b] @ v =⇩S u @ [b] @ [a] @ v"

declare eq_swap.intros[intro]
declare eq_swap.cases[elim]

lemma eq_swap_sym[sym]: "v =⇩S w ⟹ w =⇩S v" using independence_symmetric by auto

lemma eq_swap_length[dest]: "w⇩1 =⇩S w⇩2 ⟹ length w⇩1 = length w⇩2" by force
lemma eq_swap_range[dest]: "w⇩1 =⇩S w⇩2 ⟹ set w⇩1 = set w⇩2" by force

lemma eq_swap_extend:
assumes "w⇩1 =⇩S w⇩2"
shows "u @ w⇩1 @ v =⇩S u @ w⇩2 @ v"
using assms
proof induct
case (swap a b u' v')
have "u @ (u' @ [a] @ [b] @ v') @ v = (u @ u') @ [a] @ [b] @ (v' @ v)" by simp
also have "… =⇩S (u @ u') @ [b] @ [a] @ (v' @ v)" using swap by blast
also have "… = u @ (u' @ [b] @ [a] @ v') @ v" by simp
finally show ?case by this
qed

lemma eq_swap_remove1:
assumes "w⇩1 =⇩S w⇩2"
obtains (equal) "remove1 c w⇩1 = remove1 c w⇩2" | (swap) "remove1 c w⇩1 =⇩S remove1 c w⇩2"
using assms
proof induct
case (swap a b u v)
have "c ∉ set (u @ [a] @ [b] @ v) ∨
c ∈ set u ∨
c ∉ set u ∧ c = a ∨
c ∉ set u ∧ c ≠ a ∧ c = b ∨
c ∉ set u ∧ c ≠ a ∧ c ≠ b ∧ c ∈ set v"
by auto
thus ?case
proof (elim disjE)
assume 0: "c ∉ set (u @ [a] @ [b] @ v)"
have 1: "c ∉ set (u @ [b] @ [a] @ v)" using 0 by auto
have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ [b] @ v" using remove1_idem 0 by this
have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ [a] @ v" using remove1_idem 1 by this
have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩S remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 using eq_swap.intros swap(1) by this
show thesis using swap(3) 4 by this
next
assume 0: "c ∈ set u"
have 2: "remove1 c (u @ [a] @ [b] @ v) = remove1 c u @ [a] @ [b] @ v"
unfolding remove1_append using 0 by simp
have 3: "remove1 c (u @ [b] @ [a] @ v) = remove1 c u @ [b] @ [a] @ v"
unfolding remove1_append using 0 by simp
have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩S remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 using eq_swap.intros swap(1) by this
show thesis using swap(3) 4 by this
next
assume 0: "c ∉ set u ∧ c = a"
have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [b] @ v"
unfolding remove1_append using remove1_idem 0 by auto
have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ v"
unfolding remove1_append using remove1_idem 0 by auto
have 4: "remove1 c (u @ [a] @ [b] @ v) = remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 by rule
show thesis using swap(2) 4 by this
next
assume 0: "c ∉ set u ∧ c ≠ a ∧ c = b"
have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ v"
unfolding remove1_append using remove1_idem 0 by auto
have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [a] @ v"
unfolding remove1_append using remove1_idem 0 by auto
have 4: "remove1 c (u @ [a] @ [b] @ v) = remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 by rule
show thesis using swap(2) 4 by this
next
assume 0: "c ∉ set u ∧ c ≠ a ∧ c ≠ b ∧ c ∈ set v"
have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ [b] @ remove1 c v"
unfolding remove1_append using 0 by simp
have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ [a] @ remove1 c v"
unfolding remove1_append using 0 by simp
have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩S remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 using eq_swap.intros swap(1) by this
show ?thesis using swap(3) 4 by this
qed
qed

lemma eq_swap_rev:
assumes "w⇩1 =⇩S w⇩2"
shows "rev w⇩1 =⇩S rev w⇩2"
using assms
proof induct
case (swap a b u v)
have 1: "rev v @ [a] @ [b] @ rev u =⇩S rev v @ [b] @ [a] @ rev u" using swap by blast
have 2: "rev v @ [b] @ [a] @ rev u =⇩S rev v @ [a] @ [b] @ rev u" using 1 eq_swap_sym by blast
show ?case using 2 by simp
qed

abbreviation eq_fin :: "'item list ⇒ 'item list ⇒ bool" (infix "=⇩F" 50)
where "eq_fin ≡ eq_swap⇧*⇧*"

lemma eq_fin_symp[intro, sym]: "u =⇩F v ⟹ v =⇩F u"
using eq_swap_sym sym_rtrancl[to_pred] unfolding symp_def by metis

lemma eq_fin_length[dest]: "w⇩1 =⇩F w⇩2 ⟹ length w⇩1 = length w⇩2"
by (induct rule: rtranclp.induct, auto)
lemma eq_fin_range[dest]: "w⇩1 =⇩F w⇩2 ⟹ set w⇩1 = set w⇩2"
by (induct rule: rtranclp.induct, auto)

lemma eq_fin_remove1:
assumes "w⇩1 =⇩F w⇩2"
shows "remove1 c w⇩1 =⇩F remove1 c w⇩2"
using assms
proof induct
case (base)
show ?case by simp
next
case (step w⇩2 w⇩3)
show ?case
using step(2)
proof (cases rule: eq_swap_remove1[where ?c = c])
case equal
show ?thesis using step equal by simp
next
case swap
show ?thesis using step swap by auto
qed
qed

lemma eq_fin_rev:
assumes "w⇩1 =⇩F w⇩2"
shows "rev w⇩1 =⇩F rev w⇩2"
using assms by (induct, auto dest: eq_swap_rev)

lemma eq_fin_concat_eq_fin_start:
assumes "u @ v⇩1 =⇩F u @ v⇩2"
shows "v⇩1 =⇩F v⇩2"
using assms
proof (induct u arbitrary: v⇩1 v⇩2 rule: rev_induct)
case (Nil)
show ?case using Nil by simp
next
case (snoc a u)
have 1: "u @ [a] @ v⇩1 =⇩F u @ [a] @ v⇩2" using snoc(2) by simp
have 2: "[a] @ v⇩1 =⇩F [a] @ v⇩2" using snoc(1) 1 by this
show ?case using eq_fin_remove1[OF 2, of a] by simp
qed

lemma eq_fin_concat: "u @ w⇩1 @ v =⇩F u @ w⇩2 @ v ⟷ w⇩1 =⇩F w⇩2"
proof
assume 0: "u @ w⇩1 @ v =⇩F u @ w⇩2 @ v"
have 1: "w⇩1 @ v =⇩F w⇩2 @ v" using eq_fin_concat_eq_fin_start 0 by this
have 2: "rev (w⇩1 @ v) =⇩F rev (w⇩2 @ v)" using 1 by (blast dest: eq_fin_rev)
have 3: "rev v @ rev w⇩1 =⇩F rev v @ rev w⇩2" using 2 by simp
have 4: "rev w⇩1 =⇩F rev w⇩2" using eq_fin_concat_eq_fin_start 3 by this
have 5: "rev (rev w⇩1) =⇩F rev (rev w⇩2)" using 4 by (blast dest: eq_fin_rev)
show "w⇩1 =⇩F w⇩2" using 5 by simp
next
show "u @ w⇩1 @ v =⇩F u @ w⇩2 @ v" if "w⇩1 =⇩F w⇩2"
using that by (induct, auto dest: eq_swap_extend[of _ _ u v])
qed
lemma eq_fin_concat_start[iff]: "w @ w⇩1 =⇩F w @ w⇩2 ⟷ w⇩1 =⇩F w⇩2"
using eq_fin_concat[of "w" _ "[]"] by simp
lemma eq_fin_concat_end[iff]: "w⇩1 @ w =⇩F w⇩2 @ w ⟷ w⇩1 =⇩F w⇩2"
using eq_fin_concat[of "[]" _ "w"] by simp

lemma ind_eq_fin':
assumes "Ind {a} (set v)"
shows "[a] @ v =⇩F v @ [a]"
using assms
proof (induct v)
case (Nil)
show ?case by simp
next
case (Cons b v)
have 1: "Ind {a} (set v)" using Cons(2) by auto
have 2: "ind a b" using Cons(2) by auto
have "[a] @ b # v = [a] @ [b] @ v" by simp
also have "… =⇩S [b] @ [a] @ v" using eq_swap.intros[OF 2, of "[]"] by auto
also have "… =⇩F [b] @ v @ [a]" using Cons(1) 1 by blast
also have "… = (b # v) @ [a]" by simp
finally show ?case by this
qed

lemma ind_eq_fin[intro]:
assumes "Ind (set u) (set v)"
shows "u @ v =⇩F v @ u"
using assms
proof (induct u)
case (Nil)
show ?case by simp
next
case (Cons a u)
have 1: "Ind (set u) (set v)" using Cons(2) by auto
have 2: "Ind {a} (set v)" using Cons(2) by auto
have "(a # u) @ v = [a] @ u @ v" by simp
also have "… =⇩F [a] @ v @ u" using Cons(1) 1 by blast
also have "… = ([a] @ v) @ u" by simp
also have "… =⇩F (v @ [a]) @ u" using ind_eq_fin' 2 by blast
also have "… = v @ (a # u)" by simp
finally show ?case by this
qed

definition le_fin :: "'item list ⇒ 'item list ⇒ bool" (infix "≼⇩F" 50)
where "w⇩1 ≼⇩F w⇩2 ≡ ∃ v⇩1. w⇩1 @ v⇩1 =⇩F w⇩2"

lemma le_finI[intro 0]:
assumes "w⇩1 @ v⇩1 =⇩F w⇩2"
shows "w⇩1 ≼⇩F w⇩2"
using assms unfolding le_fin_def by auto
lemma le_finE[elim 0]:
assumes "w⇩1 ≼⇩F w⇩2"
obtains v⇩1
where "w⇩1 @ v⇩1 =⇩F w⇩2"
using assms unfolding le_fin_def by auto

lemma le_fin_empty[simp]: "[] ≼⇩F w" by force
lemma le_fin_trivial[intro]: "w⇩1 =⇩F w⇩2 ⟹ w⇩1 ≼⇩F w⇩2"
proof
assume 1: "w⇩1 =⇩F w⇩2"
show "w⇩1 @ [] =⇩F w⇩2" using 1 by simp
qed

lemma le_fin_length[dest]: "w⇩1 ≼⇩F w⇩2 ⟹ length w⇩1 ≤ length w⇩2" by force
lemma le_fin_range[dest]: "w⇩1 ≼⇩F w⇩2 ⟹ set w⇩1 ⊆ set w⇩2" by force

lemma eq_fin_alt_def: "w⇩1 =⇩F w⇩2 ⟷ w⇩1 ≼⇩F w⇩2 ∧ w⇩2 ≼⇩F w⇩1"
proof
show "w⇩1 ≼⇩F w⇩2 ∧ w⇩2 ≼⇩F w⇩1" if "w⇩1 =⇩F w⇩2" using that by blast
next
assume 0: "w⇩1 ≼⇩F w⇩2 ∧ w⇩2 ≼⇩F w⇩1"
have 1: "w⇩1 ≼⇩F w⇩2" "w⇩2 ≼⇩F w⇩1" using 0 by auto
have 10: "length w⇩1 = length w⇩2" using 1 by force
obtain v⇩1 v⇩2 where 2: "w⇩1 @ v⇩1 =⇩F w⇩2" "w⇩2 @ v⇩2 =⇩F w⇩1" using 1 by (elim le_finE)
have 3: "length w⇩1 = length (w⇩1 @ v⇩1)" using 2 10 by force
have 4: "w⇩1 = w⇩1 @ v⇩1" using 3 by auto
have 5: "length w⇩2 = length (w⇩2 @ v⇩2)" using 2 10 by force
have 6: "w⇩2 = w⇩2 @ v⇩2" using 5 by auto
show "w⇩1 =⇩F w⇩2" using 4 6 2 by simp
qed

lemma le_fin_reflp[simp, intro]: "w ≼⇩F w" by auto
lemma le_fin_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 ≼⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
proof -
obtain v⇩1 where 1: "w⇩1 @ v⇩1 =⇩F w⇩2" using assms(1) by rule
obtain v⇩2 where 2: "w⇩2 @ v⇩2 =⇩F w⇩3" using assms(2) by rule
show ?thesis
proof
have "w⇩1 @ v⇩1 @ v⇩2 = (w⇩1 @ v⇩1) @ v⇩2" by simp
also have "… =⇩F w⇩2 @ v⇩2" using 1 by blast
also have "… =⇩F w⇩3" using 2 by blast
finally show "w⇩1 @ v⇩1 @ v⇩2 =⇩F w⇩3" by this
qed
qed
lemma eq_fin_le_fin_transp[intro, trans]:
assumes "w⇩1 =⇩F w⇩2" "w⇩2 ≼⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
using assms by auto
lemma le_fin_eq_fin_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 =⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
using assms by auto
lemma prefix_le_fin_transp[intro, trans]:
assumes "w⇩1 ≤ w⇩2" "w⇩2 ≼⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
proof -
obtain v⇩1 where 1: "w⇩2 = w⇩1 @ v⇩1" using assms(1) by rule
obtain v⇩2 where 2: "w⇩2 @ v⇩2 =⇩F w⇩3" using assms(2) by rule
show ?thesis
proof
show "w⇩1 @ v⇩1 @ v⇩2 =⇩F w⇩3" using 1 2 by simp
qed
qed
lemma le_fin_prefix_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 ≤ w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
proof -
obtain v⇩1 where 1: "w⇩1 @ v⇩1 =⇩F w⇩2" using assms(1) by rule
obtain v⇩2 where 2: "w⇩3 = w⇩2 @ v⇩2" using assms(2) by rule
show ?thesis
proof
have "w⇩1 @ v⇩1 @ v⇩2 = (w⇩1 @ v⇩1) @ v⇩2" by simp
also have "… =⇩F w⇩2 @ v⇩2" using 1 by blast
also have "… = w⇩3" using 2 by simp
finally show "w⇩1 @ v⇩1 @ v⇩2 =⇩F w⇩3" by this
qed
qed
lemma prefix_eq_fin_transp[intro, trans]:
assumes "w⇩1 ≤ w⇩2" "w⇩2 =⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
using assms by auto

lemma le_fin_concat_start[iff]: "w @ w⇩1 ≼⇩F w @ w⇩2 ⟷ w⇩1 ≼⇩F w⇩2"
proof
assume 0: "w @ w⇩1 ≼⇩F w @ w⇩2"
obtain v⇩1 where 1: "w @ w⇩1 @ v⇩1 =⇩F w @ w⇩2" using 0 by auto
show "w⇩1 ≼⇩F w⇩2" using 1 by auto
next
assume 0: "w⇩1 ≼⇩F w⇩2"
obtain v⇩1 where 1: "w⇩1 @ v⇩1 =⇩F w⇩2" using 0 by auto
have 2: "(w @ w⇩1) @ v⇩1 =⇩F w @ w⇩2" using 1 by auto
show "w @ w⇩1 ≼⇩F w @ w⇩2" using 2 by blast
qed
lemma le_fin_concat_end[dest]:
assumes "w⇩1 ≼⇩F w⇩2"
shows "w⇩1 ≼⇩F w⇩2 @ w"
proof -
obtain v⇩1 where 1: "w⇩1 @ v⇩1 =⇩F w⇩2" using assms by rule
show ?thesis
proof
have "w⇩1 @ v⇩1 @ w = (w⇩1 @ v⇩1) @ w" by simp
also have "… =⇩F w⇩2 @ w" using 1 by blast
finally show "w⇩1 @ v⇩1 @ w =⇩F w⇩2 @ w" by this
qed
qed

definition le_fininf :: "'item list ⇒ 'item stream ⇒ bool" (infix "≼⇩F⇩I" 50)
where "w⇩1 ≼⇩F⇩I w⇩2 ≡ ∃ v⇩2. v⇩2 ≤⇩F⇩I w⇩2 ∧ w⇩1 ≼⇩F v⇩2"

lemma le_fininfI[intro 0]:
assumes "v⇩2 ≤⇩F⇩I w⇩2" "w⇩1 ≼⇩F v⇩2"
shows "w⇩1 ≼⇩F⇩I w⇩2"
using assms unfolding le_fininf_def by auto
lemma le_fininfE[elim 0]:
assumes "w⇩1 ≼⇩F⇩I w⇩2"
obtains v⇩2
where "v⇩2 ≤⇩F⇩I w⇩2" "w⇩1 ≼⇩F v⇩2"
using assms unfolding le_fininf_def by auto

lemma le_fininf_empty[simp]: "[] ≼⇩F⇩I w" by force

lemma le_fininf_range[dest]: "w⇩1 ≼⇩F⇩I w⇩2 ⟹ set w⇩1 ⊆ sset w⇩2" by force

lemma eq_fin_le_fininf_transp[intro, trans]:
assumes "w⇩1 =⇩F w⇩2" "w⇩2 ≼⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma le_fin_le_fininf_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 ≼⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma prefix_le_fininf_transp[intro, trans]:
assumes "w⇩1 ≤ w⇩2" "w⇩2 ≼⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by auto
lemma le_fin_prefix_fininf_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 ≤⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by auto
lemma eq_fin_prefix_fininf_transp[intro, trans]:
assumes "w⇩1 =⇩F w⇩2" "w⇩2 ≤⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by auto

lemma le_fininf_concat_start[iff]: "w @ w⇩1 ≼⇩F⇩I w @- w⇩2 ⟷ w⇩1 ≼⇩F⇩I w⇩2"
proof
assume 0: "w @ w⇩1 ≼⇩F⇩I w @- w⇩2"
obtain v⇩2 where 1: "v⇩2 ≤⇩F⇩I w @- w⇩2" "w @ w⇩1 ≼⇩F v⇩2" using 0 by rule
have 2: "length w ≤ length v⇩2" using 1(2) by force
have 4: "w ≤ v⇩2" using prefix_fininf_extend[OF 1(1) 2] by this
obtain v⇩1 where 5: "v⇩2 = w @ v⇩1" using 4 by rule
show "w⇩1 ≼⇩F⇩I w⇩2"
proof
show "v⇩1 ≤⇩F⇩I w⇩2" using 1(1) unfolding 5 by auto
show "w⇩1 ≼⇩F v⇩1" using 1(2) unfolding 5 by simp
qed
next
assume 0: "w⇩1 ≼⇩F⇩I w⇩2"
obtain v⇩2 where 1: "v⇩2 ≤⇩F⇩I w⇩2" "w⇩1 ≼⇩F v⇩2" using 0 by rule
show "w @ w⇩1 ≼⇩F⇩I w @- w⇩2"
proof
show "w @ v⇩2 ≤⇩F⇩I (w @- w⇩2)" using 1(1) by auto
show "w @ w⇩1 ≼⇩F w @ v⇩2" using 1(2) by auto
qed
qed

lemma le_fininf_singleton[intro, simp]: "[shd v] ≼⇩F⇩I v"
proof -
have "[shd v] ≼⇩F⇩I shd v ## sdrop 1 v" by blast
also have "… = v" by simp
finally show ?thesis by this
qed

definition le_inf :: "'item stream ⇒ 'item stream ⇒ bool" (infix "≼⇩I" 50)
where "w⇩1 ≼⇩I w⇩2 ≡ ∀ v⇩1. v⇩1 ≤⇩F⇩I w⇩1 ⟶ v⇩1 ≼⇩F⇩I w⇩2"

lemma le_infI[intro 0]:
assumes "⋀ v⇩1. v⇩1 ≤⇩F⇩I w⇩1 ⟹ v⇩1 ≼⇩F⇩I w⇩2"
shows "w⇩1 ≼⇩I w⇩2"
using assms unfolding le_inf_def by auto
lemma le_infE[elim 0]:
assumes "w⇩1 ≼⇩I w⇩2" "v⇩1 ≤⇩F⇩I w⇩1"
obtains "v⇩1 ≼⇩F⇩I w⇩2"
using assms unfolding le_inf_def by auto

lemma le_inf_range[dest]:
assumes "w⇩1 ≼⇩I w⇩2"
shows "sset w⇩1 ⊆ sset w⇩2"
proof
fix a
assume 1: "a ∈ sset w⇩1"
obtain i where 2: "a = w⇩1 !! i" using 1 by (metis imageE sset_range)
have 3: "stake (Suc i) w⇩1 ≤⇩F⇩I w⇩1" by rule
have 4: "stake (Suc i) w⇩1 ≼⇩F⇩I w⇩2" using assms 3 by rule
have 5: "w⇩1 !! i ∈ set (stake (Suc i) w⇩1)" by (meson lessI set_stake_snth)
show "a ∈ sset w⇩2" unfolding 2 using 5 4 by fastforce
qed

lemma le_inf_reflp[simp, intro]: "w ≼⇩I w" by auto
lemma prefix_fininf_le_inf_transp[intro, trans]:
assumes "w⇩1 ≤⇩F⇩I w⇩2" "w⇩2 ≼⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma le_fininf_le_inf_transp[intro, trans]:
assumes "w⇩1 ≼⇩F⇩I w⇩2" "w⇩2 ≼⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma le_inf_transp[intro, trans]:
assumes "w⇩1 ≼⇩I w⇩2" "w⇩2 ≼⇩I w⇩3"
shows "w⇩1 ≼⇩I w⇩3"
using assms by blast

lemma le_infI':
assumes "⋀ k. ∃ v. v ≤⇩F⇩I w⇩1 ∧ k < length v ∧ v ≼⇩F⇩I w⇩2"
shows "w⇩1 ≼⇩I w⇩2"
proof
fix u
assume 1: "u ≤⇩F⇩I w⇩1"
obtain v where 2: "v ≤⇩F⇩I w⇩1" "length u < length v" "v ≼⇩F⇩I w⇩2" using assms by auto
have 3: "length u ≤ length v" using 2(2) by auto
have 4: "u ≤ v" using prefix_fininf_length 1 2(1) 3 by this
show "u ≼⇩F⇩I w⇩2" using 4 2(3) by rule
qed

lemma le_infI_chain_left:
assumes "chain w" "⋀ k. w k ≼⇩F⇩I v"
shows "limit w ≼⇩I v"
proof (rule le_infI')
fix k
obtain l where 1: "k < length (w l)" using assms(1) by rule
show "∃ va. va ≤⇩F⇩I limit w ∧ k < length va ∧ va ≼⇩F⇩I v"
proof (intro exI conjI)
show "w l ≤⇩F⇩I limit w" using chain_prefix_limit assms(1) by this
show "k < length (w l)" using 1 by this
show "w l ≼⇩F⇩I v" using assms(2) by this
qed
qed
lemma le_infI_chain_right:
assumes "chain w" "⋀ u. u ≤⇩F⇩I v ⟹ u ≼⇩F w (l u)"
shows "v ≼⇩I limit w"
proof
fix u
assume 1: "u ≤⇩F⇩I v"
show "u ≼⇩F⇩I limit w"
proof
show "w (l u) ≤⇩F⇩I limit w" using chain_prefix_limit assms(1) by this
show "u ≼⇩F w (l u)" using assms(2) 1 by this
qed
qed
lemma le_infI_chain_right':
assumes "chain w" "⋀ k. stake k v ≼⇩F w (l k)"
shows "v ≼⇩I limit w"
proof (rule le_infI_chain_right)
show "chain w" using assms(1) by this
next
fix u
assume 1: "u ≤⇩F⇩I v"
have 2: "stake (length u) v = u" using 1 by (simp add: prefix_fininf_def shift_eq)
have 3: "stake (length u) v ≼⇩F w (l (length u))" using assms(2) by this
show "u ≼⇩F w (l (length u))" using 3 unfolding 2 by this
qed

definition eq_inf :: "'item stream ⇒ 'item stream ⇒ bool" (infix "=⇩I" 50)
where "w⇩1 =⇩I w⇩2 ≡ w⇩1 ≼⇩I w⇩2 ∧ w⇩2 ≼⇩I w⇩1"

lemma eq_infI[intro 0]:
assumes "w⇩1 ≼⇩I w⇩2" "w⇩2 ≼⇩I w⇩1"
shows "w⇩1 =⇩I w⇩2"
using assms unfolding eq_inf_def by auto
lemma eq_infE[elim 0]:
assumes "w⇩1 =⇩I w⇩2"
obtains "w⇩1 ≼⇩I w⇩2" "w⇩2 ≼⇩I w⇩1"
using assms unfolding eq_inf_def by auto

lemma eq_inf_range[dest]: "w⇩1 =⇩I w⇩2 ⟹ sset w⇩1 = sset w⇩2" by force

lemma eq_inf_reflp[simp, intro]: "w =⇩I w" by auto
lemma eq_inf_symp[intro]: "w⇩1 =⇩I w⇩2 ⟹ w⇩2 =⇩I w⇩1" by auto
lemma eq_inf_transp[intro, trans]:
assumes "w⇩1 =⇩I w⇩2" "w⇩2 =⇩I w⇩3"
shows "w⇩1 =⇩I w⇩3"
using assms by blast
lemma le_fininf_eq_inf_transp[intro, trans]:
assumes "w⇩1 ≼⇩F⇩I w⇩2" "w⇩2 =⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma le_inf_eq_inf_transp[intro, trans]:
assumes "w⇩1 ≼⇩I w⇩2" "w⇩2 =⇩I w⇩3"
shows "w⇩1 ≼⇩I w⇩3"
using assms by blast
lemma eq_inf_le_inf_transp[intro, trans]:
assumes "w⇩1 =⇩I w⇩2" "w⇩2 ≼⇩I w⇩3"
shows "w⇩1 ≼⇩I w⇩3"
using assms by blast
lemma prefix_fininf_eq_inf_transp[intro, trans]:
assumes "w⇩1 ≤⇩F⇩I w⇩2" "w⇩2 =⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast

lemma le_inf_concat_start[iff]: "w @- w⇩1 ≼⇩I w @- w⇩2 ⟷ w⇩1 ≼⇩I w⇩2"
proof
assume 1: "w @- w⇩1 ≼⇩I w @- w⇩2"
show "w⇩1 ≼⇩I w⇩2"
proof
fix v⇩1
assume 2: "v⇩1 ≤⇩F⇩I w⇩1"
have "w @ v⇩1 ≤⇩F⇩I w @- w⇩1" using 2 by auto
also have "… ≼⇩I w @- w⇩2" using 1 by this
finally show "v⇩1 ≼⇩F⇩I w⇩2" by rule
qed
next
assume 1: "w⇩1 ≼⇩I w⇩2"
show "w @- w⇩1 ≼⇩I w @- w⇩2"
proof
fix v⇩1
assume 2: "v⇩1 ≤⇩F⇩I w @- w⇩1"
then show "v⇩1 ≼⇩F⇩I w @- w⇩2"
proof (cases rule: prefix_fininf_append)
case (absorb)
show ?thesis using absorb by auto
next
case (extend z)
show ?thesis using 1 extend by auto
qed
qed
qed
lemma eq_fin_le_inf_concat_end[dest]: "w⇩1 =⇩F w⇩2 ⟹ w⇩1 @- w ≼⇩I w⇩2 @- w"
proof
fix v⇩1
assume 1: "w⇩1 =⇩F w⇩2" "v⇩1 ≤⇩F⇩I w⇩1 @- w"
show "v⇩1 ≼⇩F⇩I w⇩2 @- w"
using 1(2)
proof (cases rule: prefix_fininf_append)
case (absorb)
show ?thesis
proof
show "w⇩2 ≤⇩F⇩I (w⇩2 @- w)" by auto
show "v⇩1 ≼⇩F w⇩2" using absorb 1(1) by auto
qed
next
case (extend w')
show ?thesis
proof
show "w⇩2 @ w' ≤⇩F⇩I (w⇩2 @- w)" using extend(2) by auto
show "v⇩1 ≼⇩F w⇩2 @ w'" unfolding extend(1) using 1(1) by auto
qed
qed
qed

lemma eq_inf_concat_start[iff]: "w @- w⇩1 =⇩I w @- w⇩2 ⟷ w⇩1 =⇩I w⇩2" by blast
lemma eq_inf_concat_end[dest]: "w⇩1 =⇩F w⇩2 ⟹ w⇩1 @- w =⇩I w⇩2 @- w"
proof -
assume 0: "w⇩1 =⇩F w⇩2"
have 1: "w⇩2 =⇩F w⇩1" using 0 by auto
show "w⇩1 @- w =⇩I w⇩2 @- w"
using eq_fin_le_inf_concat_end[OF 0] eq_fin_le_inf_concat_end[OF 1] by auto
qed

lemma le_fininf_suffixI[intro]:
assumes "w =⇩I w⇩1 @- w⇩2"
shows "w⇩1 ≼⇩F⇩I w"
using assms by blast
lemma le_fininf_suffixE[elim]:
assumes "w⇩1 ≼⇩F⇩I w"
obtains w⇩2
where "w =⇩I w⇩1 @- w⇩2"
proof -
obtain v⇩2 where 1: "v⇩2 ≤⇩F⇩I w" "w⇩1 ≼⇩F v⇩2" using assms(1) by rule
obtain u⇩1 where 2: "w⇩1 @ u⇩1 =⇩F v⇩2" using 1(2) by rule
obtain v⇩2' where 3: "w = v⇩2 @- v⇩2'" using 1(1) by rule
show ?thesis
proof
show "w =⇩I w⇩1 @- u⇩1 @- v⇩2'" unfolding 3 using 2 by fastforce
qed
qed

lemma subsume_fin:
assumes "u⇩1 ≼⇩F⇩I w" "v⇩1 ≼⇩F⇩I w"
obtains w⇩1
where "u⇩1 ≼⇩F w⇩1" "v⇩1 ≼⇩F w⇩1"
proof -
obtain u⇩2 where 2: "u⇩2 ≤⇩F⇩I w" "u⇩1 ≼⇩F u⇩2" using assms(1) by rule
obtain v⇩2 where 3: "v⇩2 ≤⇩F⇩I w" "v⇩1 ≼⇩F v⇩2" using assms(2) by rule
show ?thesis
proof (cases "length u⇩2" "length v⇩2" rule: le_cases)
case le
show ?thesis
proof
show "u⇩1 ≼⇩F v⇩2" using 2(2) prefix_fininf_length[OF 2(1) 3(1) le] by auto
show "v⇩1 ≼⇩F v⇩2" using 3(2) by this
qed
next
case ge
show ?thesis
proof
show "u⇩1 ≼⇩F u⇩2" using 2(2) by this
show "v⇩1 ≼⇩F u⇩2" using 3(2) prefix_fininf_length[OF 3(1) 2(1) ge] by auto
qed
qed
qed

lemma eq_fin_end:
assumes "u⇩1 =⇩F u⇩2" "u⇩1 @ v⇩1 =⇩F u⇩2 @ v⇩2"
shows "v⇩1 =⇩F v⇩2"
proof -
have "u⇩1 @ v⇩2 =⇩F u⇩2 @ v⇩2" using assms(1) by blast
also have "… =⇩F u⇩1 @ v⇩1" using assms(2) by blast
finally show ?thesis by blast
qed

definition indoc :: "'item ⇒ 'item list ⇒ bool"
where "indoc a u ≡ ∃ u⇩1 u⇩2. u = u⇩1 @ [a] @ u⇩2 ∧ a ∉ set u⇩1 ∧ Ind {a} (set u⇩1)"

lemma indoc_set: "indoc a u ⟹ a ∈ set u" unfolding indoc_def by auto

lemma indoc_appendI1[intro]:
assumes "indoc a u"
shows "indoc a (u @ v)"
using assms unfolding indoc_def by force
lemma indoc_appendI2[intro]:
assumes "a ∉ set u" "Ind {a} (set u)" "indoc a v"
shows "indoc a (u @ v)"
proof -
obtain v⇩1 v⇩2 where 1: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1" "Ind {a} (set v⇩1)"
using assms(3) unfolding indoc_def by blast
show ?thesis
proof (unfold indoc_def, intro exI conjI)
show "u @ v = (u @ v⇩1) @ [a] @ v⇩2" unfolding 1(1) by simp
show "a ∉ set (u @ v⇩1)" using assms(1) 1(2) by auto
show "Ind {a} (set (u @ v⇩1))" using assms(2) 1(3) by auto
qed
qed
lemma indoc_appendE[elim!]:
assumes "indoc a (u @ v)"
obtains (first) "a ∈ set u" "indoc a u" | (second)  "a ∉ set u" "Ind {a} (set u)" "indoc a v"
proof -
obtain w⇩1 w⇩2 where 1: "u @ v = w⇩1 @ [a] @ w⇩2" "a ∉ set w⇩1" "Ind {a} (set w⇩1)"
using assms unfolding indoc_def by blast
show ?thesis
proof (cases "a ∈ set u")
case True
obtain u⇩1 u⇩2 where 2: "u = u⇩1 @ [a] @ u⇩2" "a ∉ set u⇩1"
using split_list_first[OF True] by auto
have 3: "w⇩1 = u⇩1"
proof (rule split_list_first_unique)
show "w⇩1 @ [a] @ w⇩2 = u⇩1 @ [a] @ u⇩2 @ v" using 1(1) unfolding 2(1) by simp
show "a ∉ set w⇩1" using 1(2) by auto
show "a ∉ set u⇩1" using 2(2) by this
qed
show ?thesis
proof (rule first)
show "a ∈ set u" using True by this
show "indoc a u"
proof (unfold indoc_def, intro exI conjI)
show "u = u⇩1 @ [a] @ u⇩2" using 2(1) by this
show "a ∉ set u⇩1" using 1(2) unfolding 3 by this
show "Ind {a} (set u⇩1)" using 1(3) unfolding 3 by this
qed
qed
next
case False
have 2: "a ∈ set v" using indoc_set assms False by fastforce
obtain v⇩1 v⇩2 where 3: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1"
using split_list_first[OF 2] by auto
have 4: "w⇩1 = u @ v⇩1"
proof (rule split_list_first_unique)
show "w⇩1 @ [a] @ w⇩2 = (u @ v⇩1) @ [a] @ v⇩2" using 1(1) unfolding 3(1) by simp
show "a ∉ set w⇩1" using 1(2) by auto
show "a ∉ set (u @ v⇩1)" using False 3(2) by auto
qed
show ?thesis
proof (rule second)
show "a ∉ set u" using False by this
show "Ind {a} (set u)" using 1(3) 4 by auto
show "indoc a v"
proof (unfold indoc_def, intro exI conjI)
show "v = v⇩1 @ [a] @ v⇩2" using 3(1) by this
show "a ∉ set v⇩1" using 1(2) unfolding 4 by auto
show "Ind {a} (set v⇩1)" using 1(3) unfolding 4 by auto
qed
qed
qed
qed

lemma indoc_single: "indoc a [b] ⟷ a = b"
proof
assume 1: "indoc a [b]"
obtain u⇩1 u⇩2 where 2: "[b] = u⇩1 @ [a] @ u⇩2" "Ind {a} (set u⇩1)"
using 1 unfolding indoc_def by auto
show "a = b" using 2(1)
by (metis append_eq_Cons_conv append_is_Nil_conv list.distinct(2) list.inject)
next
assume 1: "a = b"
show "indoc a [b]"
unfolding indoc_def 1
proof (intro exI conjI)
show "[b] = [] @ [b] @ []" by simp
show "b ∉ set []" by simp
show "Ind {b} (set [])" by simp
qed
qed

lemma indoc_append[simp]: "indoc a (u @ v) ⟷
indoc a u ∨ a ∉ set u ∧ Ind {a} (set u) ∧ indoc a v" by blast
lemma indoc_Nil[simp]: "indoc a [] ⟷ False" unfolding indoc_def by auto
lemma indoc_Cons[simp]: "indoc a (b # v) ⟷ a = b ∨ a ≠ b ∧ ind a b ∧ indoc a v"
proof -
have "indoc a (b # v) ⟷ indoc a ([b] @ v)" by simp
also have "… ⟷ indoc a [b] ∨ a ∉ set [b] ∧ Ind {a} (set [b]) ∧ indoc a v"
unfolding indoc_append by rule
also have "… ⟷ a = b ∨ a ≠ b ∧ ind a b ∧ indoc a v" unfolding indoc_single by simp
finally show ?thesis by this
qed

lemma eq_swap_indoc: "u =⇩S v ⟹ indoc c u ⟹ indoc c v" by auto
lemma eq_fin_indoc: "u =⇩F v ⟹ indoc c u ⟹ indoc c v" by (induct rule: rtranclp.induct, auto)

lemma eq_fin_ind':
assumes "[a] @ u =⇩F u⇩1 @ [a] @ u⇩2" "a ∉ set u⇩1"
shows "Ind {a} (set u⇩1)"
proof -
have 1: "indoc a ([a] @ u)" by simp
have 2: "indoc a (u⇩1 @ [a] @ u⇩2)" using eq_fin_indoc assms(1) 1 by this
show ?thesis using assms(2) 2 by blast
qed
lemma eq_fin_ind:
assumes "u @ v =⇩F v @ u" "set u ∩ set v = {}"
shows "Ind (set u) (set v)"
using assms
proof (induct u)
case Nil
show ?case by simp
next
case (Cons a u)
have 1: "Ind {a} (set v)"
proof (rule eq_fin_ind')
show "[a] @ u @ v =⇩F v @ [a] @ u" using Cons(2) by simp
show "a ∉ set v" using Cons(3) by simp
qed
have 2: "Ind (set [a]) (set v)" using 1 by simp
have 4: "Ind (set u) (set v)"
proof (rule Cons(1))
have "[a] @ u @ v = (a # u) @ v" by simp
also have "… =⇩F v @ a # u" using Cons(2) by this
also have "… = (v @ [a]) @ u" by simp
also have "… =⇩F ([a] @ v) @ u" using 2 by blast
also have "… = [a] @ v @ u" by simp
finally show "u @ v =⇩F v @ u" by blast
show "set u ∩ set v = {}" using Cons(3) by auto
qed
show ?case using 1 4 by auto
qed

lemma le_fin_member':
assumes "[a] ≼⇩F u @ v" "a ∈ set u"
shows "[a] ≼⇩F u"
proof -
obtain w where 1: "[a] @ w =⇩F u @ v" using assms(1) by rule
obtain u⇩1 u⇩2 where 2: "u = u⇩1 @ [a] @ u⇩2" "a ∉ set u⇩1"
using split_list_first[OF assms(2)] by auto
have 3: "Ind {a} (set u⇩1)"
proof (rule eq_fin_ind')
show "[a] @ w =⇩F u⇩1 @ [a] @ u⇩2 @ v" using 1 unfolding 2(1) by simp
show "a ∉ set u⇩1" using 2(2) by this
qed
have 4: "Ind (set [a]) (set u⇩1)" using 3 by simp
have "[a] ≤ [a] @ u⇩1 @ u⇩2" by auto
also have "… = ([a] @ u⇩1) @ u⇩2" by simp
also have "… =⇩F (u⇩1 @ [a]) @ u⇩2" using 4 by blast
also have "… = u" unfolding 2(1) by simp
finally show ?thesis by this
qed
lemma le_fin_not_member':
assumes "[a] ≼⇩F u @ v" "a ∉ set u"
shows "[a] ≼⇩F v"
proof -
obtain w where 1: "[a] @ w =⇩F u @ v" using assms(1) by rule
have 3: "a ∈ set v" using assms by auto
obtain v⇩1 v⇩2 where 4: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1" using split_list_first[OF 3] by auto
have 5: "[a] @ w =⇩F u @ v⇩1 @ [a] @ v⇩2" using 1 unfolding 4(1) by this
have 6: "Ind {a} (set (u @ v⇩1))"
proof (rule eq_fin_ind')
show "[a] @ w =⇩F (u @ v⇩1) @ [a] @ v⇩2" using 5 by simp
show "a ∉ set (u @ v⇩1)" using assms(2) 4(2) by auto
qed
have 9: "Ind (set [a]) (set v⇩1)" using 6 by auto
have "[a] ≤ [a] @ v⇩1 @ v⇩2" by auto
also have "… = ([a] @ v⇩1) @ v⇩2" by simp
also have "… =⇩F (v⇩1 @ [a]) @ v⇩2" using 9 by blast
also have "… = v⇩1 @ [a] @ v⇩2" by simp
also have "… = v" unfolding 4(1) by rule
finally show ?thesis by this
qed
lemma le_fininf_not_member':
assumes "[a] ≼⇩F⇩I u @- v" "a ∉ set u"
shows "[a] ≼⇩F⇩I v"
proof -
obtain v⇩2 where 1: "v⇩2 ≤⇩F⇩I u @- v" "[a] ≼⇩F v⇩2" using le_fininfE assms(1) by this
show ?thesis
using 1(1)
proof (cases rule: prefix_fininf_append)
case absorb
have "[a] ≼⇩F v⇩2" using 1(2) by this
also have "… ≤ u" using absorb by this
finally have 2: "a ∈ set u" by force
show ?thesis using assms(2) 2 by simp
next
case (extend z)
have "[a] ≼⇩F v⇩2" using 1(2) by this
also have "… = u @ z" using extend(1) by this
finally have 2: "[a] ≼⇩F u @ z" by this
have "[a] ≼⇩F z" using le_fin_not_member' 2 assms(2) by this
also have "… ≤⇩F⇩I v" using extend(2) by this
finally show ?thesis by this
qed
qed

lemma le_fin_ind'':
assumes "[a] ≼⇩F w" "[b] ≼⇩F w" "a ≠ b"
shows "ind a b"
proof -
obtain u where 1: "[a] @ u =⇩F w" using assms(1) by rule
obtain v where 2: "[b] @ v =⇩F w" using assms(2) by rule
have 3: "[a] @ u =⇩F [b] @ v" using 1 2[symmetric] by auto
have 4: "a ∈ set v" using 3 assms(3)
by (metis append_Cons append_Nil eq_fin_range list.set_intros(1) set_ConsD)
obtain v⇩1 v⇩2 where 5: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1" using split_list_first[OF 4] by auto
have 7: "Ind {a} (set ([b] @ v⇩1))"
proof (rule eq_fin_ind')
show "[a] @ u =⇩F ([b] @ v⇩1) @ [a] @ v⇩2" using 3 unfolding 5(1) by simp
show "a ∉ set ([b] @ v⇩1)" using assms(3) 5(2) by auto
qed
show ?thesis using 7 by auto
qed
lemma le_fin_ind':
assumes "[a] ≼⇩F w" "v ≼⇩F w" "a ∉ set v"
shows "Ind {a} (set v)"
using assms
proof (induct v arbitrary: w)
case Nil
show ?case by simp
next
case (Cons b v)
have 1: "ind a b"
proof (rule le_fin_ind'')
show "[a] ≼⇩F w" using Cons(2) by this
show "[b] ≼⇩F w" using Cons(3) by auto
show "a ≠ b" using Cons(4) by auto
qed
obtain w' where 2: "[b] @ w' =⇩F w" using Cons(3) by auto
have 3: "Ind {a} (set v)"
proof (rule Cons(1))
show "[a] ≼⇩F w'"
proof (rule le_fin_not_member')
show "[a] ≼⇩F [b] @ w'" using Cons(2) 2 by auto
show "a ∉ set [b]" using Cons(4) by auto
qed
have "[b] @ v = b # v" by simp
also have "… ≼⇩F w" using Cons(3) by this
also have "… =⇩F [b] @ w'" using 2 by auto
finally show "v ≼⇩F w'" by blast
show "a ∉ set v" using Cons(4) by auto
qed
show ?case using 1 3 by auto
qed
lemma le_fininf_ind'':
assumes "[a] ≼⇩F⇩I w" "[b] ≼⇩F⇩I w" "a ≠ b"
shows "ind a b"
using subsume_fin le_fin_ind'' assms by metis
lemma le_fininf_ind':
assumes "[a] ≼⇩F⇩I w" "v ≼⇩F⇩I w" "a ∉ set v"
shows "Ind {a} (set v)"
using subsume_fin le_fin_ind' assms by metis

lemma indoc_alt_def: "indoc a v ⟷ v =⇩F [a] @ remove1 a v"
proof
assume 0: "indoc a v"
obtain v⇩1 v⇩2 where 1: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1" "Ind {a} (set v⇩1)"
using 0 unfolding indoc_def by blast
have 2: "Ind (set [a]) (set v⇩1)" using 1(3) by simp
have "v = v⇩1 @ [a] @ v⇩2" using 1(1) by this
also have "… = (v⇩1 @ [a]) @ v⇩2" by simp
also have "… =⇩F ([a] @ v⇩1) @ v⇩2" using 2 by blast
also have "… = [a] @ v⇩1 @ v⇩2" by simp
also have "… = [a] @ remove1 a v" unfolding 1(1) remove1_append using 1(2) by auto
finally show "v =⇩F [a] @ remove1 a v" by this
next
assume 0: "v =⇩F [a] @ remove1 a v"
have 1: "indoc a ([a] @ remove1 a v)" by simp
show "indoc a v" using eq_fin_indoc 0  1 by blast
qed

lemma levi_lemma:
assumes "t @ u =⇩F v @ w"
obtains p r s q
where "t =⇩F p @ r" "u =⇩F s @ q" "v =⇩F p @ s" "w =⇩F r @ q" "Ind (set r) (set s)"
using assms
proof (induct t arbitrary: thesis v w)
case Nil
show ?case
proof (rule Nil(1))
show "[] =⇩F [] @ []" by simp
show "v =⇩F [] @ v" by simp
show "u =⇩F v @ w" using Nil(2) by simp
show "w =⇩F [] @ w" by simp
show "Ind (set []) (set v)" by simp
qed
next
case (Cons a t')
have 1: "[a] ≼⇩F v @ w" using Cons(3) by blast
show ?case
proof (cases "a ∈ set v")
case False
have 2: "[a] ≼⇩F w" using le_fin_not_member' 1 False by this
obtain w' where 3: "w =⇩F [a] @ w'" using 2 by blast
have 4: "v ≼⇩F v @ w" by auto
have 5: "Ind (set [a]) (set v)" using le_fin_ind'[OF 1 4] False by simp
have "[a] @ t' @ u = (a # t') @ u" by simp
also have "… =⇩F v @ w" using Cons(3) by this
also have "… =⇩F v @ [a] @ w'" using 3 by blast
also have "… = (v @ [a]) @ w'" by simp
also have "… =⇩F ([a] @ v) @ w'" using 5 by blast
also have "… = [a] @ v @ w'" by simp
finally have 6: "t' @ u =⇩F v @ w'" by blast
obtain p r' s q where 7: "t' =⇩F p @ r'" "u =⇩F s @ q" "v =⇩F p @ s" "w' =⇩F r' @ q"
"Ind (set r') (set s)" using Cons(1)[OF _ 6] by this
have 8: "set v = set p ∪ set s" using eq_fin_range 7(3) by auto
have 9: "Ind (set [a]) (set p)" using 5 8 by auto
have 10: "Ind (set [a]) (set s)" using 5 8 by auto
show ?thesis
proof (rule Cons(2))
have "a # t' = [a] @ t'" by simp
also have "… =⇩F [a] @ p @ r'" using 7(1) by blast
also have "… = ([a] @ p) @ r'" by simp
also have "… =⇩F (p @ [a]) @ r'" using 9 by blast
also have "… = p @ [a] @ r'" by simp
finally show "a # t' =⇩F p @ [a] @ r'" by this
show "u =⇩F s @ q" using 7(2) by this
show "v =⇩F p @ s" using 7(3) by this
have "w =⇩F [a] @ w'" using 3 by this
also have "… =⇩F [a] @ r' @ q" using 7(4) by blast
also have "… = ([a] @ r') @ q" by simp
finally show "w =⇩F ([a] @ r') @ q" by this
show "Ind (set ([a] @ r')) (set s)" using 7(5) 10 by auto
qed
next
case True
have 2: "[a] ≼⇩F v" using le_fin_member' 1 True by this
obtain v' where 3: "v =⇩F [a] @ v'" using 2 by blast
have "[a] @ t' @ u = (a # t') @ u" by simp
also have "… =⇩F v @ w" using Cons(3) by this
also have "… =⇩F ([a] @ v') @ w" using 3 by blast
also have "… = [a] @ v' @ w" by simp
finally have 4: "t' @ u =⇩F v' @ w" by blast
obtain p' r s q where 7: "t' =⇩F p' @ r" "u =⇩F s @ q" "v' =⇩F p' @ s" "w =⇩F r @ q"
"Ind (set r) (set s)" using Cons(1)[OF _ 4] by this
show ?thesis
proof (rule Cons(2))
have "a # t' = [a] @ t'" by simp
also have "… =⇩F [a] @ p' @ r" using 7(1) by blast
also have "… = ([a] @ p') @ r" by simp
finally show "a # t' =⇩F ([a] @ p') @ r" by this
show "u =⇩F s @ q" using 7(2) by this
have "v =⇩F [a] @ v'" using 3 by this
also have "… =⇩F [a] @ p' @ s" using 7(3) by blast
also have "… = ([a] @ p') @ s" by simp
finally show "v =⇩F ([a] @ p') @ s" by this
show "w =⇩F r @ q" using 7(4) by this
show "Ind (set r) (set s)" using 7(5) by this
qed
qed
qed

end

end
```