[STATEMENT]
lemma FG_advice_minus_size:
  "\<lbrakk>size \<phi> \<le> size \<psi>; \<phi> \<noteq> \<psi>\<rbrakk> \<Longrightarrow> \<phi>[Y - {\<psi>}]\<^sub>\<mu> = \<phi>[Y]\<^sub>\<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size \<phi> \<le> size \<psi>; \<phi> \<noteq> \<psi>\<rbrakk> \<Longrightarrow> \<phi>[Y - {\<psi>}]\<^sub>\<mu> = \<phi>[Y]\<^sub>\<mu>
[PROOF STEP]
using subfrmlsn_size subformulas\<^sub>\<nu>_subfrmlsn FG_advice_minus_subformulas
[PROOF STATE]
proof (prove)
using this:
?\<psi> \<in> subfrmlsn ?\<phi> \<Longrightarrow> size ?\<psi> < size ?\<phi> \<or> ?\<psi> = ?\<phi>
subformulas\<^sub>\<nu> ?\<phi> \<subseteq> subfrmlsn ?\<phi>
?\<psi> \<notin> subformulas\<^sub>\<nu> ?\<phi> \<Longrightarrow> ?\<phi>[?Y - {?\<psi>}]\<^sub>\<mu> = ?\<phi>[?Y]\<^sub>\<mu>

goal (1 subgoal):
 1. \<lbrakk>size \<phi> \<le> size \<psi>; \<phi> \<noteq> \<psi>\<rbrakk> \<Longrightarrow> \<phi>[Y - {\<psi>}]\<^sub>\<mu> = \<phi>[Y]\<^sub>\<mu>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma bind_returns_result_E3:
  assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y" and "h \<turnstile> f \<rightarrow>\<^sub>r x" and "pure f h"
  shows "h \<turnstile> g x \<rightarrow>\<^sub>r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> g x \<rightarrow>\<^sub>r y
[PROOF STEP]
using assms returns_result_eq bind_returns_result_E2
[PROOF STATE]
proof (prove)
using this:
h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y
h \<turnstile> f \<rightarrow>\<^sub>r x
pure f h
\<lbrakk>?h \<turnstile> ?f \<rightarrow>\<^sub>r ?y; ?h \<turnstile> ?f \<rightarrow>\<^sub>r ?y'\<rbrakk> \<Longrightarrow> ?y = ?y'
\<lbrakk>?h \<turnstile> ?f \<bind> ?g \<rightarrow>\<^sub>r ?y; pure ?f ?h; \<And>x. \<lbrakk>?h \<turnstile> ?f \<rightarrow>\<^sub>r x; ?h \<turnstile> ?g x \<rightarrow>\<^sub>r ?y\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. h \<turnstile> g x \<rightarrow>\<^sub>r y
[PROOF STEP]
by metis


[STATEMENT]
lemma iterate_M_concat:
  assumes "h \<turnstile> iterate_M xs \<rightarrow>\<^sub>h h'"
    and "h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''"
  shows "h \<turnstile> iterate_M (xs @ ys) \<rightarrow>\<^sub>h h''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> iterate_M (xs @ ys) \<rightarrow>\<^sub>h h''
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<turnstile> iterate_M xs \<rightarrow>\<^sub>h h'
h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''

goal (1 subgoal):
 1. h \<turnstile> iterate_M (xs @ ys) \<rightarrow>\<^sub>h h''
