[STATEMENT]
lemma transIrreflexiveOrderingIsAcyclic:
  assumes "trans r" and "\<forall> x. (x, x) \<notin> r"
  shows "acyclic r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic r
[PROOF STEP]
proof (rule acyclicI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
assume "\<exists> x. (x, x) \<in> r^+"
[PROOF STATE]
proof (state)
this:
\<exists>x. (x, x) \<in> r\<^sup>+

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. (x, x) \<in> r\<^sup>+
[PROOF STEP]
obtain x where "(x, x) \<in> r^+"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. (x, x) \<in> r\<^sup>+

goal (1 subgoal):
 1. (\<And>x. (x, x) \<in> r\<^sup>+ \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> r\<^sup>+

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, x) \<in> r\<^sup>+

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
from \<open>trans r\<close>
[PROOF STATE]
proof (chain)
picking this:
trans r
[PROOF STEP]
have "r^+ = r"
[PROOF STATE]
proof (prove)
using this:
trans r

goal (1 subgoal):
 1. r\<^sup>+ = r
[PROOF STEP]
by (rule trancl_id)
[PROOF STATE]
proof (state)
this:
r\<^sup>+ = r

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x, x) \<in> r\<^sup>+
r\<^sup>+ = r
[PROOF STEP]
have "(x, x) \<in> r"
[PROOF STATE]
proof (prove)
using this:
(x, x) \<in> r\<^sup>+
r\<^sup>+ = r

goal (1 subgoal):
 1. (x, x) \<in> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, x) \<in> r

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
with \<open>\<forall> x. (x, x) \<notin> r\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (x, x) \<notin> r
(x, x) \<in> r
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x, x) \<notin> r
(x, x) \<in> r

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

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>x. (x, x) \<in> r\<^sup>+ \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
thus "\<forall> x. (x, x) \<notin> r^+"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. (x, x) \<in> r\<^sup>+ \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> r\<^sup>+
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. (x, x) \<notin> r\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lexLessAppend:
  assumes "b \<noteq> []"
  shows "(a @ b, a) \<in> lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a @ b, a) \<in> lexLess
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a @ b, a) \<in> lexLess
[PROOF STEP]
from \<open>b \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> []
[PROOF STEP]
have "\<exists> aa list. b = aa # list"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> []

goal (1 subgoal):
 1. \<exists>aa list. b = aa # list
