[STATEMENT]
lemma has_branch: "\<exists>b. branch b T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. branch b T
[PROOF STEP]
proof (induction T)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>b. branch b Leaf
 2. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
case (Leaf)
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. \<exists>b. branch b Leaf
 2. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
have "branch [] Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch [] Leaf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch [] Leaf

goal (2 subgoals):
 1. \<exists>b. branch b Leaf
 2. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch [] Leaf
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
branch [] Leaf

goal (1 subgoal):
 1. \<exists>b. branch b Leaf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b. branch b Leaf

goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
case (Branching T\<^sub>1 T\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<exists>b. branch b T\<^sub>1
\<exists>b. branch b T\<^sub>2

goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>b. branch b T\<^sub>1
\<exists>b. branch b T\<^sub>2
[PROOF STEP]
obtain b where "branch b T\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>b. branch b T\<^sub>1
\<exists>b. branch b T\<^sub>2

goal (1 subgoal):
 1. (\<And>b. branch b T\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch b T\<^sub>1

goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch b T\<^sub>1
[PROOF STEP]
have "branch (Left#b) (Branching T\<^sub>1 T\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
branch b T\<^sub>1

goal (1 subgoal):
 1. branch (Left # b) (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (Left # b) (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (Left # b) (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
branch (Left # b) (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. \<exists>b. branch b (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b. branch b (Branching T\<^sub>1 T\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed