[STATEMENT]
lemma treezise_delete:
  assumes "internal p T"
  shows "treesize (delete p T) < treesize T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. treesize (delete p T) < treesize T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
internal p T

goal (1 subgoal):
 1. treesize (delete p T) < treesize T
[PROOF STEP]
proof (induction p arbitrary: T)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. internal [] T \<Longrightarrow> treesize (delete [] T) < treesize T
 2. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
case (Nil)
[PROOF STATE]
proof (state)
this:
internal [] T

goal (2 subgoals):
 1. \<And>T. internal [] T \<Longrightarrow> treesize (delete [] T) < treesize T
 2. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal [] T
[PROOF STEP]
have "\<exists>T1 T2. T = Branching T1 T2"
[PROOF STATE]
proof (prove)
using this:
internal [] T

goal (1 subgoal):
 1. \<exists>T1 T2. T = Branching T1 T2
[PROOF STEP]
by (cases T) auto
[PROOF STATE]
proof (state)
this:
\<exists>T1 T2. T = Branching T1 T2

goal (2 subgoals):
 1. \<And>T. internal [] T \<Longrightarrow> treesize (delete [] T) < treesize T
 2. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>T1 T2. T = Branching T1 T2
[PROOF STEP]
obtain T1 T2 where T1T2_p: "T = Branching T1 T2"
[PROOF STATE]
proof (prove)
using this:
\<exists>T1 T2. T = Branching T1 T2