[PROOF STEP]
apply(induct "xs" arbitrary: h h'')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h h''. \<lbrakk>h \<turnstile> iterate_M [] \<rightarrow>\<^sub>h h'; h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''\<rbrakk> \<Longrightarrow> h \<turnstile> iterate_M ([] @ ys) \<rightarrow>\<^sub>h h''
 2. \<And>a xs h h''. \<lbrakk>\<And>h h''. \<lbrakk>h \<turnstile> iterate_M xs \<rightarrow>\<^sub>h h'; h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''\<rbrakk> \<Longrightarrow> h \<turnstile> iterate_M (xs @ ys) \<rightarrow>\<^sub>h h''; h \<turnstile> iterate_M (a # xs) \<rightarrow>\<^sub>h h'; h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''\<rbrakk> \<Longrightarrow> h \<turnstile> iterate_M ((a # xs) @ ys) \<rightarrow>\<^sub>h h''
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs h h''. \<lbrakk>\<And>h h''. \<lbrakk>h \<turnstile> iterate_M xs \<rightarrow>\<^sub>h h'; h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''\<rbrakk> \<Longrightarrow> h \<turnstile> iterate_M (xs @ ys) \<rightarrow>\<^sub>h h''; h \<turnstile> iterate_M (a # xs) \<rightarrow>\<^sub>h h'; h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''\<rbrakk> \<Longrightarrow> h \<turnstile> iterate_M ((a # xs) @ ys) \<rightarrow>\<^sub>h h''
[PROOF STEP]
apply(auto)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs h h''. \<lbrakk>\<And>h h''. \<lbrakk>h \<turnstile> iterate_M xs \<rightarrow>\<^sub>h h'; h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''\<rbrakk> \<Longrightarrow> h \<turnstile> iterate_M (xs @ ys) \<rightarrow>\<^sub>h h''; h \<turnstile> a \<bind> (\<lambda>_. iterate_M xs) \<rightarrow>\<^sub>h h'; h' \<turnstile> iterate_M ys \<rightarrow>\<^sub>h h''\<rbrakk> \<Longrightarrow> h \<turnstile> a \<bind> (\<lambda>_. iterate_M (xs @ ys)) \<rightarrow>\<^sub>h h''
[PROOF STEP]
by (meson bind_returns_heap_E bind_returns_heap_I)


[STATEMENT]
lemma card_sumset_geq1:
  assumes A: "A \<noteq> {}" "finite A" and B: "B \<noteq> {}" "finite B"
  shows "card(int.sumset A B) \<ge> (card A) + (card B) - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
finite A

goal (1 subgoal):
 1. card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
proof (induction "card A" arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
 2. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B); Suc x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = card ?A; ?A \<noteq> {}; finite ?A\<rbrakk> \<Longrightarrow> card ?A + card B - 1 \<le> card (int.sumset ?A B)
Suc n = card A
A \<noteq> {}
finite A

goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
 2. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B); Suc x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
define a where "a = Max A"
[PROOF STATE]
proof (state)
this:
a = Max A

goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
 2. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B); Suc x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
define A' where "A' \<equiv> A - {a}"
[PROOF STATE]
proof (state)
this:
A' \<equiv> A - {a}

goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
 2. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B); Suc x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A' \<equiv> A - {a}
[PROOF STEP]
obtain a: "a \<in> A" "A' = A - {a}" "finite A'" "a \<notin> A'" and A: "A = insert a A'"
[PROOF STATE]
proof (prove)
using this:
A' \<equiv> A - {a}

goal (1 subgoal):
 1. (\<lbrakk>a \<in> A; A' = A - {a}; finite A'; a \<notin> A'; A = insert a A'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Max_in Suc a_def
[PROOF STATE]
proof (prove)
using this:
A' \<equiv> A - {a}
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Max ?A \<in> ?A
\<lbrakk>n = card ?A; ?A \<noteq> {}; finite ?A\<rbrakk> \<Longrightarrow> card ?A + card B - 1 \<le> card (int.sumset ?A B)
Suc n = card A
A \<noteq> {}
finite A
a = Max A

goal (1 subgoal):
 1. (\<lbrakk>a \<in> A; A' = A - {a}; finite A'; a \<notin> A'; A = insert a A'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> A
A' = A - {a}
finite A'
a \<notin> A'
A = insert a A'

goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
 2. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B); Suc x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n = card ?A; ?A \<noteq> {}; finite ?A\<rbrakk> \<Longrightarrow> card ?A + card B - 1 \<le> card (int.sumset ?A B)
Suc n = card A
A \<noteq> {}
finite A
a \<in> A
A' = A - {a}
finite A'
a \<notin> A'
A = insert a A'
[PROOF STEP]
have n: "card A' = n"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = card ?A; ?A \<noteq> {}; finite ?A\<rbrakk> \<Longrightarrow> card ?A + card B - 1 \<le> card (int.sumset ?A B)
Suc n = card A
A \<noteq> {}
finite A
a \<in> A
A' = A - {a}
finite A'
a \<notin> A'
A = insert a A'

goal (1 subgoal):
 1. card A' = n
[PROOF STEP]
by (metis card_Diff_singleton diff_Suc_Suc minus_nat.diff_0 One_nat_def)
[PROOF STATE]
proof (state)
this:
card A' = n

goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
 2. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B); Suc x = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
proof (cases "A' = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A' = {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
 2. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A' = {}

goal (2 subgoals):
 1. A' = {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
 2. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A' = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A' = {}

goal (1 subgoal):
 1. card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
by (simp add: A B(2) int.card_sumset_singleton_eq int.sumset_commute)
[PROOF STATE]
proof (state)
this:
card A + card B - 1 \<le> card (int.sumset A B)

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A' \<noteq> {}

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
have "a + Max B \<notin> int.sumset A' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + Max B \<notin> int.sumset A' B
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. a + Max B \<notin> int.sumset A' B
[PROOF STEP]
by (smt (verit, best) DiffE Max_ge a a_def int.sumset.cases singleton_iff)
[PROOF STATE]
proof (state)
this:
a + Max B \<notin> int.sumset A' B

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a + Max B \<notin> int.sumset A' B
[PROOF STEP]
have *: "\<not> int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A' B"
[PROOF STATE]
proof (prove)
using this:
a + Max B \<notin> int.sumset A' B

goal (1 subgoal):
 1. \<not> int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A' B
[PROOF STEP]
using B Max_in
[PROOF STATE]
proof (prove)
using this:
a + Max B \<notin> int.sumset A' B
B \<noteq> {}
finite B
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Max ?A \<in> ?A

goal (1 subgoal):
 1. \<not> int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A' B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A' B

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
have "card A + card B - 1 \<le> Suc (card (int.sumset A' B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card A + card B - 1 \<le> Suc (card (int.sumset A' B))
[PROOF STEP]
using Suc False A a
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = card ?A; ?A \<noteq> {}; finite ?A\<rbrakk> \<Longrightarrow> card ?A + card B - 1 \<le> card (int.sumset ?A B)
Suc n = card A
A \<noteq> {}
finite A
A' \<noteq> {}
A = insert a A'
a \<in> A
A' = A - {a}
finite A'
a \<notin> A'

goal (1 subgoal):
 1. card A + card B - 1 \<le> Suc (card (int.sumset A' B))
[PROOF STEP]
using le_diff_conv
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = card ?A; ?A \<noteq> {}; finite ?A\<rbrakk> \<Longrightarrow> card ?A + card B - 1 \<le> card (int.sumset ?A B)
Suc n = card A
A \<noteq> {}
finite A
A' \<noteq> {}
A = insert a A'
a \<in> A
A' = A - {a}
finite A'
a \<notin> A'
(?j - ?k \<le> ?i) = (?j \<le> ?i + ?k)

goal (1 subgoal):
 1. card A + card B - 1 \<le> Suc (card (int.sumset A' B))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
card A + card B - 1 \<le> Suc (card (int.sumset A' B))

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card A + card B - 1 \<le> Suc (card (int.sumset A' B))

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
have "\<dots> \<le> card (int.sumset A' B \<union> (+) a ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card (int.sumset A' B)) \<le> card (int.sumset A' B \<union> (+) a ` B)
[PROOF STEP]
using a B
[PROOF STATE]
proof (prove)
using this:
a \<in> A
A' = A - {a}
finite A'
a \<notin> A'
B \<noteq> {}
finite B

goal (1 subgoal):
 1. Suc (card (int.sumset A' B)) \<le> card (int.sumset A' B \<union> (+) a ` B)
[PROOF STEP]
by (metis "*" card_seteq finite_Un finite_imageI int.finite_sumset not_less_eq_eq sup_ge1)
[PROOF STATE]
proof (state)
this:
Suc (card (int.sumset A' B)) \<le> card (int.sumset A' B \<union> (+) a ` B)

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (card (int.sumset A' B)) \<le> card (int.sumset A' B \<union> (+) a ` B)

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
have "\<dots> \<le> card (int.sumset A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (int.sumset A' B \<union> (+) a ` B) \<le> card (int.sumset A B)
[PROOF STEP]
proof (rule card_mono)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (int.sumset A B)
 2. int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A B
[PROOF STEP]
show "finite (int.sumset A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (int.sumset A B)
[PROOF STEP]
using B Suc.prems int.finite_sumset
[PROOF STATE]
proof (prove)
using this:
B \<noteq> {}
finite B
A \<noteq> {}
finite A
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (int.sumset ?A ?B)

goal (1 subgoal):
 1. finite (int.sumset A B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (int.sumset A B)

goal (1 subgoal):
 1. int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A B
[PROOF STEP]
show "int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A B
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A = insert a A'

goal (1 subgoal):
 1. int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A B
[PROOF STEP]
by (force simp: int.sumset)
[PROOF STATE]
proof (state)
this:
int.sumset A' B \<union> (+) a ` B \<subseteq> int.sumset A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (int.sumset A' B \<union> (+) a ` B) \<le> card (int.sumset A B)

goal (1 subgoal):
 1. A' \<noteq> {} \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card A + card B - 1 \<le> card (int.sumset A B)

goal (1 subgoal):
 1. card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card A + card B - 1 \<le> card (int.sumset A B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card A + card B - 1 \<le> card (int.sumset A B)

goal (1 subgoal):
 1. \<And>A. \<lbrakk>0 = card A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> card A + card B - 1 \<le> card (int.sumset A B)
[PROOF STEP]
qed auto


[STATEMENT]
lemma fun_type_inv_wf: assumes "\<Gamma> t = TComp f T" "wf\<^sub>t\<^sub>r\<^sub>m t" shows "arity f = length T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arity f = length T
[PROOF STEP]
using \<Gamma>_wf'[OF assms(2)] assms(1)
[PROOF STATE]
proof (prove)
using this:
wf\<^sub>t\<^sub>r\<^sub>m (\<Gamma> t)
\<Gamma> t = Fun f T

goal (1 subgoal):
 1. arity f = length T
[PROOF STEP]
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def
[PROOF STATE]
proof (prove)
using this:
\<forall>f T. Fun f T \<sqsubseteq> \<Gamma> t \<longrightarrow> length T = arity f
\<Gamma> t = Fun f T

goal (1 subgoal):
 1. arity f = length T
[PROOF STEP]
by auto


[STATEMENT]
lemma wt_subst_rm_vars: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<Longrightarrow> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<Longrightarrow> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \<delta>)
[PROOF STEP]
using rm_vars_dom
[PROOF STATE]
proof (prove)
using this:
subst_domain (rm_vars ?V ?s) = subst_domain ?s - ?V

goal (1 subgoal):
 1. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<Longrightarrow> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \<delta>)
[PROOF STEP]
unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
[PROOF STATE]
proof (prove)
using this:
subst_domain (rm_vars ?V ?s) = subst_domain ?s - ?V

goal (1 subgoal):
 1. \<forall>v. \<Gamma> (Var v) = \<Gamma> (\<delta> v) \<Longrightarrow> \<forall>v. \<Gamma> (Var v) = \<Gamma> (rm_vars X \<delta> v)
[PROOF STEP]
by auto


[STATEMENT]
lemma some_GB_pmdl_dgrad_p_set:
  assumes "dickson_grading d" and "finite (component_of_term ` Keys F)" and "F \<subseteq> dgrad_p_set d m"
  shows "pmdl (some_GB F) = pmdl F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (some_GB F) = pmdl F
[PROOF STEP]
using some_GB_props_dgrad_p_set[OF assms]
[PROOF STATE]
proof (prove)
using this:
finite (some_GB F) \<and> is_Groebner_basis (some_GB F) \<and> pmdl (some_GB F) = pmdl F

goal (1 subgoal):
 1. pmdl (some_GB F) = pmdl F
[PROOF STEP]
by (elim conjE)


[STATEMENT]
lemma coeff_0_interp_factorization:
  "coeff (interp_factorization fctrs) 0 = (0 :: 'a :: idom) \<longleftrightarrow>
     fst fctrs = 0 \<or> 0 \<in> fst ` set (snd fctrs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (coeff (interp_factorization fctrs) 0 = (0::'a)) = (fst fctrs = (0::'a) \<or> (0::'a) \<in> fst ` set (snd fctrs))
[PROOF STEP]
by (force simp: interp_factorization_def case_prod_unfold coeff_0_prod_list o_def
                  coeff_0_power prod_list_zero_iff simp del: power_Suc)


[STATEMENT]
lemma (in cyclic_group) elem_is_gen_pow:
  assumes "x \<in> carrier G"
  shows "\<exists>n :: int. x = gen [^] n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. x = gen [^] n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. x = gen [^] n
[PROOF STEP]
from generator
[PROOF STATE]
proof (chain)
picking this:
carrier G = generate G {gen}
[PROOF STEP]
have x_g:"x \<in> generate G {gen}"
[PROOF STATE]
proof (prove)
using this:
carrier G = generate G {gen}

goal (1 subgoal):
 1. x \<in> generate G {gen}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
carrier G = generate G {gen}
x \<in> carrier G

goal (1 subgoal):
 1. x \<in> generate G {gen}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<in> generate G {gen}

goal (1 subgoal):
 1. \<exists>n. x = gen [^] n
[PROOF STEP]
with generate_pow[of gen]
[PROOF STATE]
proof (chain)
picking this:
gen \<in> carrier G \<Longrightarrow> generate G {gen} = {gen [^] k |k. k \<in> UNIV}
x \<in> generate G {gen}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gen \<in> carrier G \<Longrightarrow> generate G {gen} = {gen [^] k |k. k \<in> UNIV}
x \<in> generate G {gen}

goal (1 subgoal):
 1. \<exists>n. x = gen [^] n
[PROOF STEP]
using gen_closed
[PROOF STATE]
proof (prove)
using this:
gen \<in> carrier G \<Longrightarrow> generate G {gen} = {gen [^] k |k. k \<in> UNIV}
x \<in> generate G {gen}
gen \<in> carrier G

goal (1 subgoal):
 1. \<exists>n. x = gen [^] n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. x = gen [^] n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma seq_decompose:
assumes "\<sigma> \<in> seq ars" and "labels \<sigma> = \<sigma>1'@\<sigma>2'"
shows "\<exists> \<sigma>1 \<sigma>2. ({\<sigma>1,\<sigma>2} \<subseteq> seq ars \<and> \<sigma> = (fst \<sigma>1,snd \<sigma>1@snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst \<sigma> \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> \<sigma> = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst \<sigma> \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> \<sigma> = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst \<sigma> \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
obtain s ss where \<sigma>_dec: "\<sigma> = (s,ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s ss. \<sigma> = (s, ss) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) surjective_pairing
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> seq ars
?t = (fst ?t, snd ?t)

goal (1 subgoal):
 1. (\<And>s ss. \<sigma> = (s, ss) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<sigma> = (s, ss)

goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> \<sigma> = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst \<sigma> \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> \<sigma> = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst \<sigma> \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> seq ars
labels \<sigma> = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> \<sigma> = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst \<sigma> \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
unfolding \<sigma>_dec
[PROOF STATE]
proof (prove)
using this:
(s, ss) \<in> seq ars
labels (s, ss) = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, ss) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, ss) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
proof (induct ss arbitrary: s \<sigma>1' \<sigma>2' rule:list.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, []) \<in> seq ars; labels (s, []) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, []) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, []) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<And>x1 x2 s \<sigma>1' \<sigma>2'. \<lbrakk>\<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, x2) \<in> seq ars; labels (s, x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'; (s, x1 # x2) \<in> seq ars; labels (s, x1 # x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x1 # x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x1 # x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
(s, []) \<in> seq ars
labels (s, []) = \<sigma>1' @ \<sigma>2'

goal (2 subgoals):
 1. \<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, []) \<in> seq ars; labels (s, []) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, []) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, []) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<And>x1 x2 s \<sigma>1' \<sigma>2'. \<lbrakk>\<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, x2) \<in> seq ars; labels (s, x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'; (s, x1 # x2) \<in> seq ars; labels (s, x1 # x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x1 # x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x1 # x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(s, []) \<in> seq ars
labels (s, []) = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, []) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, []) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
unfolding labels_def lst_def
[PROOF STATE]
proof (prove)
using this:
(s, []) \<in> seq ars
map fst (snd (s, [])) = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, []) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> (if snd \<sigma>1 = [] then fst \<sigma>1 else snd (last (snd \<sigma>1))) = fst \<sigma>2 \<and> (if snd \<sigma>2 = [] then fst \<sigma>2 else snd (last (snd \<sigma>2))) = (if snd (s, []) = [] then fst (s, []) else snd (last (snd (s, [])))) \<and> map fst (snd \<sigma>1) = \<sigma>1' \<and> map fst (snd \<sigma>2) = \<sigma>2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, []) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, []) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. \<And>x1 x2 s \<sigma>1' \<sigma>2'. \<lbrakk>\<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, x2) \<in> seq ars; labels (s, x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'; (s, x1 # x2) \<in> seq ars; labels (s, x1 # x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x1 # x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x1 # x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 s \<sigma>1' \<sigma>2'. \<lbrakk>\<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, x2) \<in> seq ars; labels (s, x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'; (s, x1 # x2) \<in> seq ars; labels (s, x1 # x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x1 # x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x1 # x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?s, xs) \<in> seq ars; labels (?s, xs) = ?\<sigma>1' @ ?\<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (?s, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (?s, xs) \<and> labels \<sigma>1 = ?\<sigma>1' \<and> labels \<sigma>2 = ?\<sigma>2'
(s, x # xs) \<in> seq ars
labels (s, x # xs) = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. \<And>x1 x2 s \<sigma>1' \<sigma>2'. \<lbrakk>\<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, x2) \<in> seq ars; labels (s, x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'; (s, x1 # x2) \<in> seq ars; labels (s, x1 # x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x1 # x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x1 # x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have step: "(s,x) \<in> ars" and x:"(snd x,xs) \<in> seq ars"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, x) \<in> ars &&& (snd x, xs) \<in> seq ars
[PROOF STEP]
using seq_tail1[OF Cons(2)] surjective_pairing
[PROOF STATE]
proof (prove)
using this:
(snd x, xs) \<in> seq ars
(s, fst x, snd x) \<in> ars
lst (s, x # xs) = lst (snd x, xs)
?t = (fst ?t, snd ?t)

goal (1 subgoal):
 1. (s, x) \<in> ars &&& (snd x, xs) \<in> seq ars
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s, x) \<in> ars
(snd x, xs) \<in> seq ars

goal (1 subgoal):
 1. \<And>x1 x2 s \<sigma>1' \<sigma>2'. \<lbrakk>\<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, x2) \<in> seq ars; labels (s, x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'; (s, x1 # x2) \<in> seq ars; labels (s, x1 # x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x1 # x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x1 # x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
hence steps: "(s,[x]) \<in> seq ars"
[PROOF STATE]
proof (prove)
using this:
(s, x) \<in> ars
(snd x, xs) \<in> seq ars

goal (1 subgoal):
 1. (s, [x]) \<in> seq ars
[PROOF STEP]
by (metis Cons(2) append_Cons append_Nil seq_chop(1))
[PROOF STATE]
proof (state)
this:
(s, [x]) \<in> seq ars

goal (1 subgoal):
 1. \<And>x1 x2 s \<sigma>1' \<sigma>2'. \<lbrakk>\<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, x2) \<in> seq ars; labels (s, x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'; (s, x1 # x2) \<in> seq ars; labels (s, x1 # x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x1 # x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x1 # x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
from Cons(3)
[PROOF STATE]
proof (chain)
picking this:
labels (s, x # xs) = \<sigma>1' @ \<sigma>2'
[PROOF STEP]
have a:"fst x#labels (snd x,xs) = \<sigma>1'@\<sigma>2'"
[PROOF STATE]
proof (prove)
using this:
labels (s, x # xs) = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. fst x # labels (snd x, xs) = \<sigma>1' @ \<sigma>2'
[PROOF STEP]
unfolding labels_def snd_conv
[PROOF STATE]
proof (prove)
using this:
map fst (x # xs) = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. fst x # map fst xs = \<sigma>1' @ \<sigma>2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst x # labels (snd x, xs) = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. \<And>x1 x2 s \<sigma>1' \<sigma>2'. \<lbrakk>\<And>s \<sigma>1' \<sigma>2'. \<lbrakk>(s, x2) \<in> seq ars; labels (s, x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'; (s, x1 # x2) \<in> seq ars; labels (s, x1 # x2) = \<sigma>1' @ \<sigma>2'\<rbrakk> \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x1 # x2) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x1 # x2) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
proof (cases "\<sigma>1'=[]")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<sigma>1' = []

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
from a True
[PROOF STATE]
proof (chain)
picking this:
fst x # labels (snd x, xs) = \<sigma>1' @ \<sigma>2'
\<sigma>1' = []
[PROOF STEP]
obtain l ls where \<sigma>2'_dec: "\<sigma>2' = l#ls" and y1:"fst x = l" and y2:"labels (snd x,xs) = []@ls"
[PROOF STATE]
proof (prove)
using this:
fst x # labels (snd x, xs) = \<sigma>1' @ \<sigma>2'
\<sigma>1' = []

goal (1 subgoal):
 1. (\<And>l ls. \<lbrakk>\<sigma>2' = l # ls; fst x = l; labels (snd x, xs) = [] @ ls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>2' = l # ls
fst x = l
labels (snd x, xs) = [] @ ls

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
obtain \<sigma>1 \<sigma>2 where ih: "\<sigma>1 \<in> seq ars" "\<sigma>2 \<in> seq ars" "(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)" "lst \<sigma>1 = fst \<sigma>2"
    "labels \<sigma>1 = []" "labels \<sigma>2 = ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma>1 \<sigma>2. \<lbrakk>\<sigma>1 \<in> seq ars; \<sigma>2 \<in> seq ars; (snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2); lst \<sigma>1 = fst \<sigma>2; labels \<sigma>1 = []; labels \<sigma>2 = ls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons(1)[OF x y2]
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (snd x, xs) \<and> labels \<sigma>1 = [] \<and> labels \<sigma>2 = ls

goal (1 subgoal):
 1. (\<And>\<sigma>1 \<sigma>2. \<lbrakk>\<sigma>1 \<in> seq ars; \<sigma>2 \<in> seq ars; (snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2); lst \<sigma>1 = fst \<sigma>2; labels \<sigma>1 = []; labels \<sigma>2 = ls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
labels \<sigma>1 = []
labels \<sigma>2 = ls

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
hence c:"fst (snd x,xs) = fst \<sigma>1"
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
labels \<sigma>1 = []
labels \<sigma>2 = ls

goal (1 subgoal):
 1. fst (snd x, xs) = fst \<sigma>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (snd x, xs) = fst \<sigma>1

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have 1: "\<sigma>1 = (snd x,[])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>1 = (snd x, [])
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
labels \<sigma>1 = []
labels \<sigma>2 = ls

goal (1 subgoal):
 1. \<sigma>1 = (snd x, [])
[PROOF STEP]
unfolding labels_def
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
map fst (snd \<sigma>1) = []
map fst (snd \<sigma>2) = ls

goal (1 subgoal):
 1. \<sigma>1 = (snd x, [])
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<sigma>1 \<in> seq ars; \<sigma>2 \<in> seq ars; lst \<sigma>1 = fst \<sigma>2; snd \<sigma>1 = []; ls = map fst (snd \<sigma>2); snd x = fst \<sigma>1; xs = snd \<sigma>2\<rbrakk> \<Longrightarrow> \<sigma>1 = (fst \<sigma>1, [])
[PROOF STEP]
by (metis surjective_pairing)
[PROOF STATE]
proof (state)
this:
\<sigma>1 = (snd x, [])

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
hence 2: "snd x = fst \<sigma>1" "xs = snd \<sigma>2"
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 = (snd x, [])

goal (1 subgoal):
 1. snd x = fst \<sigma>1 &&& xs = snd \<sigma>2
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 = (snd x, [])
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
labels \<sigma>1 = []
labels \<sigma>2 = ls

goal (1 subgoal):
 1. snd x = fst \<sigma>1 &&& xs = snd \<sigma>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd x = fst \<sigma>1
xs = snd \<sigma>2

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have 3: "snd x = fst \<sigma>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd x = fst \<sigma>2
[PROOF STEP]
using ih 1
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
labels \<sigma>1 = []
labels \<sigma>2 = ls
\<sigma>1 = (snd x, [])

goal (1 subgoal):
 1. snd x = fst \<sigma>2
[PROOF STEP]
unfolding lst_def
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
(if snd \<sigma>1 = [] then fst \<sigma>1 else snd (last (snd \<sigma>1))) = fst \<sigma>2
labels \<sigma>1 = []
labels \<sigma>2 = ls
\<sigma>1 = (snd x, [])

goal (1 subgoal):
 1. snd x = fst \<sigma>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd x = fst \<sigma>2

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "\<sigma>2 = (snd x,xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>2 = (snd x, xs)
[PROOF STEP]
using x 1 2 3 surjective_pairing
[PROOF STATE]
proof (prove)
using this:
(snd x, xs) \<in> seq ars
\<sigma>1 = (snd x, [])
snd x = fst \<sigma>1
xs = snd \<sigma>2
snd x = fst \<sigma>2
?t = (fst ?t, snd ?t)

goal (1 subgoal):
 1. \<sigma>2 = (snd x, xs)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<sigma>2 = (snd x, xs)

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
hence l:"lst (s, [x]) = fst \<sigma>2"
[PROOF STATE]
proof (prove)
using this:
\<sigma>2 = (snd x, xs)

goal (1 subgoal):
 1. lst (s, [x]) = fst \<sigma>2
[PROOF STEP]
unfolding lst_def
[PROOF STATE]
proof (prove)
using this:
\<sigma>2 = (snd x, xs)

goal (1 subgoal):
 1. (if snd (s, [x]) = [] then fst (s, [x]) else snd (last (snd (s, [x])))) = fst \<sigma>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lst (s, [x]) = fst \<sigma>2

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have m:"{(s,[]), (s,x# snd \<sigma>2)} \<subseteq> seq ars"  (is "{?\<sigma>1,?\<sigma>2} \<subseteq> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars
[PROOF STEP]
using seq.intros(1) seq_concat(1)[OF steps _ l] ih
[PROOF STATE]
proof (prove)
using this:
(?a, []) \<in> seq ?ars
\<sigma>2 \<in> seq ars \<Longrightarrow> (fst (s, [x]), snd (s, [x]) @ snd \<sigma>2) \<in> seq ars
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
labels \<sigma>1 = []
labels \<sigma>2 = ls

goal (1 subgoal):
 1. {(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "(s, x # xs) = (fst ?\<sigma>1, snd ?\<sigma>1 @ snd ?\<sigma>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, x # xs) = (fst (s, []), snd (s, []) @ snd (s, x # snd \<sigma>2))
[PROOF STEP]
using m 2
[PROOF STATE]
proof (prove)
using this:
{(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars
snd x = fst \<sigma>1
xs = snd \<sigma>2

goal (1 subgoal):
 1. (s, x # xs) = (fst (s, []), snd (s, []) @ snd (s, x # snd \<sigma>2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s, x # xs) = (fst (s, []), snd (s, []) @ snd (s, x # snd \<sigma>2))

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(s, x # xs) = (fst (s, []), snd (s, []) @ snd (s, x # snd \<sigma>2))

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "lst ?\<sigma>1 = fst ?\<sigma>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lst (s, []) = fst (s, x # snd \<sigma>2)
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
{(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars

goal (1 subgoal):
 1. lst (s, []) = fst (s, x # snd \<sigma>2)
[PROOF STEP]
unfolding lst_def
[PROOF STATE]
proof (prove)
using this:
{(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars

goal (1 subgoal):
 1. (if snd (s, []) = [] then fst (s, []) else snd (last (snd (s, [])))) = fst (s, x # snd \<sigma>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lst (s, []) = fst (s, x # snd \<sigma>2)

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lst (s, []) = fst (s, x # snd \<sigma>2)

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "lst ?\<sigma>2 = lst (s,x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lst (s, x # snd \<sigma>2) = lst (s, x # xs)
[PROOF STEP]
unfolding lst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if snd (s, x # snd \<sigma>2) = [] then fst (s, x # snd \<sigma>2) else snd (last (snd (s, x # snd \<sigma>2)))) = (if snd (s, x # xs) = [] then fst (s, x # xs) else snd (last (snd (s, x # xs))))
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
snd x = fst \<sigma>1
xs = snd \<sigma>2
snd x = fst \<sigma>2

goal (1 subgoal):
 1. (if snd (s, x # snd \<sigma>2) = [] then fst (s, x # snd \<sigma>2) else snd (last (snd (s, x # snd \<sigma>2)))) = (if snd (s, x # xs) = [] then fst (s, x # xs) else snd (last (snd (s, x # xs))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lst (s, x # snd \<sigma>2) = lst (s, x # xs)

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lst (s, x # snd \<sigma>2) = lst (s, x # xs)

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "labels (s,[]) = \<sigma>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. labels (s, []) = \<sigma>1'
[PROOF STEP]
unfolding labels_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (snd (s, [])) = \<sigma>1'
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
\<sigma>1' = []

goal (1 subgoal):
 1. map fst (snd (s, [])) = \<sigma>1'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
labels (s, []) = \<sigma>1'

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
labels (s, []) = \<sigma>1'

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "labels ?\<sigma>2 = \<sigma>2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. labels (s, x # snd \<sigma>2) = \<sigma>2'
[PROOF STEP]
using ih y1
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
labels \<sigma>1 = []
labels \<sigma>2 = ls
fst x = l

goal (1 subgoal):
 1. labels (s, x # snd \<sigma>2) = \<sigma>2'
[PROOF STEP]
unfolding \<sigma>2'_dec labels_def
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
map fst (snd \<sigma>1) = []
map fst (snd \<sigma>2) = ls
fst x = l

goal (1 subgoal):
 1. map fst (snd (s, x # snd \<sigma>2)) = l # ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
labels (s, x # snd \<sigma>2) = \<sigma>2'

goal (2 subgoals):
 1. \<sigma>1' = [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
 2. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars
(s, x # xs) = (fst (s, []), snd (s, []) @ snd (s, x # snd \<sigma>2))
lst (s, []) = fst (s, x # snd \<sigma>2)
lst (s, x # snd \<sigma>2) = lst (s, x # xs)
labels (s, []) = \<sigma>1'
labels (s, x # snd \<sigma>2) = \<sigma>2'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{(s, []), (s, x # snd \<sigma>2)} \<subseteq> seq ars
(s, x # xs) = (fst (s, []), snd (s, []) @ snd (s, x # snd \<sigma>2))
lst (s, []) = fst (s, x # snd \<sigma>2)
lst (s, x # snd \<sigma>2) = lst (s, x # xs)
labels (s, []) = \<sigma>1'
labels (s, x # snd \<sigma>2) = \<sigma>2'

goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<sigma>1' \<noteq> []

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<sigma>1' \<noteq> []
[PROOF STEP]
obtain l ls where \<sigma>1'_dec:"\<sigma>1' = l#ls"
[PROOF STATE]
proof (prove)
using this:
\<sigma>1' \<noteq> []

goal (1 subgoal):
 1. (\<And>l ls. \<sigma>1' = l # ls \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using list.exhaust
[PROOF STATE]
proof (prove)
using this:
\<sigma>1' \<noteq> []
\<lbrakk>?y = [] \<Longrightarrow> ?P; \<And>x21 x22. ?y = x21 # x22 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>l ls. \<sigma>1' = l # ls \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>1' = l # ls

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
hence y1:"fst x = l" and y2:"labels (snd x,xs) = ls @ \<sigma>2'"
[PROOF STATE]
proof (prove)
using this:
\<sigma>1' = l # ls

goal (1 subgoal):
 1. fst x = l &&& labels (snd x, xs) = ls @ \<sigma>2'
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<sigma>1' = l # ls
fst x # labels (snd x, xs) = \<sigma>1' @ \<sigma>2'

goal (1 subgoal):
 1. fst x = l &&& labels (snd x, xs) = ls @ \<sigma>2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst x = l
labels (snd x, xs) = ls @ \<sigma>2'

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
obtain \<sigma>1 \<sigma>2 where ih: "\<sigma>1 \<in> seq ars" "\<sigma>2 \<in> seq ars" "(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)"
    "lst \<sigma>1 = fst \<sigma>2" "lst \<sigma>2 = lst (snd x, xs)" "labels \<sigma>1 = ls" "labels \<sigma>2 = \<sigma>2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma>1 \<sigma>2. \<lbrakk>\<sigma>1 \<in> seq ars; \<sigma>2 \<in> seq ars; (snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2); lst \<sigma>1 = fst \<sigma>2; lst \<sigma>2 = lst (snd x, xs); labels \<sigma>1 = ls; labels \<sigma>2 = \<sigma>2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  Cons(1)[OF x y2]
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (snd x, xs) \<and> labels \<sigma>1 = ls \<and> labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. (\<And>\<sigma>1 \<sigma>2. \<lbrakk>\<sigma>1 \<in> seq ars; \<sigma>2 \<in> seq ars; (snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2); lst \<sigma>1 = fst \<sigma>2; lst \<sigma>2 = lst (snd x, xs); labels \<sigma>1 = ls; labels \<sigma>2 = \<sigma>2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
hence "{(s,x# snd \<sigma>1),\<sigma>2} \<subseteq> seq ars" (is "{?\<sigma>1,_} \<subseteq> seq ars")
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. {(s, x # snd \<sigma>1), \<sigma>2} \<subseteq> seq ars
[PROOF STEP]
using seq_concat(1)[OF steps] ih
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'
\<lbrakk>?ss2.0 \<in> seq ars; lst (s, [x]) = fst ?ss2.0\<rbrakk> \<Longrightarrow> (fst (s, [x]), snd (s, [x]) @ snd ?ss2.0) \<in> seq ars
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. {(s, x # snd \<sigma>1), \<sigma>2} \<subseteq> seq ars
[PROOF STEP]
unfolding lst_def
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
(if snd \<sigma>1 = [] then fst \<sigma>1 else snd (last (snd \<sigma>1))) = fst \<sigma>2
(if snd \<sigma>2 = [] then fst \<sigma>2 else snd (last (snd \<sigma>2))) = (if snd (snd x, xs) = [] then fst (snd x, xs) else snd (last (snd (snd x, xs))))
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'
\<lbrakk>?ss2.0 \<in> seq ars; (if snd (s, [x]) = [] then fst (s, [x]) else snd (last (snd (s, [x])))) = fst ?ss2.0\<rbrakk> \<Longrightarrow> (fst (s, [x]), snd (s, [x]) @ snd ?ss2.0) \<in> seq ars
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
(if snd \<sigma>1 = [] then fst \<sigma>1 else snd (last (snd \<sigma>1))) = fst \<sigma>2
(if snd \<sigma>2 = [] then fst \<sigma>2 else snd (last (snd \<sigma>2))) = (if snd (snd x, xs) = [] then fst (snd x, xs) else snd (last (snd (snd x, xs))))
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. {(s, x # snd \<sigma>1), \<sigma>2} \<subseteq> seq ars
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(s, x # snd \<sigma>1), \<sigma>2} \<subseteq> seq ars

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(s, x # snd \<sigma>1), \<sigma>2} \<subseteq> seq ars

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "(s,x#xs) = (fst ?\<sigma>1,snd ?\<sigma>1@snd \<sigma>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, x # xs) = (fst (s, x # snd \<sigma>1), snd (s, x # snd \<sigma>1) @ snd \<sigma>2)
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. (s, x # xs) = (fst (s, x # snd \<sigma>1), snd (s, x # snd \<sigma>1) @ snd \<sigma>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s, x # xs) = (fst (s, x # snd \<sigma>1), snd (s, x # snd \<sigma>1) @ snd \<sigma>2)

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(s, x # xs) = (fst (s, x # snd \<sigma>1), snd (s, x # snd \<sigma>1) @ snd \<sigma>2)

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "lst ?\<sigma>1 = fst \<sigma>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lst (s, x # snd \<sigma>1) = fst \<sigma>2
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. lst (s, x # snd \<sigma>1) = fst \<sigma>2
[PROOF STEP]
unfolding lst_def
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
(if snd \<sigma>1 = [] then fst \<sigma>1 else snd (last (snd \<sigma>1))) = fst \<sigma>2
(if snd \<sigma>2 = [] then fst \<sigma>2 else snd (last (snd \<sigma>2))) = (if snd (snd x, xs) = [] then fst (snd x, xs) else snd (last (snd (snd x, xs))))
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. (if snd (s, x # snd \<sigma>1) = [] then fst (s, x # snd \<sigma>1) else snd (last (snd (s, x # snd \<sigma>1)))) = fst \<sigma>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lst (s, x # snd \<sigma>1) = fst \<sigma>2

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lst (s, x # snd \<sigma>1) = fst \<sigma>2

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "lst \<sigma>2 = lst (s, x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lst \<sigma>2 = lst (s, x # xs)
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. lst \<sigma>2 = lst (s, x # xs)
[PROOF STEP]
unfolding lst_def
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
(if snd \<sigma>1 = [] then fst \<sigma>1 else snd (last (snd \<sigma>1))) = fst \<sigma>2
(if snd \<sigma>2 = [] then fst \<sigma>2 else snd (last (snd \<sigma>2))) = (if snd (snd x, xs) = [] then fst (snd x, xs) else snd (last (snd (snd x, xs))))
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. (if snd \<sigma>2 = [] then fst \<sigma>2 else snd (last (snd \<sigma>2))) = (if snd (s, x # xs) = [] then fst (s, x # xs) else snd (last (snd (s, x # xs))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lst \<sigma>2 = lst (s, x # xs)

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lst \<sigma>2 = lst (s, x # xs)

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "labels ?\<sigma>1 = \<sigma>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. labels (s, x # snd \<sigma>1) = \<sigma>1'
[PROOF STEP]
using ih \<sigma>1'_dec y1
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'
\<sigma>1' = l # ls
fst x = l

goal (1 subgoal):
 1. labels (s, x # snd \<sigma>1) = \<sigma>1'
[PROOF STEP]
unfolding labels_def
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
map fst (snd \<sigma>1) = ls
map fst (snd \<sigma>2) = \<sigma>2'
\<sigma>1' = l # ls
fst x = l

goal (1 subgoal):
 1. map fst (snd (s, x # snd \<sigma>1)) = \<sigma>1'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
labels (s, x # snd \<sigma>1) = \<sigma>1'

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
labels (s, x # snd \<sigma>1) = \<sigma>1'

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
have "labels \<sigma>2 = \<sigma>2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 \<in> seq ars
\<sigma>2 \<in> seq ars
(snd x, xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2)
lst \<sigma>1 = fst \<sigma>2
lst \<sigma>2 = lst (snd x, xs)
labels \<sigma>1 = ls
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. \<sigma>1' \<noteq> [] \<Longrightarrow> \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(s, x # snd \<sigma>1), \<sigma>2} \<subseteq> seq ars
(s, x # xs) = (fst (s, x # snd \<sigma>1), snd (s, x # snd \<sigma>1) @ snd \<sigma>2)
lst (s, x # snd \<sigma>1) = fst \<sigma>2
lst \<sigma>2 = lst (s, x # xs)
labels (s, x # snd \<sigma>1) = \<sigma>1'
labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{(s, x # snd \<sigma>1), \<sigma>2} \<subseteq> seq ars
(s, x # xs) = (fst (s, x # snd \<sigma>1), snd (s, x # snd \<sigma>1) @ snd \<sigma>2)
lst (s, x # snd \<sigma>1) = fst \<sigma>2
lst \<sigma>2 = lst (s, x # xs)
labels (s, x # snd \<sigma>1) = \<sigma>1'
labels \<sigma>2 = \<sigma>2'

goal (1 subgoal):
 1. \<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> (s, x # xs) = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst (s, x # xs) \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>1 \<sigma>2. {\<sigma>1, \<sigma>2} \<subseteq> seq ars \<and> \<sigma> = (fst \<sigma>1, snd \<sigma>1 @ snd \<sigma>2) \<and> lst \<sigma>1 = fst \<sigma>2 \<and> lst \<sigma>2 = lst \<sigma> \<and> labels \<sigma>1 = \<sigma>1' \<and> labels \<sigma>2 = \<sigma>2'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_cong[fundef_cong]:
  assumes "b s = b' s"
    and "b' s \<Longrightarrow> m1 s = m1' s"
    and "\<And>s'. s' = s \<Longrightarrow> \<not> b' s' \<Longrightarrow> m2 s' = m2' s'"
  shows "(condition b m1 m2) s = (condition b' m1' m2') s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. condition b
  m1
  m2 s = condition b'
  m1'
  m2' s
[PROOF STEP]
by (simp add: assms(1) assms(2) assms(3))


[STATEMENT]
lemma spmf_fast_uniform_ub:
  "spmf fast_uniform x \<le> (if x < n then 1 / n else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf local.fast_uniform x \<le> (if x < n then 1 / real n else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spmf local.fast_uniform x \<le> (if x < n then 1 / real n else 0)
[PROOF STEP]
have "{..<Suc 0} = {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..<Suc 0} = {0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{..<Suc 0} = {0}

goal (1 subgoal):
 1. spmf local.fast_uniform x \<le> (if x < n then 1 / real n else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{..<Suc 0} = {0}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{..<Suc 0} = {0}

goal (1 subgoal):
 1. spmf local.fast_uniform x \<le> (if x < n then 1 / real n else 0)
[PROOF STEP]
using spmf_fast_dice_roll_ub[of 1 x]
[PROOF STATE]
proof (prove)
using this:
{..<Suc 0} = {0}
0 < 1 \<Longrightarrow> spmf (pmf_of_set {..<1} \<bind> local.fast_dice_roll 1) x \<le> (if x < n then 1 / real n else 0)

goal (1 subgoal):
 1. spmf local.fast_uniform x \<le> (if x < n then 1 / real n else 0)
[PROOF STEP]
by(simp add: fast_uniform_def pmf_of_set_singleton bind_return_pmf split: if_split_asm)
[PROOF STATE]
proof (state)
this:
spmf local.fast_uniform x \<le> (if x < n then 1 / real n else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_range_map_Some:
  shows "v \<in> set abs_ast_variable_section \<Longrightarrow>
            (abs_range_map v) = Some [0..<length (snd (snd (astDom ! v)))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> set abs_ast_variable_section \<Longrightarrow> abs_range_map v = Some [0..<length (snd (snd (astDom ! v)))]
[PROOF STEP]
by (simp add: numVars_def abs_range_map_def o_def abs_ast_variable_section_def map_of_zip_map_Some)


[STATEMENT]
lemma right_total_MM_Rel[transfer_rule]: "right_total MM_Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_total MM_Rel
[PROOF STEP]
unfolding right_total_def MM_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. \<exists>x. local.mat_mod x = to_int_mat y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. local.mat_mod x = to_int_mat y
[PROOF STEP]
fix M :: "'a mod_ring mat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. local.mat_mod x = to_int_mat y
[PROOF STEP]
show "\<exists>x. mat_mod x = to_int_mat M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. local.mat_mod x = to_int_mat M
[PROOF STEP]
by (intro exI[of _ "to_int_mat M"], simp add: mat_mod_to_int_mat)
[PROOF STATE]
proof (state)
this:
\<exists>x. local.mat_mod x = to_int_mat M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_rcat_read_bytes_enclosed:
  fixes w :: "'b::len word"
  assumes "LENGTH('b) \<le> 2^LENGTH('a)"
    and "unat offset + si \<le> 2^LENGTH('a)"
  shows "word_rcat (read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) = \<langle>unat offset * 8,(unat offset + si) * 8\<rangle>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rcat (local.read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) = \<langle>unat offset * 8,(unat offset + si) * 8\<rangle>w
[PROOF STEP]
apply (rule word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size (word_rcat (local.read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si)) \<longrightarrow> word_rcat (local.read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) !! n = (\<langle>unat offset * 8,(unat offset + si) * 8\<rangle>w) !! n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
LENGTH('b) \<le> 2 ^ LENGTH('a)
unat offset + si \<le> 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<And>n. n < size (word_rcat (local.read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si)) \<longrightarrow> word_rcat (local.read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) !! n = (\<langle>unat offset * 8,(unat offset + si) * 8\<rangle>w) !! n
[PROOF STEP]
apply (auto simp add: test_bit_rcat word_size length_read_bytes rev_nth nth_read_bytes unat_of_nat nth_takebyte unat_word_ariths )
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>LENGTH('b) \<le> 2 ^ LENGTH('a); unat offset + si \<le> 2 ^ LENGTH('a); n < LENGTH('b); n div 8 < si; take_byte (unat offset + n div 8) w !! (n mod 8)\<rbrakk> \<Longrightarrow> (\<langle>unat offset * 8,unat offset * 8 + si * 8\<rangle>w) !! n
 2. \<And>n. \<lbrakk>LENGTH('b) \<le> 2 ^ LENGTH('a); unat offset + si \<le> 2 ^ LENGTH('a); n < LENGTH('b); (\<langle>unat offset * 8,unat offset * 8 + si * 8\<rangle>w) !! n\<rbrakk> \<Longrightarrow> n div 8 < si
 3. \<And>n. \<lbrakk>LENGTH('b) \<le> 2 ^ LENGTH('a); unat offset + si \<le> 2 ^ LENGTH('a); n < LENGTH('b); (\<langle>unat offset * 8,unat offset * 8 + si * 8\<rangle>w) !! n\<rbrakk> \<Longrightarrow> rev (local.read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) ! (n div 8) !! (n mod 8)
[PROOF STEP]
apply (auto simp add: take_byte_def nth_ucast nth_takebits take_bit_eq_mod split: if_split_asm)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>LENGTH('b) \<le> 2 ^ LENGTH('a); unat offset + si \<le> 2 ^ LENGTH('a); n < LENGTH('b); (\<langle>unat offset * 8,unat offset * 8 + si * 8\<rangle>w) !! n\<rbrakk> \<Longrightarrow> n div 8 < si
 2. \<And>n. \<lbrakk>LENGTH('b) \<le> 2 ^ LENGTH('a); unat offset + si \<le> 2 ^ LENGTH('a); n < LENGTH('b); (\<langle>unat offset * 8,unat offset * 8 + si * 8\<rangle>w) !! n\<rbrakk> \<Longrightarrow> rev (local.read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) ! (n div 8) !! (n mod 8)
[PROOF STEP]
apply (auto simp add: nth_takebits split: if_split_asm)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>LENGTH('b) \<le> 2 ^ LENGTH('a); unat offset + si \<le> 2 ^ LENGTH('a); n < LENGTH('b); (\<langle>unat offset * 8,unat offset * 8 + si * 8\<rangle>w) !! n\<rbrakk> \<Longrightarrow> rev (local.read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) ! (n div 8) !! (n mod 8)
[PROOF STEP]
apply (auto simp add: take_byte_def nth_ucast nth_takebits split: if_split_asm)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>LENGTH('b) \<le> 2 ^ LENGTH('a); unat offset + si \<le> 2 ^ LENGTH('a); n < LENGTH('b); n < si * 8; w !! (n + unat offset * 8)\<rbrakk> \<Longrightarrow> rev (local.read_bytes (\<lambda>a'. ucast (\<langle>unat (a' - a) * 8,unat (a' - a) * 8 + 8\<rangle>w)) (a + offset) si) ! (n div 8) !! (n mod 8)
[PROOF STEP]
by (auto simp add: rev_nth length_read_bytes take_byte_def nth_ucast nth_takebits nth_read_bytes unat_word_ariths unat_of_nat take_bit_eq_mod split: if_split_asm)


[STATEMENT]
lemma Load_correct:
"\<lbrakk> wf_prog wt P;
    P \<turnstile> C sees M:Ts\<rightarrow>T=(mxs,mxl\<^sub>0,ins,xt) in C;
    ins!pc = Load idx;
    P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: \<Phi> C M;
    Some \<sigma>' = exec (P, None, h, (stk,loc,C,M,pc)#frs);
    P,\<Phi> \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> P,\<Phi> \<turnstile> \<sigma>'\<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wt P; P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, ins, xt) in C; ins ! pc = Load idx; P,T,mxs,length ins,xt \<turnstile> ins ! pc,pc :: \<Phi> C M; \<lfloor>\<sigma>'\<rfloor> = exec (P, None, h, (stk, loc, C, M, pc) # frs); P,\<Phi> |- (None, h, (stk, loc, C, M, pc) # frs) [ok]\<rbrakk> \<Longrightarrow> P,\<Phi> |- \<sigma>' [ok]
[PROOF STEP]
by (fastforce dest: sees_method_fun [of _ C] elim!: confTs_confT_sup)


[STATEMENT]
lemma Pop_correct:
"\<lbrakk> wf_prog wt P;
  P \<turnstile> C sees M:Ts\<rightarrow>T=(mxs,mxl\<^sub>0,ins,xt) in C;
  ins ! pc = Pop;
  P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: \<Phi> C M;
  Some \<sigma>' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ;
  P,\<Phi> \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> P,\<Phi> \<turnstile> \<sigma>'\<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wt P; P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, ins, xt) in C; ins ! pc = Pop; P,T,mxs,length ins,xt \<turnstile> ins ! pc,pc :: \<Phi> C M; \<lfloor>\<sigma>'\<rfloor> = exec (P, None, h, (stk, loc, C, M, pc) # frs); P,\<Phi> |- (None, h, (stk, loc, C, M, pc) # frs) [ok]\<rbrakk> \<Longrightarrow> P,\<Phi> |- \<sigma>' [ok]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wt P; P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, ins, xt) in C; ins ! pc = Pop; P,T,mxs,length ins,xt \<turnstile> ins ! pc,pc :: \<Phi> C M; \<lfloor>\<sigma>'\<rfloor> = exec (P, None, h, (stk, loc, C, M, pc) # frs); P,\<Phi> |- (None, h, (stk, loc, C, M, pc) # frs) [ok]\<rbrakk> \<Longrightarrow> P,\<Phi> |- \<sigma>' [ok]
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Tsa Ta mxsa mxl\<^sub>0' is xta ts ST LT z zs ab bb. \<lbrakk>\<sigma>' = (None, h, (zs, loc, C, M, Suc pc) # frs); wf_prog wt P; P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, ins, xt) in C; ins ! pc = Pop; P \<turnstile> h \<surd>; P \<turnstile> C sees M: Tsa\<rightarrow>Ta = (mxsa, mxl\<^sub>0', is, xta) in C; \<Phi> C M ! pc = \<lfloor>(ts # ST, LT)\<rfloor>; P,h \<turnstile> loc [:\<le>\<^sub>\<top>] LT; pc < length is; conf_fs P h \<Phi> M (length Tsa) Ta frs; \<forall>x\<in>set (relevant_entries P Pop pc xt). case x of (f, t, C, ab) \<Rightarrow> is_class P C \<and> (case ab of (h, d) \<Rightarrow> d \<le> Suc (length ST) \<and> d < mxs); Suc pc < length ins; stk = z # zs; \<forall>x\<in>set (xcpt_eff Pop P pc (ts # ST, LT) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < length ins; P,h \<turnstile> z :\<le> ts; P,h \<turnstile> zs [:\<le>] ST; \<forall>x\<in>set (xcpt_eff Pop P pc (ts # ST, LT) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' \<Phi> C M ! pc'; \<Phi> C M ! Suc pc = \<lfloor>(ab, bb)\<rfloor>; P \<turnstile> ST [\<le>] ab; P \<turnstile> LT [\<le>\<^sub>\<top>] bb\<rbrakk> \<Longrightarrow> \<exists>Ts T mxs mxl\<^sub>0 is. (\<exists>xt. P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C) \<and> P,h \<turnstile> zs [:\<le>] ab \<and> P,h \<turnstile> loc [:\<le>\<^sub>\<top>] bb \<and> Suc pc < length is \<and> conf_fs P h \<Phi> M (length Ts) T frs
[PROOF STEP]
apply (drule (1) sees_method_fun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Tsa Ta mxsa mxl\<^sub>0' is xta ts ST LT z zs ab bb. \<lbrakk>\<sigma>' = (None, h, (zs, loc, C, M, Suc pc) # frs); wf_prog wt P; ins ! pc = Pop; P \<turnstile> h \<surd>; P \<turnstile> C sees M: Tsa\<rightarrow>Ta = (mxsa, mxl\<^sub>0', is, xta) in C; \<Phi> C M ! pc = \<lfloor>(ts # ST, LT)\<rfloor>; P,h \<turnstile> loc [:\<le>\<^sub>\<top>] LT; pc < length is; conf_fs P h \<Phi> M (length Tsa) Ta frs; \<forall>x\<in>set (relevant_entries P Pop pc xt). case x of (f, t, C, ab) \<Rightarrow> is_class P C \<and> (case ab of (h, d) \<Rightarrow> d \<le> Suc (length ST) \<and> d < mxs); Suc pc < length ins; stk = z # zs; \<forall>x\<in>set (xcpt_eff Pop P pc (ts # ST, LT) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < length ins; P,h \<turnstile> z :\<le> ts; P,h \<turnstile> zs [:\<le>] ST; \<forall>x\<in>set (xcpt_eff Pop P pc (ts # ST, LT) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' \<Phi> C M ! pc'; \<Phi> C M ! Suc pc = \<lfloor>(ab, bb)\<rfloor>; P \<turnstile> ST [\<le>] ab; P \<turnstile> LT [\<le>\<^sub>\<top>] bb; Tsa = Ts \<and> Ta = T \<and> (mxsa, mxl\<^sub>0', is, xta) = (mxs, mxl\<^sub>0, ins, xt) \<and> C = C\<rbrakk> \<Longrightarrow> \<exists>Ts T mxs mxl\<^sub>0 is. (\<exists>xt. P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C) \<and> P,h \<turnstile> zs [:\<le>] ab \<and> P,h \<turnstile> loc [:\<le>\<^sub>\<top>] bb \<and> Suc pc < length is \<and> conf_fs P h \<Phi> M (length Ts) T frs
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done