[STATEMENT]
lemma combine_forward:
  assumes "dom_children (Node r {|(t1,e1)|}) T"
      and "\<forall>v \<in> dverts (Node r {|(t1,e1)|}). forward v"
      and "wf_dlverts (Node r {|(t1,e1)|})"
      and "v \<in> dverts (Node (r@Dtree.root t1) (sucs t1))"
    shows "forward v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. forward v
[PROOF STEP]
proof(cases "v = r @ Dtree.root t1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v = r @ dtree.root t1

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
have 0: "(Dtree.root t1) \<in> dverts t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dtree.root t1 \<in> dverts t1
[PROOF STEP]
by (simp add: dtree.set_sel(1))
[PROOF STATE]
proof (state)
this:
dtree.root t1 \<in> dverts t1

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dtree.root t1 \<in> dverts t1
[PROOF STEP]
have fwd_t1: "forward (Dtree.root t1)"
[PROOF STATE]
proof (prove)
using this:
dtree.root t1 \<in> dverts t1

goal (1 subgoal):
 1. forward (dtree.root t1)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
dtree.root t1 \<in> dverts t1
Ball (dverts (Node r {|(t1, e1)|})) forward

goal (1 subgoal):
 1. forward (dtree.root t1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
forward (dtree.root t1)

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
forward (dtree.root t1)

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
have "set r \<inter> set (Dtree.root t1) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set r \<inter> set (dtree.root t1) = {}
[PROOF STEP]
using assms(3) 0 lverts_if_in_verts
[PROOF STATE]
proof (prove)
using this:
wf_dlverts (Node r {|(t1, e1)|})
dtree.root t1 \<in> dverts t1
\<lbrakk>?v \<in> dverts ?t; ?x \<in> set ?v\<rbrakk> \<Longrightarrow> ?x \<in> dlverts ?t

goal (1 subgoal):
 1. set r \<inter> set (dtree.root t1) = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set r \<inter> set (dtree.root t1) = {}

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set r \<inter> set (dtree.root t1) = {}

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
have "\<exists>x\<in>set r. \<exists>y\<in>set (Dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
using assms(1,3) root_arc_if_dom_wfdlverts
[PROOF STATE]
proof (prove)
using this:
dom_children (Node r {|(t1, e1)|}) T
wf_dlverts (Node r {|(t1, e1)|})
\<lbrakk>dom_children (Node ?r ?xs) ?T; ?t1.0 \<in> fst ` fset ?xs; wf_dlverts (Node ?r ?xs)\<rbrakk> \<Longrightarrow> \<exists>x\<in>set ?r. \<exists>y\<in>set (dtree.root ?t1.0). x \<rightarrow>\<^bsub>?T\<^esub> y

goal (1 subgoal):
 1. \<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
forward (dtree.root t1)
set r \<inter> set (dtree.root t1) = {}
\<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
have "\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (Dtree.root t1)"
[PROOF STATE]
proof (prove)
using this:
forward (dtree.root t1)
set r \<inter> set (dtree.root t1) = {}
\<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. \<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
[PROOF STEP]
using forward_arc_to_head
[PROOF STATE]
proof (prove)
using this:
forward (dtree.root t1)
set r \<inter> set (dtree.root t1) = {}
\<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y
\<lbrakk>forward ?ys; set ?xs \<inter> set ?ys = {}; ?x \<in> set ?xs; ?y \<in> set ?ys; ?x \<rightarrow>\<^bsub>T\<^esub> ?y\<rbrakk> \<Longrightarrow> ?y = hd ?ys

goal (1 subgoal):
 1. \<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
have fwd_r: "forward r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. forward r
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
Ball (dverts (Node r {|(t1, e1)|})) forward

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

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
forward r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
forward r

goal (1 subgoal):
 1. forward v
[PROOF STEP]
using forward_app fwd_t1 True
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
forward r
\<lbrakk>forward ?s1.0; forward ?s2.0; \<exists>x\<in>set ?s1.0. x \<rightarrow>\<^bsub>T\<^esub> hd ?s2.0\<rbrakk> \<Longrightarrow> forward (?s1.0 @ ?s2.0)
forward (dtree.root t1)
v = r @ dtree.root t1

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

goal (1 subgoal):
 1. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> r @ dtree.root t1

goal (1 subgoal):
 1. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> r @ dtree.root t1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<noteq> r @ dtree.root t1

goal (1 subgoal):
 1. forward v
[PROOF STEP]
using assms(2,4) dverts_suc_subseteq
[PROOF STATE]
proof (prove)
using this:
v \<noteq> r @ dtree.root t1
Ball (dverts (Node r {|(t1, e1)|})) forward
v \<in> dverts (Node (r @ dtree.root t1) (sucs t1))
?x \<in> fst ` fset (sucs ?t) \<Longrightarrow> dverts ?x \<subseteq> dverts ?t

goal (1 subgoal):
 1. forward v
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
forward v

goal:
No subgoals!
[PROOF STEP]
qed