goal (1 subgoal):
 1. (\<And>T1 T2. T = Branching T1 T2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T = Branching T1 T2

goal (2 subgoals):
 1. \<And>T. internal [] T \<Longrightarrow> treesize (delete [] T) < treesize T
 2. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = Branching T1 T2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
T = Branching T1 T2

goal (1 subgoal):
 1. treesize (delete [] T) < treesize T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
treesize (delete [] T) < treesize T

goal (1 subgoal):
 1. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
internal p ?T \<Longrightarrow> treesize (delete p ?T) < treesize ?T
internal (a # p) T

goal (1 subgoal):
 1. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal p ?T \<Longrightarrow> treesize (delete p ?T) < treesize ?T
internal (a # p) T
[PROOF STEP]
have "\<exists>T1 T2. T = Branching T1 T2"
[PROOF STATE]
proof (prove)
using this:
internal p ?T \<Longrightarrow> treesize (delete p ?T) < treesize ?T
internal (a # p) T

goal (1 subgoal):
 1. \<exists>T1 T2. T = Branching T1 T2
[PROOF STEP]
using path_inv_Cons internal_is_path
[PROOF STATE]
proof (prove)
using this:
internal p ?T \<Longrightarrow> treesize (delete p ?T) < treesize ?T
internal (a # p) T
path (?a # ?ds) ?T \<longrightarrow> (\<exists>l r. ?T = Branching l r)
internal ?ds ?T \<Longrightarrow> path ?ds ?T

goal (1 subgoal):
 1. \<exists>T1 T2. T = Branching T1 T2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T1 T2. T = Branching T1 T2

goal (1 subgoal):
 1. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>T1 T2. T = Branching T1 T2
[PROOF STEP]
obtain T1 T2 where T1T2_p: "T = Branching T1 T2"
[PROOF STATE]
proof (prove)
using this:
\<exists>T1 T2. T = Branching T1 T2

goal (1 subgoal):
 1. (\<And>T1 T2. T = Branching T1 T2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T = Branching T1 T2

goal (1 subgoal):
 1. \<And>a p T. \<lbrakk>\<And>T. internal p T \<Longrightarrow> treesize (delete p T) < treesize T; internal (a # p) T\<rbrakk> \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. treesize (delete (a # p) T) < treesize T
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
 2. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
assume a_p: a
[PROOF STATE]
proof (state)
this:
a

goal (2 subgoals):
 1. a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
 2. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
from a_p
[PROOF STATE]
proof (chain)
picking this:
a
[PROOF STEP]
have "delete (a#p) T = (Branching (delete p T1) T2)"
[PROOF STATE]
proof (prove)
using this:
a

goal (1 subgoal):
 1. delete (a # p) T = Branching (delete p T1) T2
[PROOF STEP]
using T1T2_p
[PROOF STATE]
proof (prove)
using this:
a
T = Branching T1 T2

goal (1 subgoal):
 1. delete (a # p) T = Branching (delete p T1) T2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
delete (a # p) T = Branching (delete p T1) T2

goal (2 subgoals):
 1. a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
 2. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
delete (a # p) T = Branching (delete p T1) T2

goal (2 subgoals):
 1. a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
 2. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
from a_p
[PROOF STATE]
proof (chain)
picking this:
a
[PROOF STEP]
have "internal p T1"
[PROOF STATE]
proof (prove)
using this:
a

goal (1 subgoal):
 1. internal p T1
[PROOF STEP]
using T1T2_p Cons
[PROOF STATE]
proof (prove)
using this:
a
T = Branching T1 T2
internal p ?T \<Longrightarrow> treesize (delete p ?T) < treesize ?T
internal (a # p) T

goal (1 subgoal):
 1. internal p T1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal p T1

goal (2 subgoals):
 1. a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
 2. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal p T1
[PROOF STEP]
have "treesize (delete p T1) < treesize T1"
[PROOF STATE]
proof (prove)
using this:
internal p T1

goal (1 subgoal):
 1. treesize (delete p T1) < treesize T1
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
internal p T1
internal p ?T \<Longrightarrow> treesize (delete p ?T) < treesize ?T
internal (a # p) T

goal (1 subgoal):
 1. treesize (delete p T1) < treesize T1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
treesize (delete p T1) < treesize T1

goal (2 subgoals):
 1. a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
 2. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
delete (a # p) T = Branching (delete p T1) T2
treesize (delete p T1) < treesize T1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
delete (a # p) T = Branching (delete p T1) T2
treesize (delete p T1) < treesize T1

goal (1 subgoal):
 1. treesize (delete (a # p) T) < treesize T
[PROOF STEP]
using T1T2_p
[PROOF STATE]
proof (prove)
using this:
delete (a # p) T = Branching (delete p T1) T2
treesize (delete p T1) < treesize T1
T = Branching T1 T2

goal (1 subgoal):
 1. treesize (delete (a # p) T) < treesize T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
treesize (delete (a # p) T) < treesize T

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
assume a_p: "\<not>a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
from a_p
[PROOF STATE]
proof (chain)
picking this:
\<not> a
[PROOF STEP]
have "delete (a#p) T = (Branching T1 (delete p T2))"
[PROOF STATE]
proof (prove)
using this:
\<not> a

goal (1 subgoal):
 1. delete (a # p) T = Branching T1 (delete p T2)
[PROOF STEP]
using T1T2_p
[PROOF STATE]
proof (prove)
using this:
\<not> a
T = Branching T1 T2

goal (1 subgoal):
 1. delete (a # p) T = Branching T1 (delete p T2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
delete (a # p) T = Branching T1 (delete p T2)

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
delete (a # p) T = Branching T1 (delete p T2)

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
from a_p
[PROOF STATE]
proof (chain)
picking this:
\<not> a
[PROOF STEP]
have "internal p T2"
[PROOF STATE]
proof (prove)
using this:
\<not> a

goal (1 subgoal):
 1. internal p T2
[PROOF STEP]
using T1T2_p Cons
[PROOF STATE]
proof (prove)
using this:
\<not> a
T = Branching T1 T2
internal p ?T \<Longrightarrow> treesize (delete p ?T) < treesize ?T
internal (a # p) T

goal (1 subgoal):
 1. internal p T2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal p T2

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal p T2
[PROOF STEP]
have "treesize (delete p T2) < treesize T2"
[PROOF STATE]
proof (prove)
using this:
internal p T2

goal (1 subgoal):
 1. treesize (delete p T2) < treesize T2
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
internal p T2
internal p ?T \<Longrightarrow> treesize (delete p ?T) < treesize ?T
internal (a # p) T

goal (1 subgoal):
 1. treesize (delete p T2) < treesize T2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
treesize (delete p T2) < treesize T2

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> treesize (delete (a # p) T) < treesize T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
delete (a # p) T = Branching T1 (delete p T2)
treesize (delete p T2) < treesize T2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
delete (a # p) T = Branching T1 (delete p T2)
treesize (delete p T2) < treesize T2

goal (1 subgoal):
 1. treesize (delete (a # p) T) < treesize T
[PROOF STEP]
using T1T2_p
[PROOF STATE]
proof (prove)
using this:
delete (a # p) T = Branching T1 (delete p T2)
treesize (delete p T2) < treesize T2
T = Branching T1 T2

goal (1 subgoal):
 1. treesize (delete (a # p) T) < treesize T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
treesize (delete (a # p) T) < treesize T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
treesize (delete (a # p) T) < treesize T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma treesize_cutoff: "treesize (cutoff red ds T) \<le> treesize T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. treesize (cutoff red ds T) \<le> treesize T
[PROOF STEP]
proof (induction T arbitrary: ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. treesize (cutoff red ds Leaf) \<le> treesize Leaf
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. treesize (cutoff red ds T1) \<le> treesize T1; \<And>ds. treesize (cutoff red ds T2) \<le> treesize T2\<rbrakk> \<Longrightarrow> treesize (cutoff red ds (Branching T1 T2)) \<le> treesize (Branching T1 T2)
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>ds. treesize (cutoff red ds Leaf) \<le> treesize Leaf
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. treesize (cutoff red ds T1) \<le> treesize T1; \<And>ds. treesize (cutoff red ds T2) \<le> treesize T2\<rbrakk> \<Longrightarrow> treesize (cutoff red ds (Branching T1 T2)) \<le> treesize (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. treesize (cutoff red ds Leaf) \<le> treesize Leaf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
treesize (cutoff red ds Leaf) \<le> treesize Leaf

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. treesize (cutoff red ds T1) \<le> treesize T1; \<And>ds. treesize (cutoff red ds T2) \<le> treesize T2\<rbrakk> \<Longrightarrow> treesize (cutoff red ds (Branching T1 T2)) \<le> treesize (Branching T1 T2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. treesize (cutoff red ds T1) \<le> treesize T1; \<And>ds. treesize (cutoff red ds T2) \<le> treesize T2\<rbrakk> \<Longrightarrow> treesize (cutoff red ds (Branching T1 T2)) \<le> treesize (Branching T1 T2)
[PROOF STEP]
case (Branching T1 T2)
[PROOF STATE]
proof (state)
this:
treesize (cutoff red ?ds T1) \<le> treesize T1
treesize (cutoff red ?ds T2) \<le> treesize T2

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. treesize (cutoff red ds T1) \<le> treesize T1; \<And>ds. treesize (cutoff red ds T2) \<le> treesize T2\<rbrakk> \<Longrightarrow> treesize (cutoff red ds (Branching T1 T2)) \<le> treesize (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
treesize (cutoff red ?ds T1) \<le> treesize T1
treesize (cutoff red ?ds T2) \<le> treesize T2
[PROOF STEP]
have "treesize (cutoff red (ds@[Left]) T1) + treesize (cutoff red (ds@[Right]) T2) \<le> treesize T1 + treesize T2"
[PROOF STATE]
proof (prove)
using this:
treesize (cutoff red ?ds T1) \<le> treesize T1
treesize (cutoff red ?ds T2) \<le> treesize T2

goal (1 subgoal):
 1. treesize (cutoff red (ds @ [Left]) T1) + treesize (cutoff red (ds @ [Right]) T2) \<le> treesize T1 + treesize T2
[PROOF STEP]
using add_mono
[PROOF STATE]
proof (prove)
using this:
treesize (cutoff red ?ds T1) \<le> treesize T1
treesize (cutoff red ?ds T2) \<le> treesize T2
\<lbrakk>?a \<le> ?b; ?c \<le> ?d\<rbrakk> \<Longrightarrow> ?a + ?c \<le> ?b + ?d

goal (1 subgoal):
 1. treesize (cutoff red (ds @ [Left]) T1) + treesize (cutoff red (ds @ [Right]) T2) \<le> treesize T1 + treesize T2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
treesize (cutoff red (ds @ [Left]) T1) + treesize (cutoff red (ds @ [Right]) T2) \<le> treesize T1 + treesize T2

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. treesize (cutoff red ds T1) \<le> treesize T1; \<And>ds. treesize (cutoff red ds T2) \<le> treesize T2\<rbrakk> \<Longrightarrow> treesize (cutoff red ds (Branching T1 T2)) \<le> treesize (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
treesize (cutoff red (ds @ [Left]) T1) + treesize (cutoff red (ds @ [Right]) T2) \<le> treesize T1 + treesize T2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
treesize (cutoff red (ds @ [Left]) T1) + treesize (cutoff red (ds @ [Right]) T2) \<le> treesize T1 + treesize T2

goal (1 subgoal):
 1. treesize (cutoff red ds (Branching T1 T2)) \<le> treesize (Branching T1 T2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
treesize (cutoff red ds (Branching T1 T2)) \<le> treesize (Branching T1 T2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cutoff_branch':
  assumes "anybranch T (\<lambda>b. red(ds@b))"
  shows "anybranch (cutoff red ds T) (\<lambda>b. red(ds@b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. anybranch (cutoff red ds T) (\<lambda>p. red (ds @ p))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
anybranch T (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. anybranch (cutoff red ds T) (\<lambda>p. red (ds @ p))
[PROOF STEP]
proof (induction T arbitrary: ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
(* This proof seems a bit excessive for such a simple theorem *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
case (Leaf)
[PROOF STATE]
proof (state)
this:
anybranch Leaf (\<lambda>p. red (ds @ p))

goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
let ?T = "cutoff red ds Leaf"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
assume "branch b ?T"
[PROOF STATE]
proof (state)
this:
branch b (cutoff red ds Leaf)

goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch b (cutoff red ds Leaf)
[PROOF STEP]
have "branch b Leaf"
[PROOF STATE]
proof (prove)
using this:
branch b (cutoff red ds Leaf)

goal (1 subgoal):
 1. branch b Leaf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch b Leaf

goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch b Leaf
[PROOF STEP]
have "red(ds@b)"
[PROOF STATE]
proof (prove)
using this:
branch b Leaf

goal (1 subgoal):
 1. red (ds @ b)
[PROOF STEP]
using Leaf
[PROOF STATE]
proof (prove)
using this:
branch b Leaf
anybranch Leaf (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. red (ds @ b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
red (ds @ b)

goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
branch ?b2 (cutoff red ds Leaf) \<Longrightarrow> red (ds @ ?b2)

goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch ?b2 (cutoff red ds Leaf) \<Longrightarrow> red (ds @ ?b2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
branch ?b2 (cutoff red ds Leaf) \<Longrightarrow> red (ds @ ?b2)

goal (1 subgoal):
 1. anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
anybranch (cutoff red ds Leaf) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
case (Branching T\<^sub>1 T\<^sub>2)
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>1) (\<lambda>p. red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>2) (\<lambda>p. red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
let ?T = "cutoff red ds (Branching T\<^sub>1 T\<^sub>2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
from Branching
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>1) (\<lambda>p. red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>2) (\<lambda>p. red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))
[PROOF STEP]
have "\<forall>p. branch (Left#p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ (Left#p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>1) (\<lambda>p. red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>2) (\<lambda>p. red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. \<forall>p. branch (Left # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Left # p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p. branch (Left # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Left # p)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p. branch (Left # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Left # p)
[PROOF STEP]
have "\<forall>p. branch p T\<^sub>1 \<longrightarrow> red (ds @ (Left#p))"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. branch (Left # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Left # p)

goal (1 subgoal):
 1. anybranch T\<^sub>1 (\<lambda>p. red (ds @ Left # p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>1 (\<lambda>p. red (ds @ Left # p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>1 (\<lambda>p. red (ds @ Left # p))
[PROOF STEP]
have "anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red (ds @ Left # p))

goal (1 subgoal):
 1. anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))
[PROOF STEP]
have aa: "anybranch (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. red ((ds @ [Left]) @ p))
         "
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))

goal (1 subgoal):
 1. anybranch (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. red ((ds @ [Left]) @ p))
[PROOF STEP]
using Branching
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>1) (\<lambda>p. red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>2) (\<lambda>p. red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. anybranch (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. red ((ds @ [Left]) @ p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
anybranch (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. red ((ds @ [Left]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
from Branching
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>1) (\<lambda>p. red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>2) (\<lambda>p. red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))
[PROOF STEP]
have "\<forall>p. branch (Right#p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ (Right#p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>1) (\<lambda>p. red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>2) (\<lambda>p. red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. \<forall>p. branch (Right # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Right # p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p. branch (Right # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Right # p)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p. branch (Right # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Right # p)
[PROOF STEP]
have "\<forall>p. branch p T\<^sub>2 \<longrightarrow> red (ds @ (Right#p))"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. branch (Right # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Right # p)

goal (1 subgoal):
 1. anybranch T\<^sub>2 (\<lambda>p. red (ds @ Right # p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>2 (\<lambda>p. red (ds @ Right # p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>2 (\<lambda>p. red (ds @ Right # p))
[PROOF STEP]
have "anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>2 (\<lambda>p. red (ds @ Right # p))

goal (1 subgoal):
 1. anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))
[PROOF STEP]
have bb: "anybranch (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. red ((ds @ [Right]) @ p))
         "
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. anybranch (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. red ((ds @ [Right]) @ p))
[PROOF STEP]
using Branching
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>1) (\<lambda>p. red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anybranch (cutoff red ?ds T\<^sub>2) (\<lambda>p. red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. anybranch (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. red ((ds @ [Right]) @ p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
anybranch (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
anybranch (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
assume b_p: "branch b ?T"
[PROOF STATE]
proof (state)
this:
branch b (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
have "red ds \<or> \<not>red ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red ds \<or> \<not> red ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
red ds \<or> \<not> red ds

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
red ds \<or> \<not> red ds
[PROOF STEP]
have "red(ds@b)"
[PROOF STATE]
proof (prove)
using this:
red ds \<or> \<not> red ds

goal (1 subgoal):
 1. red (ds @ b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. red ds \<Longrightarrow> red (ds @ b)
 2. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
assume ds_p: "red ds"
[PROOF STATE]
proof (state)
this:
red ds

goal (2 subgoals):
 1. red ds \<Longrightarrow> red (ds @ b)
 2. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
red ds
[PROOF STEP]
have "?T = Leaf"
[PROOF STATE]
proof (prove)
using this:
red ds

goal (1 subgoal):
 1. cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Leaf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Leaf

goal (2 subgoals):
 1. red ds \<Longrightarrow> red (ds @ b)
 2. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Leaf
[PROOF STEP]
have "b = []"
[PROOF STATE]
proof (prove)
using this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Leaf

goal (1 subgoal):
 1. b = []
[PROOF STEP]
using b_p branch_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Leaf
branch b (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))
branch ?b Leaf = (?b = [])

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

goal (2 subgoals):
 1. red ds \<Longrightarrow> red (ds @ b)
 2. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = []
[PROOF STEP]
show "red(ds@b)"
[PROOF STATE]
proof (prove)
using this:
b = []

goal (1 subgoal):
 1. red (ds @ b)
[PROOF STEP]
using ds_p
[PROOF STATE]
proof (prove)
using this:
b = []
red ds

goal (1 subgoal):
 1. red (ds @ b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
red (ds @ b)

goal (1 subgoal):
 1. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
assume ds_p: "\<not>red ds"
[PROOF STATE]
proof (state)
this:
\<not> red ds

goal (1 subgoal):
 1. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
let ?T\<^sub>1' = "cutoff red (ds@[Left])  T\<^sub>1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
let ?T\<^sub>2' = "cutoff red (ds@[Right]) T\<^sub>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
from ds_p
[PROOF STATE]
proof (chain)
picking this:
\<not> red ds
[PROOF STEP]
have "?T = Branching ?T\<^sub>1' ?T\<^sub>2'"
[PROOF STATE]
proof (prove)
using this:
\<not> red ds

goal (1 subgoal):
 1. cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)

goal (1 subgoal):
 1. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
from this b_p
[PROOF STATE]
proof (chain)
picking this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)
branch b (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))
[PROOF STEP]
obtain a b' where "b = a # b' \<and> (a \<longrightarrow> branch b' ?T\<^sub>1') \<and> (\<not>a \<longrightarrow> branch b' ?T\<^sub>2' )"
[PROOF STATE]
proof (prove)
using this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)
branch b (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))

goal (1 subgoal):
 1. (\<And>a b'. b = a # b' \<and> (a \<longrightarrow> branch b' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> branch b' (cutoff red (ds @ [Right]) T\<^sub>2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using branch_inv_Branching[of b ?T\<^sub>1' ?T\<^sub>2']
[PROOF STATE]
proof (prove)
using this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)
branch b (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))
branch b (Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)) = (\<exists>a b'. b = a # b' \<and> (a \<longrightarrow> branch b' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> branch b' (cutoff red (ds @ [Right]) T\<^sub>2)))

goal (1 subgoal):
 1. (\<And>a b'. b = a # b' \<and> (a \<longrightarrow> branch b' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> branch b' (cutoff red (ds @ [Right]) T\<^sub>2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = a # b' \<and> (a \<longrightarrow> branch b' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> branch b' (cutoff red (ds @ [Right]) T\<^sub>2))

goal (1 subgoal):
 1. \<not> red ds \<Longrightarrow> red (ds @ b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = a # b' \<and> (a \<longrightarrow> branch b' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> branch b' (cutoff red (ds @ [Right]) T\<^sub>2))
[PROOF STEP]
show "red(ds@b)"
[PROOF STATE]
proof (prove)
using this:
b = a # b' \<and> (a \<longrightarrow> branch b' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> branch b' (cutoff red (ds @ [Right]) T\<^sub>2))

goal (1 subgoal):
 1. red (ds @ b)
[PROOF STEP]
using aa bb
[PROOF STATE]
proof (prove)
using this:
b = a # b' \<and> (a \<longrightarrow> branch b' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> branch b' (cutoff red (ds @ [Right]) T\<^sub>2))
anybranch (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. red ((ds @ [Left]) @ p))
anybranch (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. red (ds @ b)
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
red (ds @ b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
red (ds @ b)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
branch ?b2 (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) \<Longrightarrow> red (ds @ ?b2)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T1) (\<lambda>p. red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anybranch (cutoff red ds T2) (\<lambda>p. red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anybranch (cutoff red ds (Branching T1 T2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch ?b2 (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) \<Longrightarrow> red (ds @ ?b2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
branch ?b2 (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) \<Longrightarrow> red (ds @ ?b2)

goal (1 subgoal):
 1. anybranch (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) (\<lambda>p. red (ds @ p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
anybranch (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) (\<lambda>p. red (ds @ p))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cutoff_branch:
  assumes "anybranch T (\<lambda>p. red p)"
  shows "anybranch (cutoff red [] T) (\<lambda>p. red p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. anybranch (cutoff red [] T) red
[PROOF STEP]
using assms cutoff_branch'[of T red "[]"]
[PROOF STATE]
proof (prove)
using this:
anybranch T red
anybranch T (\<lambda>p. red ([] @ p)) \<Longrightarrow> anybranch (cutoff red [] T) (\<lambda>p. red ([] @ p))

goal (1 subgoal):
 1. anybranch (cutoff red [] T) red
[PROOF STEP]
by auto


[STATEMENT]
lemma cutoff_internal':
  assumes "anybranch T (\<lambda>b. red(ds@b))"
  shows "anyinternal (cutoff red ds T) (\<lambda>b. \<not>red(ds@b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. anyinternal (cutoff red ds T) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
anybranch T (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. anyinternal (cutoff red ds T) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
proof (induction T arbitrary: ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds Leaf) (\<lambda>p. \<not> red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
(* This proof seems a bit excessive for such a simple theorem *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds Leaf) (\<lambda>p. \<not> red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
case (Leaf)
[PROOF STATE]
proof (state)
this:
anybranch Leaf (\<lambda>p. red (ds @ p))

goal (2 subgoals):
 1. \<And>ds. anybranch Leaf (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds Leaf) (\<lambda>p. \<not> red (ds @ p))
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch Leaf (\<lambda>p. red (ds @ p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
anybranch Leaf (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. anyinternal (cutoff red ds Leaf) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
using internal_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
anybranch Leaf (\<lambda>p. red (ds @ p))
\<not> internal ?b Leaf

goal (1 subgoal):
 1. anyinternal (cutoff red ds Leaf) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
anyinternal (cutoff red ds Leaf) (\<lambda>p. \<not> red (ds @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
case (Branching T\<^sub>1 T\<^sub>2)
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>1) (\<lambda>p. \<not> red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>2) (\<lambda>p. \<not> red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
let ?T = "cutoff red ds (Branching T\<^sub>1 T\<^sub>2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
from Branching
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>1) (\<lambda>p. \<not> red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>2) (\<lambda>p. \<not> red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))
[PROOF STEP]
have "\<forall>p. branch (Left#p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ (Left#p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>1) (\<lambda>p. \<not> red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>2) (\<lambda>p. \<not> red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. \<forall>p. branch (Left # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Left # p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p. branch (Left # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Left # p)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p. branch (Left # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Left # p)
[PROOF STEP]
have "\<forall>p. branch p T\<^sub>1 \<longrightarrow> red (ds @ (Left#p))"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. branch (Left # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Left # p)

goal (1 subgoal):
 1. anybranch T\<^sub>1 (\<lambda>p. red (ds @ Left # p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>1 (\<lambda>p. red (ds @ Left # p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>1 (\<lambda>p. red (ds @ Left # p))
[PROOF STEP]
have "anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red (ds @ Left # p))

goal (1 subgoal):
 1. anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))
[PROOF STEP]
have aa: "anyinternal (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. \<not> red ((ds @ [Left]) @ p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))

goal (1 subgoal):
 1. anyinternal (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. \<not> red ((ds @ [Left]) @ p))
[PROOF STEP]
using Branching
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red ((ds @ [Left]) @ p))
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>1) (\<lambda>p. \<not> red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>2) (\<lambda>p. \<not> red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. anyinternal (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. \<not> red ((ds @ [Left]) @ p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
anyinternal (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. \<not> red ((ds @ [Left]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
from Branching
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>1) (\<lambda>p. \<not> red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>2) (\<lambda>p. \<not> red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))
[PROOF STEP]
have "\<forall>p. branch (Right#p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ (Right#p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>1) (\<lambda>p. \<not> red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>2) (\<lambda>p. \<not> red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. \<forall>p. branch (Right # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Right # p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p. branch (Right # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Right # p)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p. branch (Right # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Right # p)
[PROOF STEP]
have "\<forall>p. branch p T\<^sub>2 \<longrightarrow> red (ds @ (Right#p))"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. branch (Right # p) (Branching T\<^sub>1 T\<^sub>2) \<longrightarrow> red (ds @ Right # p)

goal (1 subgoal):
 1. anybranch T\<^sub>2 (\<lambda>p. red (ds @ Right # p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>2 (\<lambda>p. red (ds @ Right # p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>2 (\<lambda>p. red (ds @ Right # p))
[PROOF STEP]
have "anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>2 (\<lambda>p. red (ds @ Right # p))

goal (1 subgoal):
 1. anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))
[PROOF STEP]
have bb: "anyinternal (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. \<not> red ((ds @ [Right]) @ p))"
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. anyinternal (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. \<not> red ((ds @ [Right]) @ p))
[PROOF STEP]
using Branching
[PROOF STATE]
proof (prove)
using this:
anybranch T\<^sub>2 (\<lambda>p. red ((ds @ [Right]) @ p))
anybranch T\<^sub>1 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>1) (\<lambda>p. \<not> red (?ds @ p))
anybranch T\<^sub>2 (\<lambda>p. red (?ds @ p)) \<Longrightarrow> anyinternal (cutoff red ?ds T\<^sub>2) (\<lambda>p. \<not> red (?ds @ p))
anybranch (Branching T\<^sub>1 T\<^sub>2) (\<lambda>p. red (ds @ p))

goal (1 subgoal):
 1. anyinternal (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. \<not> red ((ds @ [Right]) @ p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
anyinternal (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. \<not> red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
anyinternal (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. \<not> red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
assume b_p: "internal p ?T"
[PROOF STATE]
proof (state)
this:
internal p (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal p (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))
[PROOF STEP]
have ds_p: "\<not>red ds"
[PROOF STATE]
proof (prove)
using this:
internal p (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))

goal (1 subgoal):
 1. \<not> red ds
[PROOF STEP]
using internal_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
internal p (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))
\<not> internal ?b Leaf

goal (1 subgoal):
 1. \<not> red ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> red ds

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
have "p=[] \<or> p\<noteq>[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = [] \<or> p \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = [] \<or> p \<noteq> []

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = [] \<or> p \<noteq> []
[PROOF STEP]
have "\<not>red(ds@p)"
[PROOF STATE]
proof (prove)
using this:
p = [] \<or> p \<noteq> []

goal (1 subgoal):
 1. \<not> red (ds @ p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> \<not> red (ds @ p)
 2. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
assume "p=[]"
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> \<not> red (ds @ p)
 2. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = []
[PROOF STEP]
show "\<not>red(ds@p)"
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. \<not> red (ds @ p)
[PROOF STEP]
using ds_p
[PROOF STATE]
proof (prove)
using this:
p = []
\<not> red ds

goal (1 subgoal):
 1. \<not> red (ds @ p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> red (ds @ p)

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
let ?T\<^sub>1' = "cutoff red (ds@[Left])  T\<^sub>1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
let ?T\<^sub>2' = "cutoff red (ds@[Right]) T\<^sub>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
assume "p\<noteq>[]"
[PROOF STATE]
proof (state)
this:
p \<noteq> []

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<noteq> []

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
have "?T = Branching ?T\<^sub>1' ?T\<^sub>2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)
[PROOF STEP]
using ds_p
[PROOF STATE]
proof (prove)
using this:
\<not> red ds

goal (1 subgoal):
 1. cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> []
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)
[PROOF STEP]
obtain a p' where b_p: "p = a # p' \<and>
             (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and>
             (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2))"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)

goal (1 subgoal):
 1. (\<And>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using b_p internal_inv_Branching[of p ?T\<^sub>1' ?T\<^sub>2']
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []
cutoff red ds (Branching T\<^sub>1 T\<^sub>2) = Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)
internal p (cutoff red ds (Branching T\<^sub>1 T\<^sub>2))
internal p (Branching (cutoff red (ds @ [Left]) T\<^sub>1) (cutoff red (ds @ [Right]) T\<^sub>2)) = (p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2))))

goal (1 subgoal):
 1. (\<And>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = a # p' \<and> (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2))

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = a # p' \<and> (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2))
[PROOF STEP]
have "\<not>red(ds @ [a] @ p')"
[PROOF STATE]
proof (prove)
using this:
p = a # p' \<and> (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2))

goal (1 subgoal):
 1. \<not> red (ds @ [a] @ p')
[PROOF STEP]
using aa bb
[PROOF STATE]
proof (prove)
using this:
p = a # p' \<and> (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2))
anyinternal (cutoff red (ds @ [Left]) T\<^sub>1) (\<lambda>p. \<not> red ((ds @ [Left]) @ p))
anyinternal (cutoff red (ds @ [Right]) T\<^sub>2) (\<lambda>p. \<not> red ((ds @ [Right]) @ p))

goal (1 subgoal):
 1. \<not> red (ds @ [a] @ p')
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
\<not> red (ds @ [a] @ p')

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<not> red (ds @ p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> red (ds @ [a] @ p')
[PROOF STEP]
show "\<not>red(ds @ p)"
[PROOF STATE]
proof (prove)
using this:
\<not> red (ds @ [a] @ p')

goal (1 subgoal):
 1. \<not> red (ds @ p)
[PROOF STEP]
using b_p
[PROOF STATE]
proof (prove)
using this:
\<not> red (ds @ [a] @ p')
p = a # p' \<and> (a \<longrightarrow> internal p' (cutoff red (ds @ [Left]) T\<^sub>1)) \<and> (\<not> a \<longrightarrow> internal p' (cutoff red (ds @ [Right]) T\<^sub>2))

goal (1 subgoal):
 1. \<not> red (ds @ p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> red (ds @ p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> red (ds @ p)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
internal ?p2 (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) \<Longrightarrow> \<not> red (ds @ ?p2)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. anybranch T1 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T1) (\<lambda>p. \<not> red (ds @ p)); \<And>ds. anybranch T2 (\<lambda>p. red (ds @ p)) \<Longrightarrow> anyinternal (cutoff red ds T2) (\<lambda>p. \<not> red (ds @ p)); anybranch (Branching T1 T2) (\<lambda>p. red (ds @ p))\<rbrakk> \<Longrightarrow> anyinternal (cutoff red ds (Branching T1 T2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal ?p2 (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) \<Longrightarrow> \<not> red (ds @ ?p2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
internal ?p2 (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) \<Longrightarrow> \<not> red (ds @ ?p2)

goal (1 subgoal):
 1. anyinternal (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) (\<lambda>p. \<not> red (ds @ p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
anyinternal (cutoff red ds (Branching T\<^sub>1 T\<^sub>2)) (\<lambda>p. \<not> red (ds @ p))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cutoff_internal:
  assumes  "anybranch T red"
  shows "anyinternal (cutoff red [] T) (\<lambda>p. \<not>red p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. anyinternal (cutoff red [] T) (\<lambda>p. \<not> red p)
[PROOF STEP]
using assms cutoff_internal'[of T red "[]"]
[PROOF STATE]
proof (prove)
using this:
anybranch T red
anybranch T (\<lambda>p. red ([] @ p)) \<Longrightarrow> anyinternal (cutoff red [] T) (\<lambda>p. \<not> red ([] @ p))

goal (1 subgoal):
 1. anyinternal (cutoff red [] T) (\<lambda>p. \<not> red p)
[PROOF STEP]
by auto


[STATEMENT]
lemma cutoff_branch_internal':
  assumes "anybranch T red"
  shows "anyinternal (cutoff red [] T) (\<lambda>p. \<not>red p) \<and> anybranch (cutoff red [] T) (\<lambda>p. red p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. anyinternal (cutoff red [] T) (\<lambda>p. \<not> red p) \<and> anybranch (cutoff red [] T) red
[PROOF STEP]
using assms cutoff_internal[of T] cutoff_branch[of T]
[PROOF STATE]
proof (prove)
using this:
anybranch T red
anybranch T ?red \<Longrightarrow> anyinternal (cutoff ?red [] T) (\<lambda>p. \<not> ?red p)
anybranch T ?red \<Longrightarrow> anybranch (cutoff ?red [] T) ?red

goal (1 subgoal):
 1. anyinternal (cutoff red [] T) (\<lambda>p. \<not> red p) \<and> anybranch (cutoff red [] T) red
[PROOF STEP]
by blast


[STATEMENT]
lemma cutoff_branch_internal:
  assumes "anybranch T red"
  shows "\<exists>T'. anyinternal T' (\<lambda>p. \<not>red p) \<and> anybranch T' (\<lambda>p. red p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T'. anyinternal T' (\<lambda>p. \<not> red p) \<and> anybranch T' red
[PROOF STEP]
using assms cutoff_branch_internal'
[PROOF STATE]
proof (prove)
using this:
anybranch T red
anybranch ?T ?red \<Longrightarrow> anyinternal (cutoff ?red [] ?T) (\<lambda>p. \<not> ?red p) \<and> anybranch (cutoff ?red [] ?T) ?red

goal (1 subgoal):
 1. \<exists>T'. anyinternal T' (\<lambda>p. \<not> red p) \<and> anybranch T' red
[PROOF STEP]
by blast


[STATEMENT]
lemma subtree_pos:
  "subtree T ds \<subseteq> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right]) \<union> {ds}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtree T ds \<subseteq> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right]) \<union> {ds}
[PROOF STEP]
proof (rule subsetI; rule Set.UnCI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> subtree T ds; x \<notin> {ds}\<rbrakk> \<Longrightarrow> x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
let ?subtree = "subtree T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> subtree T ds; x \<notin> {ds}\<rbrakk> \<Longrightarrow> x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> subtree T ds; x \<notin> {ds}\<rbrakk> \<Longrightarrow> x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
assume asm: "x \<in> ?subtree ds"
[PROOF STATE]
proof (state)
this:
x \<in> subtree T ds

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> subtree T ds; x \<notin> {ds}\<rbrakk> \<Longrightarrow> x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
assume "x \<notin> {ds}"
[PROOF STATE]
proof (state)
this:
x \<notin> {ds}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> subtree T ds; x \<notin> {ds}\<rbrakk> \<Longrightarrow> x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> {ds}
[PROOF STEP]
have "x \<noteq> ds"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {ds}

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> subtree T ds; x \<notin> {ds}\<rbrakk> \<Longrightarrow> x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> ds
[PROOF STEP]
have "\<exists>e d. x = ds @ [d] @ e"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> ds

goal (1 subgoal):
 1. \<exists>e d. x = ds @ [d] @ e
[PROOF STEP]
using asm list.exhaust
[PROOF STATE]
proof (prove)
using this:
x \<noteq> ds
x \<in> subtree T ds
\<lbrakk>?y = [] \<Longrightarrow> ?P; \<And>x21 x22. ?y = x21 # x22 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<exists>e d. x = ds @ [d] @ e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>e d. x = ds @ [d] @ e

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> subtree T ds; x \<notin> {ds}\<rbrakk> \<Longrightarrow> x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>e d. x = ds @ [d] @ e
[PROOF STEP]
have "(\<exists>e. x = ds @ [Left] @ e) \<or> (\<exists>e. x = ds @ [Right] @ e)"
[PROOF STATE]
proof (prove)
using this:
\<exists>e d. x = ds @ [d] @ e

goal (1 subgoal):
 1. (\<exists>e. x = ds @ [Left] @ e) \<or> (\<exists>e. x = ds @ [Right] @ e)
[PROOF STEP]
using bool.exhaust
[PROOF STATE]
proof (prove)
using this:
\<exists>e d. x = ds @ [d] @ e
\<lbrakk>?y = True \<Longrightarrow> ?P; ?y = False \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<exists>e. x = ds @ [Left] @ e) \<or> (\<exists>e. x = ds @ [Right] @ e)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>e. x = ds @ [Left] @ e) \<or> (\<exists>e. x = ds @ [Right] @ e)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> subtree T ds; x \<notin> {ds}\<rbrakk> \<Longrightarrow> x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>e. x = ds @ [Left] @ e) \<or> (\<exists>e. x = ds @ [Right] @ e)
[PROOF STEP]
show "x \<in> ?subtree (ds @ [Left]) \<union> ?subtree (ds @ [Right])"
[PROOF STATE]
proof (prove)
using this:
(\<exists>e. x = ds @ [Left] @ e) \<or> (\<exists>e. x = ds @ [Right] @ e)

goal (1 subgoal):
 1. x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
(\<exists>e. x = ds @ [Left] @ e) \<or> (\<exists>e. x = ds @ [Right] @ e)
x \<in> subtree T ds

goal (1 subgoal):
 1. x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infpath_length:
  assumes "wf_infpath f"
  shows "length (f n) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (f n) = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_infpath f

goal (1 subgoal):
 1. length (f n) = n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf_infpath f \<Longrightarrow> length (f 0) = 0
 2. \<And>n. \<lbrakk>wf_infpath f \<Longrightarrow> length (f n) = n; wf_infpath f\<rbrakk> \<Longrightarrow> length (f (Suc n)) = Suc n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
wf_infpath f

goal (2 subgoals):
 1. wf_infpath f \<Longrightarrow> length (f 0) = 0
 2. \<And>n. \<lbrakk>wf_infpath f \<Longrightarrow> length (f n) = n; wf_infpath f\<rbrakk> \<Longrightarrow> length (f (Suc n)) = Suc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_infpath f
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_infpath f

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

goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf_infpath f \<Longrightarrow> length (f n) = n; wf_infpath f\<rbrakk> \<Longrightarrow> length (f (Suc n)) = Suc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf_infpath f \<Longrightarrow> length (f n) = n; wf_infpath f\<rbrakk> \<Longrightarrow> length (f (Suc n)) = Suc n
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
wf_infpath f \<Longrightarrow> length (f n) = n
wf_infpath f

goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf_infpath f \<Longrightarrow> length (f n) = n; wf_infpath f\<rbrakk> \<Longrightarrow> length (f (Suc n)) = Suc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_infpath f \<Longrightarrow> length (f n) = n
wf_infpath f
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_infpath f \<Longrightarrow> length (f n) = n
wf_infpath f

goal (1 subgoal):
 1. length (f (Suc n)) = Suc n
[PROOF STEP]
by (metis length_append_singleton)
[PROOF STATE]
proof (state)
this:
length (f (Suc n)) = Suc n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_prefix:
  assumes "wf_infpath f"
  assumes "n\<^sub>1 \<le> n\<^sub>2"
  shows "\<exists>a. (f n\<^sub>1) @ a = (f n\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_infpath f
n\<^sub>1 \<le> n\<^sub>2

goal (1 subgoal):
 1. \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
[PROOF STEP]
proof (induction n\<^sub>2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>wf_infpath f; n\<^sub>1 \<le> 0\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f 0
 2. \<And>n\<^sub>2. \<lbrakk>\<lbrakk>wf_infpath f; n\<^sub>1 \<le> n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2; wf_infpath f; n\<^sub>1 \<le> Suc n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
case (Suc n\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>wf_infpath f; n\<^sub>1 \<le> n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
wf_infpath f
n\<^sub>1 \<le> Suc n\<^sub>2

goal (2 subgoals):
 1. \<lbrakk>wf_infpath f; n\<^sub>1 \<le> 0\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f 0
 2. \<And>n\<^sub>2. \<lbrakk>\<lbrakk>wf_infpath f; n\<^sub>1 \<le> n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2; wf_infpath f; n\<^sub>1 \<le> Suc n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>wf_infpath f; n\<^sub>1 \<le> n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
wf_infpath f
n\<^sub>1 \<le> Suc n\<^sub>2
[PROOF STEP]
have "n\<^sub>1 \<le> n\<^sub>2 \<or> n\<^sub>1 = Suc n\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>wf_infpath f; n\<^sub>1 \<le> n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
wf_infpath f
n\<^sub>1 \<le> Suc n\<^sub>2

goal (1 subgoal):
 1. n\<^sub>1 \<le> n\<^sub>2 \<or> n\<^sub>1 = Suc n\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n\<^sub>1 \<le> n\<^sub>2 \<or> n\<^sub>1 = Suc n\<^sub>2

goal (2 subgoals):
 1. \<lbrakk>wf_infpath f; n\<^sub>1 \<le> 0\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f 0
 2. \<And>n\<^sub>2. \<lbrakk>\<lbrakk>wf_infpath f; n\<^sub>1 \<le> n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2; wf_infpath f; n\<^sub>1 \<le> Suc n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>1 \<le> n\<^sub>2 \<or> n\<^sub>1 = Suc n\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 \<le> n\<^sub>2 \<or> n\<^sub>1 = Suc n\<^sub>2

goal (1 subgoal):
 1. \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n\<^sub>1 \<le> n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
 2. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
assume "n\<^sub>1 \<le> n\<^sub>2"
[PROOF STATE]
proof (state)
this:
n\<^sub>1 \<le> n\<^sub>2

goal (2 subgoals):
 1. n\<^sub>1 \<le> n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
 2. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>1 \<le> n\<^sub>2
[PROOF STEP]
obtain a where a: "f n\<^sub>1 @ a = f n\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 \<le> n\<^sub>2

goal (1 subgoal):
 1. (\<And>a. f n\<^sub>1 @ a = f n\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 \<le> n\<^sub>2
\<lbrakk>wf_infpath f; n\<^sub>1 \<le> n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
wf_infpath f
n\<^sub>1 \<le> Suc n\<^sub>2

goal (1 subgoal):
 1. (\<And>a. f n\<^sub>1 @ a = f n\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n\<^sub>1 @ a = f n\<^sub>2

goal (2 subgoals):
 1. n\<^sub>1 \<le> n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
 2. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
have b: "\<exists>b. f (Suc n\<^sub>2) = f n\<^sub>2 @ [b]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. f (Suc n\<^sub>2) = f n\<^sub>2 @ [b]
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>wf_infpath f; n\<^sub>1 \<le> n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
wf_infpath f
n\<^sub>1 \<le> Suc n\<^sub>2

goal (1 subgoal):
 1. \<exists>b. f (Suc n\<^sub>2) = f n\<^sub>2 @ [b]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>b. f (Suc n\<^sub>2) = f n\<^sub>2 @ [b]

goal (2 subgoals):
 1. n\<^sub>1 \<le> n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
 2. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
f n\<^sub>1 @ a = f n\<^sub>2
\<exists>b. f (Suc n\<^sub>2) = f n\<^sub>2 @ [b]
[PROOF STEP]
have "\<exists>b. f n\<^sub>1 @ (a @ [b]) = f (Suc n\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
f n\<^sub>1 @ a = f n\<^sub>2
\<exists>b. f (Suc n\<^sub>2) = f n\<^sub>2 @ [b]

goal (1 subgoal):
 1. \<exists>b. f n\<^sub>1 @ a @ [b] = f (Suc n\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>b. f n\<^sub>1 @ a @ [b] = f (Suc n\<^sub>2)

goal (2 subgoals):
 1. n\<^sub>1 \<le> n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
 2. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>b. f n\<^sub>1 @ a @ [b] = f (Suc n\<^sub>2)
[PROOF STEP]
show "\<exists>c. f n\<^sub>1 @ c = f (Suc n\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
\<exists>b. f n\<^sub>1 @ a @ [b] = f (Suc n\<^sub>2)

goal (1 subgoal):
 1. \<exists>c. f n\<^sub>1 @ c = f (Suc n\<^sub>2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>c. f n\<^sub>1 @ c = f (Suc n\<^sub>2)

goal (1 subgoal):
 1. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
assume "n\<^sub>1 = Suc n\<^sub>2"
[PROOF STATE]
proof (state)
this:
n\<^sub>1 = Suc n\<^sub>2

goal (1 subgoal):
 1. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>1 = Suc n\<^sub>2
[PROOF STEP]
have "f n\<^sub>1 @ [] = f (Suc n\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 = Suc n\<^sub>2

goal (1 subgoal):
 1. f n\<^sub>1 @ [] = f (Suc n\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n\<^sub>1 @ [] = f (Suc n\<^sub>2)

goal (1 subgoal):
 1. n\<^sub>1 = Suc n\<^sub>2 \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f n\<^sub>1 @ [] = f (Suc n\<^sub>2)
[PROOF STEP]
show "\<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
f n\<^sub>1 @ [] = f (Suc n\<^sub>2)

goal (1 subgoal):
 1. \<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. f n\<^sub>1 @ a = f (Suc n\<^sub>2)

goal (1 subgoal):
 1. \<lbrakk>wf_infpath f; n\<^sub>1 \<le> 0\<rbrakk> \<Longrightarrow> \<exists>a. f n\<^sub>1 @ a = f 0
[PROOF STEP]
qed auto


[STATEMENT]
lemma ith_in_extension:
  assumes chain: "wf_infpath f"
  assumes smalli: "i < length (f n\<^sub>1)"
  assumes n\<^sub>1n\<^sub>2: "n\<^sub>1 \<le> n\<^sub>2"
  shows "f n\<^sub>1 ! i = f n\<^sub>2 ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n\<^sub>1 ! i = f n\<^sub>2 ! i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n\<^sub>1 ! i = f n\<^sub>2 ! i
[PROOF STEP]
from chain n\<^sub>1n\<^sub>2
[PROOF STATE]
proof (chain)
picking this:
wf_infpath f
n\<^sub>1 \<le> n\<^sub>2
[PROOF STEP]
have "\<exists>a. f n\<^sub>1 @ a = f n\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
wf_infpath f
n\<^sub>1 \<le> n\<^sub>2

goal (1 subgoal):
 1. \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
[PROOF STEP]
using chain_prefix
[PROOF STATE]
proof (prove)
using this:
wf_infpath f
n\<^sub>1 \<le> n\<^sub>2
\<lbrakk>wf_infpath ?f; ?n\<^sub>1 \<le> ?n\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>a. ?f ?n\<^sub>1 @ a = ?f ?n\<^sub>2

goal (1 subgoal):
 1. \<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a. f n\<^sub>1 @ a = f n\<^sub>2

goal (1 subgoal):
 1. f n\<^sub>1 ! i = f n\<^sub>2 ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. f n\<^sub>1 @ a = f n\<^sub>2
[PROOF STEP]
obtain a where a_p: "f n\<^sub>1 @ a = f n\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. f n\<^sub>1 @ a = f n\<^sub>2

goal (1 subgoal):
 1. (\<And>a. f n\<^sub>1 @ a = f n\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n\<^sub>1 @ a = f n\<^sub>2

goal (1 subgoal):
 1. f n\<^sub>1 ! i = f n\<^sub>2 ! i
[PROOF STEP]
have "(f n\<^sub>1 @ a) ! i = f n\<^sub>1 ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f n\<^sub>1 @ a) ! i = f n\<^sub>1 ! i
[PROOF STEP]
using smalli
[PROOF STATE]
proof (prove)
using this:
i < length (f n\<^sub>1)

goal (1 subgoal):
 1. (f n\<^sub>1 @ a) ! i = f n\<^sub>1 ! i
[PROOF STEP]
by (simp add: nth_append)
[PROOF STATE]
proof (state)
this:
(f n\<^sub>1 @ a) ! i = f n\<^sub>1 ! i

goal (1 subgoal):
 1. f n\<^sub>1 ! i = f n\<^sub>2 ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f n\<^sub>1 @ a) ! i = f n\<^sub>1 ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f n\<^sub>1 @ a) ! i = f n\<^sub>1 ! i

goal (1 subgoal):
 1. f n\<^sub>1 ! i = f n\<^sub>2 ! i
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
(f n\<^sub>1 @ a) ! i = f n\<^sub>1 ! i
f n\<^sub>1 @ a = f n\<^sub>2

goal (1 subgoal):
 1. f n\<^sub>1 ! i = f n\<^sub>2 ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n\<^sub>1 ! i = f n\<^sub>2 ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_subs:
  assumes inf: "\<not>finite(subtree T ds)"
  shows "\<not>finite(subtree T (ds @ [Left])) \<or> \<not>finite(subtree T (ds @ [Right]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
let ?subtree = "subtree T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
assume asms: "finite(?subtree(ds @ [Left]))"
                 "finite(?subtree(ds @ [Right]))"
[PROOF STATE]
proof (state)
this:
finite (subtree T (ds @ [Left]))
finite (subtree T (ds @ [Right]))

goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
have "?subtree ds \<subseteq> ?subtree (ds @ [Left] ) \<union> ?subtree (ds @ [Right]) \<union> {ds} "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtree T ds \<subseteq> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right]) \<union> {ds}
[PROOF STEP]
using subtree_pos
[PROOF STATE]
proof (prove)
using this:
subtree ?T ?ds \<subseteq> subtree ?T (?ds @ [Left]) \<union> subtree ?T (?ds @ [Right]) \<union> {?ds}

goal (1 subgoal):
 1. subtree T ds \<subseteq> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right]) \<union> {ds}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subtree T ds \<subseteq> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right]) \<union> {ds}

goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subtree T ds \<subseteq> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right]) \<union> {ds}
[PROOF STEP]
have "finite(?subtree (ds))"
[PROOF STATE]
proof (prove)
using this:
subtree T ds \<subseteq> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right]) \<union> {ds}

goal (1 subgoal):
 1. finite (subtree T ds)
[PROOF STEP]
using asms
[PROOF STATE]
proof (prove)
using this:
subtree T ds \<subseteq> subtree T (ds @ [Left]) \<union> subtree T (ds @ [Right]) \<union> {ds}
finite (subtree T (ds @ [Left]))
finite (subtree T (ds @ [Right]))

goal (1 subgoal):
 1. finite (subtree T ds)
[PROOF STEP]
by (simp add: finite_subset)
[PROOF STATE]
proof (state)
this:
finite (subtree T ds)

goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite (subtree T (ds @ [Left])); finite (subtree T (ds @ [Right]))\<rbrakk> \<Longrightarrow> finite (subtree T ds)

goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite (subtree T (ds @ [Left])); finite (subtree T (ds @ [Right]))\<rbrakk> \<Longrightarrow> finite (subtree T ds)
[PROOF STEP]
show "\<not>finite(?subtree (ds @ [Left])) \<or> \<not>finite(?subtree (ds @ [Right]))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (subtree T (ds @ [Left])); finite (subtree T (ds @ [Right]))\<rbrakk> \<Longrightarrow> finite (subtree T ds)

goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
using inf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (subtree T (ds @ [Left])); finite (subtree T (ds @ [Right]))\<rbrakk> \<Longrightarrow> finite (subtree T ds)
infinite (subtree T ds)

goal (1 subgoal):
 1. infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infinite (subtree T (ds @ [Left])) \<or> infinite (subtree T (ds @ [Right]))

goal:
No subgoals!
[PROOF STEP]
qed