[PROOF STEP]
by (simp add: neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
\<exists>aa list. b = aa # list

goal (1 subgoal):
 1. (a @ b, a) \<in> lexLess
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>aa list. b = aa # list
[PROOF STEP]
obtain aa::"'a \<times> bool" and list :: "'a Trail"
    where "b = aa # list"
[PROOF STATE]
proof (prove)
using this:
\<exists>aa list. b = aa # list

goal (1 subgoal):
 1. (\<And>aa list. b = aa # list \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = aa # list

goal (1 subgoal):
 1. (a @ b, a) \<in> lexLess
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b = aa # list

goal (1 subgoal):
 1. (a @ b, a) \<in> lexLess
[PROOF STEP]
unfolding lexLess_def
[PROOF STATE]
proof (prove)
using this:
b = aa # list

goal (1 subgoal):
 1. (a @ b, a) \<in> {(M1, M2). (M2, M1) \<in> lexord decisionLess}
[PROOF STEP]
unfolding lexord_def
[PROOF STATE]
proof (prove)
using this:
b = aa # list

goal (1 subgoal):
 1. (a @ b, a) \<in> {(M1, M2). (M2, M1) \<in> {(x, y). \<exists>a v. y = x @ a # v \<or> (\<exists>u a b v w. (a, b) \<in> decisionLess \<and> x = u @ a # v \<and> y = u @ b # w)}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a @ b, a) \<in> lexLess

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lexLessBackjump:
  assumes "p = prefixToLevel level a" and "level >= 0" and "level < currentLevel a"
  shows "(p @ [(x, False)], a) \<in> lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
p = prefixToLevel level a
0 \<le> level
level < currentLevel a
[PROOF STEP]
have "\<exists> rest. prefixToLevel level a @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)"
[PROOF STATE]
proof (prove)
using this:
p = prefixToLevel level a
0 \<le> level
level < currentLevel a

goal (1 subgoal):
 1. \<exists>rest. prefixToLevel level a @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)
[PROOF STEP]
using isProperPrefixPrefixToLevel
[PROOF STATE]
proof (prove)
using this:
p = prefixToLevel level a
0 \<le> level
level < currentLevel a
?level < currentLevel ?t \<Longrightarrow> \<exists>s. prefixToLevel ?level ?t @ s = ?t \<and> s \<noteq> [] \<and> isDecision (hd s)

goal (1 subgoal):
 1. \<exists>rest. prefixToLevel level a @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>rest. prefixToLevel level a @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
with \<open>p = prefixToLevel level a\<close>
[PROOF STATE]
proof (chain)
picking this:
p = prefixToLevel level a
\<exists>rest. prefixToLevel level a @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)
[PROOF STEP]
obtain rest
    where "p @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)"
[PROOF STATE]
proof (prove)
using this:
p = prefixToLevel level a
\<exists>rest. prefixToLevel level a @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)

goal (1 subgoal):
 1. (\<And>rest. p @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
unfolding lexLess_def
[PROOF STATE]
proof (prove)
using this:
p @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> {(M1, M2). (M2, M1) \<in> lexord decisionLess}
[PROOF STEP]
using lexord_append_left_rightI[of "hd rest" "(x, False)" "decisionLess" "p" "tl rest" "[]"]
[PROOF STATE]
proof (prove)
using this:
p @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)
(hd rest, x, False) \<in> decisionLess \<Longrightarrow> (p @ hd rest # tl rest, p @ [(x, False)]) \<in> lexord decisionLess

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> {(M1, M2). (M2, M1) \<in> lexord decisionLess}
[PROOF STEP]
unfolding decisionLess_def
[PROOF STATE]
proof (prove)
using this:
p @ rest = a \<and> rest \<noteq> [] \<and> isDecision (hd rest)
(hd rest, x, False) \<in> {(l1, l2). isDecision l1 \<and> \<not> isDecision l2} \<Longrightarrow> (p @ hd rest # tl rest, p @ [(x, False)]) \<in> lexord {(l1, l2). isDecision l1 \<and> \<not> isDecision l2}

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> {(M1, M2). (M2, M1) \<in> lexord {(l1, l2). isDecision l1 \<and> \<not> isDecision l2}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(p @ [(x, False)], a) \<in> lexLess

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lexLessBacktrack:
  assumes "p = prefixBeforeLastDecision a" "decisions a \<noteq> []"
  shows "(p @ [(x, False)], a) \<in> lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p = prefixBeforeLastDecision a
decisions a \<noteq> []

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
using prefixBeforeLastMarkedIsPrefixBeforeLastLevel[of "a"]
[PROOF STATE]
proof (prove)
using this:
p = prefixBeforeLastDecision a
decisions a \<noteq> []
decisions a \<noteq> [] \<Longrightarrow> prefixBeforeLastDecision a = prefixToLevel (currentLevel a - 1) a

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
using lexLessBackjump[of "p" "currentLevel a - 1" "a"]
[PROOF STATE]
proof (prove)
using this:
p = prefixBeforeLastDecision a
decisions a \<noteq> []
decisions a \<noteq> [] \<Longrightarrow> prefixBeforeLastDecision a = prefixToLevel (currentLevel a - 1) a
\<lbrakk>p = prefixToLevel (currentLevel a - 1) a; 0 \<le> currentLevel a - 1; currentLevel a - 1 < currentLevel a\<rbrakk> \<Longrightarrow> (p @ [(?x, False)], a) \<in> lexLess

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
unfolding currentLevel_def
[PROOF STATE]
proof (prove)
using this:
p = prefixBeforeLastDecision a
decisions a \<noteq> []
decisions a \<noteq> [] \<Longrightarrow> prefixBeforeLastDecision a = prefixToLevel (length (decisions a) - 1) a
\<lbrakk>p = prefixToLevel (length (decisions a) - 1) a; 0 \<le> length (decisions a) - 1; length (decisions a) - 1 < length (decisions a)\<rbrakk> \<Longrightarrow> (p @ [(?x, False)], a) \<in> lexLess

goal (1 subgoal):
 1. (p @ [(x, False)], a) \<in> lexLess
[PROOF STEP]
by auto


[STATEMENT]
lemma transDecisionLess:
  shows "trans decisionLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
fix x::"('a*bool)" and y::"('a*bool)" and z::"('a*bool)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
assume "(x, y) \<in> decisionLess"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> decisionLess

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
hence "\<not> isDecision y"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> decisionLess

goal (1 subgoal):
 1. \<not> isDecision y
[PROOF STEP]
unfolding decisionLess_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(l1, l2). isDecision l1 \<and> \<not> isDecision l2}

goal (1 subgoal):
 1. \<not> isDecision y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> isDecision y

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> isDecision y

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
assume "(y, z) \<in> decisionLess"
[PROOF STATE]
proof (state)
this:
(y, z) \<in> decisionLess

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
hence "isDecision y"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> decisionLess

goal (1 subgoal):
 1. isDecision y
[PROOF STEP]
unfolding decisionLess_def
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> {(l1, l2). isDecision l1 \<and> \<not> isDecision l2}

goal (1 subgoal):
 1. isDecision y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isDecision y

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> isDecision y
isDecision y
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<not> isDecision y
isDecision y

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

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
hence "(x, z) \<in> decisionLess"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. (x, z) \<in> decisionLess
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, z) \<in> decisionLess

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> decisionLess; (?y2, ?z2) \<in> decisionLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> decisionLess

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> decisionLess; (?y2, ?z2) \<in> decisionLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> decisionLess

goal (1 subgoal):
 1. trans decisionLess
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> decisionLess; (?y2, ?z2) \<in> decisionLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> decisionLess

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> decisionLess \<longrightarrow> (y, z) \<in> decisionLess \<longrightarrow> (x, z) \<in> decisionLess
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trans decisionLess

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma translexLess:
  shows "trans lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
fix x :: "'a Trail" and y :: "'a Trail" and z :: "'a Trail"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
assume "(x, y) \<in> lexLess" and "(y, z) \<in> lexLess"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> lexLess
(y, z) \<in> lexLess

goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
hence "(x, z) \<in> lexLess"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> lexLess
(y, z) \<in> lexLess

goal (1 subgoal):
 1. (x, z) \<in> lexLess
[PROOF STEP]
using lexord_trans transDecisionLess
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> lexLess
(y, z) \<in> lexLess
\<lbrakk>(?x, ?y) \<in> lexord ?r; (?y, ?z) \<in> lexord ?r; trans ?r\<rbrakk> \<Longrightarrow> (?x, ?z) \<in> lexord ?r
trans decisionLess

goal (1 subgoal):
 1. (x, z) \<in> lexLess
[PROOF STEP]
unfolding lexLess_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(M1, M2). (M2, M1) \<in> lexord decisionLess}
(y, z) \<in> {(M1, M2). (M2, M1) \<in> lexord decisionLess}
\<lbrakk>(?x, ?y) \<in> lexord ?r; (?y, ?z) \<in> lexord ?r; trans ?r\<rbrakk> \<Longrightarrow> (?x, ?z) \<in> lexord ?r
trans decisionLess

goal (1 subgoal):
 1. (x, z) \<in> {(M1, M2). (M2, M1) \<in> lexord decisionLess}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, z) \<in> lexLess

goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> lexLess; (?y2, ?z2) \<in> lexLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> lexLess

goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> lexLess; (?y2, ?z2) \<in> lexLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> lexLess

goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> lexLess; (?y2, ?z2) \<in> lexLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> lexLess

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> lexLess \<longrightarrow> (y, z) \<in> lexLess \<longrightarrow> (x, z) \<in> lexLess
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trans lexLess

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irreflexiveDecisionLess:
  shows "(x, x) \<notin> decisionLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, x) \<notin> decisionLess
[PROOF STEP]
unfolding decisionLess_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, x) \<notin> {(l1, l2). isDecision l1 \<and> \<not> isDecision l2}
[PROOF STEP]
by simp


[STATEMENT]
lemma irreflexiveLexLess:
  shows "(x, x) \<notin> lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, x) \<notin> lexLess
[PROOF STEP]
using lexord_irreflexive[of "decisionLess" "x"] irreflexiveDecisionLess
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x, x) \<notin> decisionLess \<Longrightarrow> (x, x) \<notin> lexord decisionLess
(?x, ?x) \<notin> decisionLess

goal (1 subgoal):
 1. (x, x) \<notin> lexLess
[PROOF STEP]
unfolding lexLess_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x, x) \<notin> decisionLess \<Longrightarrow> (x, x) \<notin> lexord decisionLess
(?x, ?x) \<notin> decisionLess

