[STATEMENT]
lemma internal_prefix:
  assumes "internal (ds1@ds2@[d]) T"
  shows "internal ds1 T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal ds1 T
[PROOF STEP]
(* more or less copy paste of path_prefix *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal ds1 T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
internal (ds1 @ ds2 @ [d]) T

goal (1 subgoal):
 1. internal ds1 T
[PROOF STEP]
proof (induction ds1 arbitrary: T)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. internal ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. internal (ds1 @ ds2 @ [d]) T \<Longrightarrow> internal ds1 T; internal ((a # ds1) @ ds2 @ [d]) T\<rbrakk> \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
case (Cons a ds1)
[PROOF STATE]
proof (state)
this:
internal (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T
internal ((a # ds1) @ ds2 @ [d]) T

goal (2 subgoals):
 1. \<And>T. internal ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. internal (ds1 @ ds2 @ [d]) T \<Longrightarrow> internal ds1 T; internal ((a # ds1) @ ds2 @ [d]) T\<rbrakk> \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T
internal ((a # ds1) @ ds2 @ [d]) T
[PROOF STEP]
have "\<exists>l r. T = Branching l r"
[PROOF STATE]
proof (prove)
using this:
internal (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T
internal ((a # ds1) @ ds2 @ [d]) T

goal (1 subgoal):
 1. \<exists>l r. T = Branching l r
[PROOF STEP]
using internal_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
internal (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T
internal ((a # ds1) @ ds2 @ [d]) T
\<not> internal ?b Leaf

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

goal (2 subgoals):
 1. \<And>T. internal ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. internal (ds1 @ ds2 @ [d]) T \<Longrightarrow> internal ds1 T; internal ((a # ds1) @ ds2 @ [d]) T\<rbrakk> \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l r. T = Branching l r
[PROOF STEP]
obtain l r where p_lr: "T = Branching l r"
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. T = Branching l r

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

goal (2 subgoals):
 1. \<And>T. internal ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. internal (ds1 @ ds2 @ [d]) T \<Longrightarrow> internal ds1 T; internal ((a # ds1) @ ds2 @ [d]) T\<rbrakk> \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<Longrightarrow> internal (a # ds1) T
 2. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
assume atrue: "a"
[PROOF STATE]
proof (state)
this:
a

goal (2 subgoals):
 1. a \<Longrightarrow> internal (a # ds1) T
 2. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a
[PROOF STEP]
have "internal ((ds1) @ ds2 @[d]) l"
[PROOF STATE]
proof (prove)
using this:
a

goal (1 subgoal):
 1. internal (ds1 @ ds2 @ [d]) l
[PROOF STEP]
using p_lr Cons(2) internal_inv_Branching
[PROOF STATE]
proof (prove)
using this:
a
T = Branching l r
internal ((a # ds1) @ ds2 @ [d]) T
internal ?p (Branching ?l ?r) = (?p = [] \<or> (\<exists>a p'. ?p = a # p' \<and> (a \<longrightarrow> internal p' ?l) \<and> (\<not> a \<longrightarrow> internal p' ?r)))

goal (1 subgoal):
 1. internal (ds1 @ ds2 @ [d]) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal (ds1 @ ds2 @ [d]) l

goal (2 subgoals):
 1. a \<Longrightarrow> internal (a # ds1) T
 2. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal (ds1 @ ds2 @ [d]) l
[PROOF STEP]
have "internal ds1 l"
[PROOF STATE]
proof (prove)
using this:
internal (ds1 @ ds2 @ [d]) l

goal (1 subgoal):
 1. internal ds1 l
[PROOF STEP]
using Cons(1)
[PROOF STATE]
proof (prove)
using this:
internal (ds1 @ ds2 @ [d]) l
internal (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T

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

goal (2 subgoals):
 1. a \<Longrightarrow> internal (a # ds1) T
 2. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal ds1 l
[PROOF STEP]
show "internal (a # ds1) T"
[PROOF STATE]
proof (prove)
using this:
internal ds1 l

goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
using p_lr atrue
[PROOF STATE]
proof (prove)
using this:
internal ds1 l
T = Branching l r
a

goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal (a # ds1) T

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
assume afalse: "~a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> a
[PROOF STEP]
have "internal ((ds1) @ ds2 @[d]) r"
[PROOF STATE]
proof (prove)
using this:
\<not> a

goal (1 subgoal):
 1. internal (ds1 @ ds2 @ [d]) r
[PROOF STEP]
using p_lr Cons(2) internal_inv_Branching
[PROOF STATE]
proof (prove)
using this:
\<not> a
T = Branching l r
internal ((a # ds1) @ ds2 @ [d]) T
internal ?p (Branching ?l ?r) = (?p = [] \<or> (\<exists>a p'. ?p = a # p' \<and> (a \<longrightarrow> internal p' ?l) \<and> (\<not> a \<longrightarrow> internal p' ?r)))

goal (1 subgoal):
 1. internal (ds1 @ ds2 @ [d]) r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal (ds1 @ ds2 @ [d]) r

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal (ds1 @ ds2 @ [d]) r
[PROOF STEP]
have "internal ds1 r"
[PROOF STATE]
proof (prove)
using this:
internal (ds1 @ ds2 @ [d]) r

goal (1 subgoal):
 1. internal ds1 r
[PROOF STEP]
using Cons(1)
[PROOF STATE]
proof (prove)
using this:
internal (ds1 @ ds2 @ [d]) r
internal (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T

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

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal ds1 r
[PROOF STEP]
show "internal (a # ds1) T"
[PROOF STATE]
proof (prove)
using this:
internal ds1 r

goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
using p_lr afalse
[PROOF STATE]
proof (prove)
using this:
internal ds1 r
T = Branching l r
\<not> a

goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal (a # ds1) T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
internal (a # ds1) T

goal (1 subgoal):
 1. \<And>T. internal ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T. internal ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
[PROOF STEP]
case (Nil)
[PROOF STATE]
proof (state)
this:
internal ([] @ ds2 @ [d]) T

goal (1 subgoal):
 1. \<And>T. internal ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal ([] @ ds2 @ [d]) T
[PROOF STEP]
have "\<exists>l r. T = Branching l r"
[PROOF STATE]
proof (prove)
using this:
internal ([] @ ds2 @ [d]) T

goal (1 subgoal):
 1. \<exists>l r. T = Branching l r
[PROOF STEP]
using internal_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
internal ([] @ ds2 @ [d]) T
\<not> internal ?b Leaf

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

goal (1 subgoal):
 1. \<And>T. internal ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l r. T = Branching l r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. T = Branching l r

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma internal_branch:
  assumes "branch (ds1@ds2@[d]) T"
  shows "internal ds1 T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal ds1 T
[PROOF STEP]
(* more or less copy paste of path_prefix *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal ds1 T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
branch (ds1 @ ds2 @ [d]) T

goal (1 subgoal):
 1. internal ds1 T
[PROOF STEP]
proof (induction ds1 arbitrary: T)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. branch ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. branch (ds1 @ ds2 @ [d]) T \<Longrightarrow> internal ds1 T; branch ((a # ds1) @ ds2 @ [d]) T\<rbrakk> \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
case (Cons a ds1)
[PROOF STATE]
proof (state)
this:
branch (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T
branch ((a # ds1) @ ds2 @ [d]) T

goal (2 subgoals):
 1. \<And>T. branch ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. branch (ds1 @ ds2 @ [d]) T \<Longrightarrow> internal ds1 T; branch ((a # ds1) @ ds2 @ [d]) T\<rbrakk> \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T
branch ((a # ds1) @ ds2 @ [d]) T
[PROOF STEP]
have "\<exists>l r. T = Branching l r"
[PROOF STATE]
proof (prove)
using this:
branch (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T
branch ((a # ds1) @ ds2 @ [d]) T

goal (1 subgoal):
 1. \<exists>l r. T = Branching l r
[PROOF STEP]
using branch_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
branch (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T
branch ((a # ds1) @ ds2 @ [d]) T
branch ?b Leaf = (?b = [])

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

goal (2 subgoals):
 1. \<And>T. branch ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. branch (ds1 @ ds2 @ [d]) T \<Longrightarrow> internal ds1 T; branch ((a # ds1) @ ds2 @ [d]) T\<rbrakk> \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l r. T = Branching l r
[PROOF STEP]
obtain l r where p_lr: "T = Branching l r"
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. T = Branching l r

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

goal (2 subgoals):
 1. \<And>T. branch ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. branch (ds1 @ ds2 @ [d]) T \<Longrightarrow> internal ds1 T; branch ((a # ds1) @ ds2 @ [d]) T\<rbrakk> \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<Longrightarrow> internal (a # ds1) T
 2. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
assume atrue: "a"
[PROOF STATE]
proof (state)
this:
a

goal (2 subgoals):
 1. a \<Longrightarrow> internal (a # ds1) T
 2. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a
[PROOF STEP]
have "branch (ds1 @ ds2 @ [d]) l"
[PROOF STATE]
proof (prove)
using this:
a

goal (1 subgoal):
 1. branch (ds1 @ ds2 @ [d]) l
[PROOF STEP]
using p_lr Cons(2) branch_inv_Branching
[PROOF STATE]
proof (prove)
using this:
a
T = Branching l r
branch ((a # ds1) @ ds2 @ [d]) T
branch ?b (Branching ?l ?r) = (\<exists>a b'. ?b = a # b' \<and> (a \<longrightarrow> branch b' ?l) \<and> (\<not> a \<longrightarrow> branch b' ?r))

goal (1 subgoal):
 1. branch (ds1 @ ds2 @ [d]) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (ds1 @ ds2 @ [d]) l

goal (2 subgoals):
 1. a \<Longrightarrow> internal (a # ds1) T
 2. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (ds1 @ ds2 @ [d]) l
[PROOF STEP]
have "internal ds1 l"
[PROOF STATE]
proof (prove)
using this:
branch (ds1 @ ds2 @ [d]) l

goal (1 subgoal):
 1. internal ds1 l
[PROOF STEP]
using Cons(1)
[PROOF STATE]
proof (prove)
using this:
branch (ds1 @ ds2 @ [d]) l
branch (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T

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

goal (2 subgoals):
 1. a \<Longrightarrow> internal (a # ds1) T
 2. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal ds1 l
[PROOF STEP]
show "internal (a # ds1) T"
[PROOF STATE]
proof (prove)
using this:
internal ds1 l

goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
using p_lr atrue
[PROOF STATE]
proof (prove)
using this:
internal ds1 l
T = Branching l r
a

goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal (a # ds1) T

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
assume afalse: "~a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> a
[PROOF STEP]
have "branch ((ds1) @ ds2 @[d]) r"
[PROOF STATE]
proof (prove)
using this:
\<not> a

goal (1 subgoal):
 1. branch (ds1 @ ds2 @ [d]) r
[PROOF STEP]
using p_lr Cons(2) branch_inv_Branching
[PROOF STATE]
proof (prove)
using this:
\<not> a
T = Branching l r
branch ((a # ds1) @ ds2 @ [d]) T
branch ?b (Branching ?l ?r) = (\<exists>a b'. ?b = a # b' \<and> (a \<longrightarrow> branch b' ?l) \<and> (\<not> a \<longrightarrow> branch b' ?r))

goal (1 subgoal):
 1. branch (ds1 @ ds2 @ [d]) r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (ds1 @ ds2 @ [d]) r

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (ds1 @ ds2 @ [d]) r
[PROOF STEP]
have "internal ds1 r"
[PROOF STATE]
proof (prove)
using this:
branch (ds1 @ ds2 @ [d]) r

goal (1 subgoal):
 1. internal ds1 r
[PROOF STEP]
using Cons(1)
[PROOF STATE]
proof (prove)
using this:
branch (ds1 @ ds2 @ [d]) r
branch (ds1 @ ds2 @ [d]) ?T \<Longrightarrow> internal ds1 ?T

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

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> internal (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal ds1 r
[PROOF STEP]
show "internal (a # ds1) T"
[PROOF STATE]
proof (prove)
using this:
internal ds1 r

goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
using p_lr afalse
[PROOF STATE]
proof (prove)
using this:
internal ds1 r
T = Branching l r
\<not> a

goal (1 subgoal):
 1. internal (a # ds1) T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal (a # ds1) T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
internal (a # ds1) T

goal (1 subgoal):
 1. \<And>T. branch ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T. branch ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
[PROOF STEP]
case (Nil)
[PROOF STATE]
proof (state)
this:
branch ([] @ ds2 @ [d]) T

goal (1 subgoal):
 1. \<And>T. branch ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch ([] @ ds2 @ [d]) T
[PROOF STEP]
have "\<exists>l r. T = Branching l r"
[PROOF STATE]
proof (prove)
using this:
branch ([] @ ds2 @ [d]) T

goal (1 subgoal):
 1. \<exists>l r. T = Branching l r
[PROOF STEP]
using branch_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
branch ([] @ ds2 @ [d]) T
branch ?b Leaf = (?b = [])

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

goal (1 subgoal):
 1. \<And>T. branch ([] @ ds2 @ [d]) T \<Longrightarrow> internal [] T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l r. T = Branching l r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. T = Branching l r

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delete_Leaf: "delete T Leaf = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delete T Leaf = Leaf
[PROOF STEP]
by (cases T) auto


[STATEMENT]
lemma path_delete:
  assumes "path p (delete ds T)"
  shows "path p T "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path p T
[PROOF STEP]
(* What a huge proof... But the four cases can be proven shorter *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path p T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path p (delete ds T)

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

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

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

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p (delete ?ds ?T) \<Longrightarrow> path p ?T
path (a # p) (delete ds T)
[PROOF STEP]
obtain b ds' where bds'_p: "ds=b#ds'"
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> path p ?T
path (a # p) (delete ds T)

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
have "\<exists>dT1 dT2. delete ds T = Branching dT1 dT2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>dT1 dT2. delete ds T = Branching dT1 dT2
[PROOF STEP]
using Cons path_inv_Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> path p ?T
path (a # p) (delete ds T)
path (?a # ?ds) ?T \<longrightarrow> (\<exists>l r. ?T = Branching l r)

goal (1 subgoal):
 1. \<exists>dT1 dT2. delete ds T = Branching dT1 dT2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>dT1 dT2. delete ds T = Branching dT1 dT2

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

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

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

goal (1 subgoal):
 1. \<exists>T1 T2. T = Branching T1 T2
[PROOF STEP]
(* Is there a lemma hidden here that I could extract? *)
[PROOF STATE]
proof (prove)
using this:
delete ds T = Branching dT1 dT2

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) 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 ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
T = Branching T1 T2

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
assume a_p: "a"
[PROOF STATE]
proof (state)
this:
a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
assume b_p: "\<not>b"
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
have "path (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> path p ?T
path (a # p) (delete ds T)

goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
path (a # p) (delete ds T)

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

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

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

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

goal (1 subgoal):
 1. path p T1
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (Branching T1 (delete ds' T2))
a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p T1
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
path p T1

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

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
assume a_p: "\<not>a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
assume b_p: "b"
[PROOF STATE]
proof (state)
this:
b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
have "path (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> path p ?T
path (a # p) (delete ds T)

goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
path (a # p) (delete ds T)

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

goal (1 subgoal):
 1. path (a # p) (Branching (delete ds' T1) T2)
[PROOF STEP]
using b_p bds'_p T1T2_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (delete ds T)
b
ds = b # ds'
T = Branching T1 T2

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

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

goal (1 subgoal):
 1. path p T2
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (Branching (delete ds' T1) T2)
\<not> a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p T2
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
path p T2

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

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
assume a_p: "a"
[PROOF STATE]
proof (state)
this:
a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
assume b_p: "b"
[PROOF STATE]
proof (state)
this:
b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
have "path (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> path p ?T
path (a # p) (delete ds T)

goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
path (a # p) (delete ds T)

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

goal (1 subgoal):
 1. path (a # p) (Branching (delete ds' T1) T2)
[PROOF STEP]
using b_p bds'_p T1T2_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (delete ds T)
b
ds = b # ds'
T = Branching T1 T2

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

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

goal (1 subgoal):
 1. path p (delete ds' T1)
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (Branching (delete ds' T1) T2)
a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p (delete ds' T1)
[PROOF STEP]
have "path p T1"
[PROOF STATE]
proof (prove)
using this:
path p (delete ds' T1)

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

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p T1
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
path p T1

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

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
assume a_p: "\<not>a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
assume b_p: "\<not>b"
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
have "path (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> path p ?T
path (a # p) (delete ds T)

goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
path (a # p) (delete ds T)

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

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

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

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

goal (1 subgoal):
 1. path p (delete ds' T2)
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (Branching T1 (delete ds' T2))
\<not> a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p (delete ds' T2)
[PROOF STEP]
have "path p T2"
[PROOF STATE]
proof (prove)
using this:
path p (delete ds' T2)

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

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p T2
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
path p T2

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

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> path p T; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> path (a # p) T
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> path (a # p) T
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> path (a # p) T
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> path (a # p) T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> path (a # p) T
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> path (a # p) T
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> path (a # p) T
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> path (a # p) T

goal (1 subgoal):
 1. path (a # p) T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path (a # p) T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma branch_delete:
  assumes "branch p (delete ds T)"
  shows "branch p T \<or> p=ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch p T \<or> p = ds
[PROOF STEP]
(* Adapted from above *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch p T \<or> p = ds
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
branch p (delete ds T)

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

goal (2 subgoals):
 1. \<And>T ds. branch [] (delete ds T) \<Longrightarrow> branch [] T \<or> [] = ds
 2. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch [] (delete ds T)
[PROOF STEP]
have "delete ds T = Leaf"
[PROOF STATE]
proof (prove)
using this:
branch [] (delete ds T)

goal (1 subgoal):
 1. delete ds T = Leaf
[PROOF STEP]
by (cases "delete ds T") auto
[PROOF STATE]
proof (state)
this:
delete ds T = Leaf

goal (2 subgoals):
 1. \<And>T ds. branch [] (delete ds T) \<Longrightarrow> branch [] T \<or> [] = ds
 2. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
delete ds T = Leaf
[PROOF STEP]
have "ds = [] \<or> T = Leaf"
[PROOF STATE]
proof (prove)
using this:
delete ds T = Leaf

goal (1 subgoal):
 1. ds = [] \<or> T = Leaf
[PROOF STEP]
using delete.elims
[PROOF STATE]
proof (prove)
using this:
delete ds T = Leaf
\<lbrakk>delete ?x ?xa = ?y; \<And>T. \<lbrakk>?x = []; ?xa = T; ?y = Leaf\<rbrakk> \<Longrightarrow> ?P; \<And>ds T\<^sub>1 T\<^sub>2. \<lbrakk>?x = True # ds; ?xa = Branching T\<^sub>1 T\<^sub>2; ?y = Branching (delete ds T\<^sub>1) T\<^sub>2\<rbrakk> \<Longrightarrow> ?P; \<And>ds T\<^sub>1 T\<^sub>2. \<lbrakk>?x = False # ds; ?xa = Branching T\<^sub>1 T\<^sub>2; ?y = Branching T\<^sub>1 (delete ds T\<^sub>2)\<rbrakk> \<Longrightarrow> ?P; \<And>a ds. \<lbrakk>?x = a # ds; ?xa = Leaf; ?y = Leaf\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. ds = [] \<or> T = Leaf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ds = [] \<or> T = Leaf

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

goal (1 subgoal):
 1. branch [] T \<or> [] = ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch [] T \<or> [] = ds

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch p (delete ?ds ?T) \<Longrightarrow> branch p ?T \<or> p = ?ds
branch (a # p) (delete ds T)
[PROOF STEP]
obtain b ds' where bds'_p: "ds=b#ds'"
[PROOF STATE]
proof (prove)
using this:
branch p (delete ?ds ?T) \<Longrightarrow> branch p ?T \<or> p = ?ds
branch (a # p) (delete ds T)

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
have "\<exists>dT1 dT2. delete ds T = Branching dT1 dT2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>dT1 dT2. delete ds T = Branching dT1 dT2
[PROOF STEP]
using Cons path_inv_Cons branch_is_path
[PROOF STATE]
proof (prove)
using this:
branch p (delete ?ds ?T) \<Longrightarrow> branch p ?T \<or> p = ?ds
branch (a # p) (delete ds T)
path (?a # ?ds) ?T \<longrightarrow> (\<exists>l r. ?T = Branching l r)
branch ?ds ?T \<Longrightarrow> path ?ds ?T

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>dT1 dT2. delete ds T = Branching dT1 dT2
[PROOF STEP]
obtain dT1 dT2 where "delete ds T = Branching dT1 dT2"
[PROOF STATE]
proof (prove)
using this:
\<exists>dT1 dT2. delete ds T = Branching dT1 dT2

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

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

goal (1 subgoal):
 1. \<exists>T1 T2. T = Branching T1 T2
[PROOF STEP]
(* Is there a lemma hidden here that I could extract? *)
[PROOF STATE]
proof (prove)
using this:
delete ds T = Branching dT1 dT2

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[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 ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
T = Branching T1 T2

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
assume a_p: "a"
[PROOF STATE]
proof (state)
this:
a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
assume b_p: "\<not>b"
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
have "branch (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
branch p (delete ?ds ?T) \<Longrightarrow> branch p ?T \<or> p = ?ds
branch (a # p) (delete ds T)

goal (1 subgoal):
 1. branch (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
branch (a # p) (delete ds T)

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

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

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

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

goal (1 subgoal):
 1. branch p T1
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
branch (a # p) (Branching T1 (delete ds' T2))
a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch p T1
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
branch p T1

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

goal (1 subgoal):
 1. branch (a # p) T \<or> a # p = ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
assume a_p: "\<not>a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
assume b_p: "b"
[PROOF STATE]
proof (state)
this:
b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
have "branch (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
branch p (delete ?ds ?T) \<Longrightarrow> branch p ?T \<or> p = ?ds
branch (a # p) (delete ds T)

goal (1 subgoal):
 1. branch (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
branch (a # p) (delete ds T)

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

goal (1 subgoal):
 1. branch (a # p) (Branching (delete ds' T1) T2)
[PROOF STEP]
using b_p bds'_p T1T2_p
[PROOF STATE]
proof (prove)
using this:
branch (a # p) (delete ds T)
b
ds = b # ds'
T = Branching T1 T2

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

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

goal (1 subgoal):
 1. branch p T2
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
branch (a # p) (Branching (delete ds' T1) T2)
\<not> a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch p T2
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
branch p T2

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

goal (1 subgoal):
 1. branch (a # p) T \<or> a # p = ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
assume a_p: "a"
[PROOF STATE]
proof (state)
this:
a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
assume b_p: "b"
[PROOF STATE]
proof (state)
this:
b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
have "branch (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
branch p (delete ?ds ?T) \<Longrightarrow> branch p ?T \<or> p = ?ds
branch (a # p) (delete ds T)

goal (1 subgoal):
 1. branch (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
branch (a # p) (delete ds T)

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

goal (1 subgoal):
 1. branch (a # p) (Branching (delete ds' T1) T2)
[PROOF STEP]
using b_p bds'_p T1T2_p
[PROOF STATE]
proof (prove)
using this:
branch (a # p) (delete ds T)
b
ds = b # ds'
T = Branching T1 T2

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

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

goal (1 subgoal):
 1. branch p (delete ds' T1)
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
branch (a # p) (Branching (delete ds' T1) T2)
a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch p (delete ds' T1)
[PROOF STEP]
have "branch p T1 \<or> p = ds'"
[PROOF STATE]
proof (prove)
using this:
branch p (delete ds' T1)

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

goal (1 subgoal):
 1. branch p T1 \<or> p = ds'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
branch p T1 \<or> p = ds'

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch p T1 \<or> p = ds'
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
branch p T1 \<or> p = ds'

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

goal (1 subgoal):
 1. branch (a # p) T \<or> a # p = ds
[PROOF STEP]
using bds'_p a_p b_p
[PROOF STATE]
proof (prove)
using this:
branch p T1 \<or> p = ds'
T = Branching T1 T2
a
ds = b # ds'
a
b

goal (1 subgoal):
 1. branch (a # p) T \<or> a # p = ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
assume a_p: "\<not>a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
assume b_p: "\<not>b"
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
have "branch (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
branch p (delete ?ds ?T) \<Longrightarrow> branch p ?T \<or> p = ?ds
branch (a # p) (delete ds T)

goal (1 subgoal):
 1. branch (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
branch (a # p) (delete ds T)

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

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

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

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

goal (1 subgoal):
 1. branch p (delete ds' T2)
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
branch (a # p) (Branching T1 (delete ds' T2))
\<not> a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch p (delete ds' T2)
[PROOF STEP]
have "branch p T2 \<or> p = ds'"
[PROOF STATE]
proof (prove)
using this:
branch p (delete ds' T2)

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

goal (1 subgoal):
 1. branch p T2 \<or> p = ds'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
branch p T2 \<or> p = ds'

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch p T2 \<or> p = ds'
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
branch p T2 \<or> p = ds'

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

goal (1 subgoal):
 1. branch (a # p) T \<or> a # p = ds
[PROOF STEP]
using bds'_p a_p b_p
[PROOF STATE]
proof (prove)
using this:
branch p T2 \<or> p = ds'
T = Branching T1 T2
\<not> a
ds = b # ds'
\<not> a
\<not> b

goal (1 subgoal):
 1. branch (a # p) T \<or> a # p = ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. branch p (delete ds T) \<Longrightarrow> branch p T \<or> p = ds; branch (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> branch (a # p) T \<or> a # p = ds

goal (1 subgoal):
 1. branch (a # p) T \<or> a # p = ds
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
branch (a # p) T \<or> a # p = ds

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma branch_delete_postfix:
  assumes "path p (delete ds T)"
  shows "\<not>(\<exists>c cs. p = ds @ c#cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>c cs. p = ds @ c # cs
[PROOF STEP]
(* Adapted from previous proof *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>c cs. p = ds @ c # cs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path p (delete ds T)

goal (1 subgoal):
 1. \<nexists>c cs. p = ds @ c # cs
[PROOF STEP]
proof (induction p arbitrary: T ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T ds. path [] (delete ds T) \<Longrightarrow> \<nexists>c cs. [] = ds @ c # cs
 2. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
path [] (delete ds T)

goal (2 subgoals):
 1. \<And>T ds. path [] (delete ds T) \<Longrightarrow> \<nexists>c cs. [] = ds @ c # cs
 2. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path [] (delete ds T)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path [] (delete ds T)

goal (1 subgoal):
 1. \<nexists>c cs. [] = ds @ c # cs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<nexists>c cs. [] = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
path p (delete ?ds ?T) \<Longrightarrow> \<nexists>c cs. p = ?ds @ c # cs
path (a # p) (delete ds T)

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p (delete ?ds ?T) \<Longrightarrow> \<nexists>c cs. p = ?ds @ c # cs
path (a # p) (delete ds T)
[PROOF STEP]
obtain b ds' where bds'_p: "ds=b#ds'"
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> \<nexists>c cs. p = ?ds @ c # cs
path (a # p) (delete ds T)

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
have "\<exists>dT1 dT2. delete ds T = Branching dT1 dT2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>dT1 dT2. delete ds T = Branching dT1 dT2
[PROOF STEP]
using Cons path_inv_Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> \<nexists>c cs. p = ?ds @ c # cs
path (a # p) (delete ds T)
path (?a # ?ds) ?T \<longrightarrow> (\<exists>l r. ?T = Branching l r)

goal (1 subgoal):
 1. \<exists>dT1 dT2. delete ds T = Branching dT1 dT2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>dT1 dT2. delete ds T = Branching dT1 dT2

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>dT1 dT2. delete ds T = Branching dT1 dT2
[PROOF STEP]
obtain dT1 dT2 where "delete ds T = Branching dT1 dT2"
[PROOF STATE]
proof (prove)
using this:
\<exists>dT1 dT2. delete ds T = Branching dT1 dT2

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
delete ds T = Branching dT1 dT2
[PROOF STEP]
have "\<exists>T1 T2. T=Branching T1 T2"
[PROOF STATE]
proof (prove)
using this:
delete ds T = Branching dT1 dT2

goal (1 subgoal):
 1. \<exists>T1 T2. T = Branching T1 T2
[PROOF STEP]
(* Is there a lemma hidden here that I could extract? *)
[PROOF STATE]
proof (prove)
using this:
delete ds T = Branching dT1 dT2

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[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 ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
T = Branching T1 T2

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
assume a_p: "a"
[PROOF STATE]
proof (state)
this:
a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
assume b_p: "\<not>b"
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> b
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
\<not> b

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
using T1T2_p a_p b_p bds'_p
[PROOF STATE]
proof (prove)
using this:
\<not> b
T = Branching T1 T2
a
\<not> b
ds = b # ds'

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
assume a_p: "\<not>a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
assume b_p: "b"
[PROOF STATE]
proof (state)
this:
b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
b

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
using T1T2_p a_p b_p bds'_p
[PROOF STATE]
proof (prove)
using this:
b
T = Branching T1 T2
\<not> a
b
ds = b # ds'

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
assume a_p: "a"
[PROOF STATE]
proof (state)
this:
a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
assume b_p: "b"
[PROOF STATE]
proof (state)
this:
b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
have "path (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> \<nexists>c cs. p = ?ds @ c # cs
path (a # p) (delete ds T)

goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
path (a # p) (delete ds T)

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (a # p) (delete ds T)
[PROOF STEP]
have "path (a # p) (Branching (delete ds' T1) T2)"
[PROOF STATE]
proof (prove)
using this:
path (a # p) (delete ds T)

goal (1 subgoal):
 1. path (a # p) (Branching (delete ds' T1) T2)
[PROOF STEP]
using b_p bds'_p T1T2_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (delete ds T)
b
ds = b # ds'
T = Branching T1 T2

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (a # p) (Branching (delete ds' T1) T2)
[PROOF STEP]
have "path p (delete ds' T1)"
[PROOF STATE]
proof (prove)
using this:
path (a # p) (Branching (delete ds' T1) T2)

goal (1 subgoal):
 1. path p (delete ds' T1)
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (Branching (delete ds' T1) T2)
a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p (delete ds' T1)
[PROOF STEP]
have "\<not> (\<exists>c cs. p = ds' @ c # cs)"
[PROOF STATE]
proof (prove)
using this:
path p (delete ds' T1)

goal (1 subgoal):
 1. \<nexists>c cs. p = ds' @ c # cs
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ds' T1)
path p (delete ?ds ?T) \<Longrightarrow> \<nexists>c cs. p = ?ds @ c # cs
path (a # p) (delete ds T)

goal (1 subgoal):
 1. \<nexists>c cs. p = ds' @ c # cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>c cs. p = ds' @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>c cs. p = ds' @ c # cs
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
\<nexists>c cs. p = ds' @ c # cs

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
using T1T2_p a_p b_p bds'_p
[PROOF STATE]
proof (prove)
using this:
\<nexists>c cs. p = ds' @ c # cs
T = Branching T1 T2
a
b
ds = b # ds'

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
assume a_p: "\<not>a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
assume b_p: "\<not>b"
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
have "path (a # p) (delete ds T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ?ds ?T) \<Longrightarrow> \<nexists>c cs. p = ?ds @ c # cs
path (a # p) (delete ds T)

goal (1 subgoal):
 1. path (a # p) (delete ds T)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
path (a # p) (delete ds T)

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (a # p) (delete ds T)
[PROOF STEP]
have "path (a # p) (Branching T1 (delete ds' T2))"
[PROOF STATE]
proof (prove)
using this:
path (a # p) (delete ds T)

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

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (a # p) (Branching T1 (delete ds' T2))
[PROOF STEP]
have "path p (delete ds' T2)"
[PROOF STATE]
proof (prove)
using this:
path (a # p) (Branching T1 (delete ds' T2))

goal (1 subgoal):
 1. path p (delete ds' T2)
[PROOF STEP]
using a_p
[PROOF STATE]
proof (prove)
using this:
path (a # p) (Branching T1 (delete ds' T2))
\<not> a

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

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p (delete ds' T2)
[PROOF STEP]
have "\<not> (\<exists>c cs. p = ds' @ c # cs)"
[PROOF STATE]
proof (prove)
using this:
path p (delete ds' T2)

goal (1 subgoal):
 1. \<nexists>c cs. p = ds' @ c # cs
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
path p (delete ds' T2)
path p (delete ?ds ?T) \<Longrightarrow> \<nexists>c cs. p = ?ds @ c # cs
path (a # p) (delete ds T)

goal (1 subgoal):
 1. \<nexists>c cs. p = ds' @ c # cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>c cs. p = ds' @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>c cs. p = ds' @ c # cs
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
\<nexists>c cs. p = ds' @ c # cs

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
using T1T2_p a_p b_p bds'_p
[PROOF STATE]
proof (prove)
using this:
\<nexists>c cs. p = ds' @ c # cs
T = Branching T1 T2
\<not> a
\<not> b
ds = b # ds'

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<And>a p T ds. \<lbrakk>\<And>T ds. path p (delete ds T) \<Longrightarrow> \<nexists>c cs. p = ds @ c # cs; path (a # p) (delete ds T)\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
\<lbrakk>\<not> a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
\<lbrakk>a; b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs
\<lbrakk>\<not> a; \<not> b\<rbrakk> \<Longrightarrow> \<nexists>c cs. a # p = ds @ c # cs

goal (1 subgoal):
 1. \<nexists>c cs. a # p = ds @ c # cs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<nexists>c cs. a # p = ds @ c # cs

goal:
No subgoals!
[PROOF STEP]
qed