goal (1 subgoal):
 1. (x, x) \<notin> {(M1, M2). (M2, M1) \<in> lexord decisionLess}
[PROOF STEP]
by auto


[STATEMENT]
lemma acyclicLexLess:
  shows "acyclic lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic lexLess
[PROOF STEP]
proof (rule transIrreflexiveOrderingIsAcyclic)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trans lexLess
 2. \<forall>x. (x, x) \<notin> lexLess
[PROOF STEP]
show "trans lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
using translexLess
[PROOF STATE]
proof (prove)
using this:
trans lexLess

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

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> lexLess
[PROOF STEP]
show "\<forall> x. (x, x) \<notin> lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> lexLess
[PROOF STEP]
using irreflexiveLexLess
[PROOF STATE]
proof (prove)
using this:
(?x, ?x) \<notin> lexLess

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> lexLess
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. (x, x) \<notin> lexLess

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finiteVarsClause:
  fixes c :: Clause
  shows "finite (vars c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars c)
[PROOF STEP]
by (induct c) auto


[STATEMENT]
lemma finiteVarsFormula:
  fixes F :: Formula
  shows "finite (vars F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars F)
[PROOF STEP]
proof (induct F)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (vars [])
 2. \<And>a F. finite (vars F) \<Longrightarrow> finite (vars (a # F))
[PROOF STEP]
case (Cons c F)
[PROOF STATE]
proof (state)
this:
finite (vars F)

goal (2 subgoals):
 1. finite (vars [])
 2. \<And>a F. finite (vars F) \<Longrightarrow> finite (vars (a # F))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite (vars F)

goal (1 subgoal):
 1. finite (vars (c # F))
[PROOF STEP]
using finiteVarsClause[of "c"]
[PROOF STATE]
proof (prove)
using this:
finite (vars F)
finite (vars c)

goal (1 subgoal):
 1. finite (vars (c # F))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (vars (c # F))

goal (1 subgoal):
 1. finite (vars [])
[PROOF STEP]
qed simp


[STATEMENT]
lemma finiteListDecompose:
  shows "finite {(a, b). l = a @ b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(a, b). l = a @ b}
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {a. case a of (a, b) \<Rightarrow> [] = a @ b}
 2. \<And>a l. finite {a. case a of (a, b) \<Rightarrow> l = a @ b} \<Longrightarrow> finite {b. case b of (aa, b) \<Rightarrow> a # l = aa @ b}
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite {a. case a of (a, b) \<Rightarrow> [] = a @ b}
 2. \<And>a l. finite {a. case a of (a, b) \<Rightarrow> l = a @ b} \<Longrightarrow> finite {b. case b of (aa, b) \<Rightarrow> a # l = aa @ b}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> [] = a @ b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {a. case a of (a, b) \<Rightarrow> [] = a @ b}

goal (1 subgoal):
 1. \<And>a l. finite {a. case a of (a, b) \<Rightarrow> l = a @ b} \<Longrightarrow> finite {b. case b of (aa, b) \<Rightarrow> a # l = aa @ b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. finite {a. case a of (a, b) \<Rightarrow> l = a @ b} \<Longrightarrow> finite {b. case b of (aa, b) \<Rightarrow> a # l = aa @ b}
[PROOF STEP]
case (Cons x l')
[PROOF STATE]
proof (state)
this:
finite {a. case a of (a, b) \<Rightarrow> l' = a @ b}

goal (1 subgoal):
 1. \<And>a l. finite {a. case a of (a, b) \<Rightarrow> l = a @ b} \<Longrightarrow> finite {b. case b of (aa, b) \<Rightarrow> a # l = aa @ b}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite {a. case a of (a, b) \<Rightarrow> l' = a @ b}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
let "?S l" = "{(a, b). l = a @ b}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
let "?S' x l'" = "{(a', b). a' = [] \<and> b = (x # l') \<or>
                                (\<exists> a. a' = x # a \<and> (a, b) \<in> (?S l'))}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
have "?S (x # l') = ?S' x l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. case a of (a, b) \<Rightarrow> x # l' = a @ b} = {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {a. case a of (a, b) \<Rightarrow> x # l' = a @ b} \<subseteq> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
 2. {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<subseteq> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
show "?S (x # l') \<subseteq> ?S' x l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. case a of (a, b) \<Rightarrow> x # l' = a @ b} \<subseteq> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b} \<Longrightarrow> xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b} \<Longrightarrow> xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
assume "k \<in> ?S (x # l')"
[PROOF STATE]
proof (state)
this:
k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b} \<Longrightarrow> xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
obtain a and b
          where "k = (a, b)" "x # l' = a @ b"
[PROOF STATE]
proof (prove)
using this:
k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>k = (a, b); x # l' = a @ b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = (a, b)
x # l' = a @ b

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b} \<Longrightarrow> xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = (a, b)
x # l' = a @ b
[PROOF STEP]
obtain a' where "a' = x # a"
[PROOF STATE]
proof (prove)
using this:
k = (a, b)
x # l' = a @ b

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b} \<Longrightarrow> xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
from \<open>k = (a, b)\<close> \<open>x # l' = a @ b\<close>
[PROOF STATE]
proof (chain)
picking this:
k = (a, b)
x # l' = a @ b
[PROOF STEP]
show "k \<in> ?S' x l'"
[PROOF STATE]
proof (prove)
using this:
k = (a, b)
x # l' = a @ b

goal (1 subgoal):
 1. k \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
using SimpleLevi[of "a" "b" "x" "l'"]
[PROOF STATE]
proof (prove)
using this:
k = (a, b)
x # l' = a @ b
(a @ b = x # l') = (a = [] \<and> b = x # l' \<or> (\<exists>t. a = x # t \<and> t @ b = l'))

goal (1 subgoal):
 1. k \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{a. case a of (a, b) \<Rightarrow> x # l' = a @ b} \<subseteq> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}

goal (1 subgoal):
 1. {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<subseteq> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<subseteq> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
show "?S' x l' \<subseteq> ?S (x # l')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<subseteq> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
assume "k \<in> ?S' x l'"
[PROOF STATE]
proof (state)
this:
k \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
[PROOF STEP]
obtain a' and b where
          "k = (a', b)" "a' = [] \<and> b = x # l' \<or> (\<exists> a . a' = x # a \<and> (a, b) \<in> ?S l')"
[PROOF STATE]
proof (prove)
using this:
k \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}

goal (1 subgoal):
 1. (\<And>a' b. \<lbrakk>k = (a', b); a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = (a', b)
a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k = (a', b)
a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
k = (a', b)
a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
assume "a' = []" "b = x # l'"
[PROOF STATE]
proof (state)
this:
a' = []
b = x # l'

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
with \<open>k = (a', b)\<close>
[PROOF STATE]
proof (chain)
picking this:
k = (a', b)
a' = []
b = x # l'
[PROOF STEP]
have "k \<in> ?S (x # l')"
[PROOF STATE]
proof (prove)
using this:
k = (a', b)
a' = []
b = x # l'

goal (1 subgoal):
 1. k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a' = []; b = x # l'\<rbrakk> \<Longrightarrow> k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a' = []; b = x # l'\<rbrakk> \<Longrightarrow> k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a' = []; b = x # l'\<rbrakk> \<Longrightarrow> k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
assume "\<exists> a. a' = x # a \<and> (a, b) \<in> ?S l'"
[PROOF STATE]
proof (state)
this:
\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}
[PROOF STEP]
obtain a where
            "a' = x # a \<and> (a, b) \<in> ?S l'"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}

goal (1 subgoal):
 1. (\<And>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
with \<open>k = (a', b)\<close>
[PROOF STATE]
proof (chain)
picking this:
k = (a', b)
a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}
[PROOF STEP]
have "k \<in> ?S (x # l')"
[PROOF STATE]
proof (prove)
using this:
k = (a', b)
a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}

goal (1 subgoal):
 1. k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<Longrightarrow> xa \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k = (a', b)
a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})
\<lbrakk>a' = []; b = x # l'\<rbrakk> \<Longrightarrow> k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
show "k \<in> ?S (x # l')"
[PROOF STATE]
proof (prove)
using this:
k = (a', b)
a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})
\<lbrakk>a' = []; b = x # l'\<rbrakk> \<Longrightarrow> k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal (1 subgoal):
 1. k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} \<subseteq> {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{a. case a of (a, b) \<Rightarrow> x # l' = a @ b} = {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{a. case a of (a, b) \<Rightarrow> x # l' = a @ b} = {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
have "?S' x l' =
      {(a', b). a' = [] \<and> b = x # l'} \<union> {(a', b). \<exists> a. a' = x # a \<and> (a, b) \<in> ?S l'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} = {(a', b). a' = [] \<and> b = x # l'} \<union> {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} = {(a', b). a' = [] \<and> b = x # l'} \<union> {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} = {(a', b). a' = [] \<and> b = x # l'} \<union> {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
have "finite {(a', b). \<exists> a. a' = x # a \<and> (a, b) \<in> ?S l'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
[PROOF STEP]
let ?h = "\<lambda> (a, b). (x # a, b)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
[PROOF STEP]
have "{(a', b). \<exists> a. a' = x # a \<and>  (a, b) \<in> ?S l'} = ?h ` {(a, b).  l' = a @ b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}} = (\<lambda>(a, b). (x # a, b)) ` {(a, b). l' = a @ b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}} = (\<lambda>(a, b). (x # a, b)) ` {(a, b). l' = a @ b}

goal (1 subgoal):
 1. finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}} = (\<lambda>(a, b). (x # a, b)) ` {(a, b). l' = a @ b}

goal (1 subgoal):
 1. finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
[PROOF STEP]
using Cons(1)
[PROOF STATE]
proof (prove)
using this:
{(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}} = (\<lambda>(a, b). (x # a, b)) ` {(a, b). l' = a @ b}
finite {a. case a of (a, b) \<Rightarrow> l' = a @ b}

goal (1 subgoal):
 1. finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
have "finite {(a', b). a' = [] \<and> b = x # l'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(a', b). a' = [] \<and> b = x # l'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {(a', b). a' = [] \<and> b = x # l'}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> l' = a @ b} \<Longrightarrow> finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{a. case a of (a, b) \<Rightarrow> x # l' = a @ b} = {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
{a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} = {(a', b). a' = [] \<and> b = x # l'} \<union> {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
finite {(a', b). a' = [] \<and> b = x # l'}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{a. case a of (a, b) \<Rightarrow> x # l' = a @ b} = {a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})}
{a. case a of (a', b) \<Rightarrow> a' = [] \<and> b = x # l' \<or> (\<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b})} = {(a', b). a' = [] \<and> b = x # l'} \<union> {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
finite {(a', b). \<exists>a. a' = x # a \<and> (a, b) \<in> {a. case a of (a, b) \<Rightarrow> l' = a @ b}}
finite {(a', b). a' = [] \<and> b = x # l'}

goal (1 subgoal):
 1. finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {a. case a of (a, b) \<Rightarrow> x # l' = a @ b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finiteListDecomposeSet:
  fixes L :: "'a list set"
  assumes "finite L"
  shows "finite {(a, b). \<exists> l. l \<in> L \<and> l = a @ b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(a, b). \<exists>l. l \<in> L \<and> l = a @ b}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {(a, b). \<exists>l. l \<in> L \<and> l = a @ b}
[PROOF STEP]
have "{(a, b). \<exists> l. l \<in> L \<and> l = a @ b} = (\<Union> l \<in> L. {(a, b). l = a @ b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(a, b). \<exists>l. l \<in> L \<and> l = a @ b} = (\<Union>l\<in>L. {(a, b). l = a @ b})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(a, b). \<exists>l. l \<in> L \<and> l = a @ b} = (\<Union>l\<in>L. {(a, b). l = a @ b})

goal (1 subgoal):
 1. finite {(a, b). \<exists>l. l \<in> L \<and> l = a @ b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(a, b). \<exists>l. l \<in> L \<and> l = a @ b} = (\<Union>l\<in>L. {(a, b). l = a @ b})

goal (1 subgoal):
 1. finite {(a, b). \<exists>l. l \<in> L \<and> l = a @ b}
[PROOF STEP]
have "finite (\<Union> l \<in> L. {(a, b). l = a @ b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union>l\<in>L. {(a, b). l = a @ b})
[PROOF STEP]
proof (rule finite_UN_I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite L
 2. \<And>l. l \<in> L \<Longrightarrow> finite {(a, b). l = a @ b}
[PROOF STEP]
from \<open>finite L\<close>
[PROOF STATE]
proof (chain)
picking this:
finite L
[PROOF STEP]
show "finite L"
[PROOF STATE]
proof (prove)
using this:
finite L

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

goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> finite {(a, b). l = a @ b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> finite {(a, b). l = a @ b}
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> finite {(a, b). l = a @ b}
[PROOF STEP]
assume "l \<in> L"
[PROOF STATE]
proof (state)
this:
l \<in> L

goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> finite {(a, b). l = a @ b}
[PROOF STEP]
show "finite {(a, b). l = a @ b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(a, b). l = a @ b}
[PROOF STEP]
by (rule finiteListDecompose)
[PROOF STATE]
proof (state)
this:
finite {(a, b). l = a @ b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite (\<Union>l\<in>L. {(a, b). l = a @ b})

goal (1 subgoal):
 1. finite {(a, b). \<exists>l. l \<in> L \<and> l = a @ b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(a, b). \<exists>l. l \<in> L \<and> l = a @ b} = (\<Union>l\<in>L. {(a, b). l = a @ b})
finite (\<Union>l\<in>L. {(a, b). l = a @ b})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{(a, b). \<exists>l. l \<in> L \<and> l = a @ b} = (\<Union>l\<in>L. {(a, b). l = a @ b})
finite (\<Union>l\<in>L. {(a, b). l = a @ b})

goal (1 subgoal):
 1. finite {(a, b). \<exists>l. l \<in> L \<and> l = a @ b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {(a, b). \<exists>l. l \<in> L \<and> l = a @ b}

goal:
No subgoals!
[PROOF STEP]
qed