[STATEMENT]
lemma sum_nodes: "inorder t = [i..j] \<Longrightarrow>
  (\<Sum>xy\<in>nodes t. (f(fst xy) :: nat)) = sum f {i..j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inorder t = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t. f (fst xy)) = sum f {i..j}
[PROOF STEP]
proof(induction t arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. inorder \<langle>\<rangle> = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>\<rangle>. f (fst xy)) = sum f {i..j}
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
inorder \<langle>\<rangle> = [i..j]

goal (2 subgoals):
 1. \<And>i j. inorder \<langle>\<rangle> = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>\<rangle>. f (fst xy)) = sum f {i..j}
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
inorder \<langle>\<rangle> = [i..j]

goal (1 subgoal):
 1. (\<Sum>xy\<in>nodes \<langle>\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>xy\<in>nodes \<langle>\<rangle>. f (fst xy)) = sum f {i..j}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
case (Node l k r)
[PROOF STATE]
proof (state)
this:
inorder l = [?i..?j] \<Longrightarrow> (\<Sum>xy\<in>nodes l. f (fst xy)) = sum f {?i..?j}
inorder r = [?i..?j] \<Longrightarrow> (\<Sum>xy\<in>nodes r. f (fst xy)) = sum f {?i..?j}
inorder \<langle>l, k, r\<rangle> = [i..j]

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
note inorder = inorder_upto_split[OF Node.prems(1)]
[PROOF STATE]
proof (state)
this:
inorder l = [i..k - 1]
inorder r = [k + 1..j]
i \<le> k
k \<le> j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
let ?Nl = "nodes l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
let ?Nr = "nodes r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
let ?N = "?Nl \<union> ?Nr"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
have "(fst ` ?Nl) \<inter> (fst ` ?Nr) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` nodes l \<inter> fst ` nodes r = {}
[PROOF STEP]
using inorder(1,2)
[PROOF STATE]
proof (prove)
using this:
inorder l = [i..k - 1]
inorder r = [k + 1..j]

goal (1 subgoal):
 1. fst ` nodes l \<inter> fst ` nodes r = {}
[PROOF STEP]
by(simp add: fst_nodes del: set_inorder add: set_inorder[symmetric])
[PROOF STATE]
proof (state)
this:
fst ` nodes l \<inter> fst ` nodes r = {}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
hence n0: "?Nl \<inter> ?Nr = {}"
[PROOF STATE]
proof (prove)
using this:
fst ` nodes l \<inter> fst ` nodes r = {}

goal (1 subgoal):
 1. nodes l \<inter> nodes r = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes l \<inter> nodes r = {}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
have "(\<Sum>xy\<in>nodes(Node l k r). (f (fst xy) :: nat))
    = (\<Sum>xy\<in>insert (k, Suc 0) (incr2 ` (nodes l \<union> nodes r)). f(fst xy))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xy\<in>nodes \<langle>l, k, r\<rangle>. f (fst xy)) = (\<Sum>xy\<in>insert (k, Suc 0) (incr2 ` (nodes l \<union> nodes r)). f (fst xy))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
(\<Sum>xy\<in>nodes \<langle>l, k, r\<rangle>. f (fst xy)) = (\<Sum>xy\<in>insert (k, Suc 0) (incr2 ` (nodes l \<union> nodes r)). f (fst xy))

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>xy\<in>nodes \<langle>l, k, r\<rangle>. f (fst xy)) = (\<Sum>xy\<in>insert (k, Suc 0) (incr2 ` (nodes l \<union> nodes r)). f (fst xy))

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
have "\<dots> = f k + (\<Sum>xy\<in>(incr2 ` (nodes l \<union> nodes r)). f(fst xy))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xy\<in>insert (k, Suc 0) (incr2 ` (nodes l \<union> nodes r)). f (fst xy)) = f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy))
[PROOF STEP]
by(subst sum.insert, auto simp: finite_nodes notin_nodes0)
[PROOF STATE]
proof (state)
this:
(\<Sum>xy\<in>insert (k, Suc 0) (incr2 ` (nodes l \<union> nodes r)). f (fst xy)) = f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy))

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>xy\<in>insert (k, Suc 0) (incr2 ` (nodes l \<union> nodes r)). f (fst xy)) = f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy))

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
have "\<dots> = sum f {i..j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy)) = sum f {i..j}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy)) = sum f {i..j}
[PROOF STEP]
have "{i..j} = {i..k-1} \<union> {k} \<union> {k+1..j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i..j} = {i..k - 1} \<union> {k} \<union> {k + 1..j}
[PROOF STEP]
using inorder(3,4)
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k \<le> j

goal (1 subgoal):
 1. {i..j} = {i..k - 1} \<union> {k} \<union> {k + 1..j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i..j} = {i..k - 1} \<union> {k} \<union> {k + 1..j}

goal (1 subgoal):
 1. f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy)) = sum f {i..j}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{i..j} = {i..k - 1} \<union> {k} \<union> {k + 1..j}

goal (1 subgoal):
 1. f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy)) = sum f {i..j}
[PROOF STEP]
using Node.IH(1)[OF inorder(1)] Node.IH(2)[OF inorder(2)] inorder(3,4)
[PROOF STATE]
proof (prove)
using this:
{i..j} = {i..k - 1} \<union> {k} \<union> {k + 1..j}
(\<Sum>xy\<in>nodes l. f (fst xy)) = sum f {i..k - 1}
(\<Sum>xy\<in>nodes r. f (fst xy)) = sum f {k + 1..j}
i \<le> k
k \<le> j

goal (1 subgoal):
 1. f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy)) = sum f {i..j}
[PROOF STEP]
by(simp add: sum_incr2 sum_Un_nat finite_nodes n0)
[PROOF STATE]
proof (state)
this:
f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy)) = sum f {i..j}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f k + (\<Sum>xy\<in>incr2 ` (nodes l \<union> nodes r). f (fst xy)) = sum f {i..j}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t1. f (fst xy)) = sum f {i..j}; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> (\<Sum>xy\<in>nodes t2. f (fst xy)) = sum f {i..j}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> (\<Sum>xy\<in>nodes \<langle>t1, x2, t2\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>xy\<in>nodes \<langle>l, k, r\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>xy\<in>nodes \<langle>l, k, r\<rangle>. f (fst xy)) = sum f {i..j}

goal (1 subgoal):
 1. (\<Sum>xy\<in>nodes \<langle>l, k, r\<rangle>. f (fst xy)) = sum f {i..j}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>xy\<in>nodes \<langle>l, k, r\<rangle>. f (fst xy)) = sum f {i..j}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "inorder t = [i..j] \<Longrightarrow> wpl i j t = Wpl i t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inorder t = [i..j] \<Longrightarrow> wpl i j t = Wpl i t
[PROOF STEP]
proof(induction t arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. inorder \<langle>\<rangle> = [i..j] \<Longrightarrow> wpl i j \<langle>\<rangle> = Wpl i \<langle>\<rangle>
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
inorder \<langle>\<rangle> = [i..j]

goal (2 subgoals):
 1. \<And>i j. inorder \<langle>\<rangle> = [i..j] \<Longrightarrow> wpl i j \<langle>\<rangle> = Wpl i \<langle>\<rangle>
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
inorder \<langle>\<rangle> = [i..j]

goal (1 subgoal):
 1. wpl i j \<langle>\<rangle> = Wpl i \<langle>\<rangle>
[PROOF STEP]
by(simp add: Wpl_def)
[PROOF STATE]
proof (state)
this:
wpl i j \<langle>\<rangle> = Wpl i \<langle>\<rangle>

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
case (Node l k r)
[PROOF STATE]
proof (state)
this:
inorder l = [?i..?j] \<Longrightarrow> wpl ?i ?j l = Wpl ?i l
inorder r = [?i..?j] \<Longrightarrow> wpl ?i ?j r = Wpl ?i r
inorder \<langle>l, k, r\<rangle> = [i..j]

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
let ?b = "\<lambda>(k,c). c * b k"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
let ?a = "\<lambda>(k,c). c * a k"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
note inorder = inorder_upto_split[OF Node.prems]
[PROOF STATE]
proof (state)
this:
inorder l = [i..k - 1]
inorder r = [k + 1..j]
i \<le> k
k \<le> j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
let ?Nl = "nodes l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
let ?Nr = "nodes r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
let ?N = "?Nl \<union> ?Nr"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
let ?Ll = "leaves i l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
let ?Lr = "leaves (k+1) r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
let ?L = "?Ll \<union> ?Lr"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "(fst ` ?Nl) \<inter> (fst ` ?Nr) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` nodes l \<inter> fst ` nodes r = {}
[PROOF STEP]
using inorder(1,2)
[PROOF STATE]
proof (prove)
using this:
inorder l = [i..k - 1]
inorder r = [k + 1..j]

goal (1 subgoal):
 1. fst ` nodes l \<inter> fst ` nodes r = {}
[PROOF STEP]
by(simp add: fst_nodes del: set_inorder add: set_inorder[symmetric])
[PROOF STATE]
proof (state)
this:
fst ` nodes l \<inter> fst ` nodes r = {}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
hence n0: "?Nl \<inter> ?Nr = {}"
[PROOF STATE]
proof (prove)
using this:
fst ` nodes l \<inter> fst ` nodes r = {}

goal (1 subgoal):
 1. nodes l \<inter> nodes r = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes l \<inter> nodes r = {}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "fst ` ?Ll \<inter> fst ` ?Lr = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` leaves i l \<inter> fst ` leaves (k + 1) r = {}
[PROOF STEP]
using inorder
[PROOF STATE]
proof (prove)
using this:
inorder l = [i..k - 1]
inorder r = [k + 1..j]
i \<le> k
k \<le> j

goal (1 subgoal):
 1. fst ` leaves i l \<inter> fst ` leaves (k + 1) r = {}
[PROOF STEP]
by(simp add: fst_leaves del: set_inorder add: set_inorder[symmetric])
[PROOF STATE]
proof (state)
this:
fst ` leaves i l \<inter> fst ` leaves (k + 1) r = {}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
hence l0: "?Ll \<inter> ?Lr = {}"
[PROOF STATE]
proof (prove)
using this:
fst ` leaves i l \<inter> fst ` leaves (k + 1) r = {}

goal (1 subgoal):
 1. leaves i l \<inter> leaves (k + 1) r = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
leaves i l \<inter> leaves (k + 1) r = {}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "wpl i j (Node l k r) =  Wpl i l + Wpl (k + 1) r + w i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wpl i j \<langle>l, k, r\<rangle> = Wpl i l + Wpl (k + 1) r + w i j
[PROOF STEP]
using Node.IH inorder
[PROOF STATE]
proof (prove)
using this:
inorder l = [?i..?j] \<Longrightarrow> wpl ?i ?j l = Wpl ?i l
inorder r = [?i..?j] \<Longrightarrow> wpl ?i ?j r = Wpl ?i r
inorder l = [i..k - 1]
inorder r = [k + 1..j]
i \<le> k
k \<le> j

goal (1 subgoal):
 1. wpl i j \<langle>l, k, r\<rangle> = Wpl i l + Wpl (k + 1) r + w i j
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wpl i j \<langle>l, k, r\<rangle> = Wpl i l + Wpl (k + 1) r + w i j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wpl i j \<langle>l, k, r\<rangle> = Wpl i l + Wpl (k + 1) r + w i j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "\<dots> = sum ?b (nodes l) + sum ?a (leaves i l) +
    sum ?b (nodes r) + sum ?a (leaves (k+1) r) + w i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Wpl i l + Wpl (k + 1) r + w i j = (\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k) + w i j
[PROOF STEP]
by (simp add: Wpl_def)
[PROOF STATE]
proof (state)
this:
Wpl i l + Wpl (k + 1) r + w i j = (\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k) + w i j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Wpl i l + Wpl (k + 1) r + w i j = (\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k) + w i j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "\<dots> = (sum ?b (nodes l) + sum ?b (nodes r))
    + (sum ?a (leaves i l) + sum ?a (leaves (k+1) r)) + w i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k) + w i j = (\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + ((\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k)) + w i j
[PROOF STEP]
by(simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k) + w i j = (\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + ((\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k)) + w i j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k) + w i j = (\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + ((\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k)) + w i j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "\<dots> = sum ?b ?N + sum ?a ?L + w i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + ((\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k)) + w i j = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + w i j
[PROOF STEP]
by(simp add: sum_Un_nat finite_nodes finite_leaves l0 n0)
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + ((\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k)) + w i j = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + w i j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l. c * b k) + (\<Sum>(k, c)\<in>nodes r. c * b k) + ((\<Sum>(k, c)\<in>leaves i l. c * a k) + (\<Sum>(k, c)\<in>leaves (k + 1) r. c * a k)) + w i j = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + w i j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "\<dots> = sum ?b ?N + sum ?a ?L + sum a {i..j+1} + sum b {i..j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + w i j = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} + sum b {i..j}
[PROOF STEP]
by (simp add: w_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + w i j = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} + sum b {i..j}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + w i j = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} + sum b {i..j}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "\<dots> = sum ?b ?N + sum b {i..j} + (sum ?a ?L + sum a {i..j+1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} + ((\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1})
[PROOF STEP]
by(simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} + ((\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1})

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} + ((\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1})

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "sum ?a ?L + sum a {i..j+1} = sum ?a (incr2 ` ?L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} = (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} = (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k)
[PROOF STEP]
have "{i..j+1} = {i..k} \<union> {k+1..j+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i..j + 1} = {i..k} \<union> {k + 1..j + 1}
[PROOF STEP]
using inorder(3,4)
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k \<le> j

goal (1 subgoal):
 1. {i..j + 1} = {i..k} \<union> {k + 1..j + 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i..j + 1} = {i..k} \<union> {k + 1..j + 1}

goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} = (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{i..j + 1} = {i..k} \<union> {k + 1..j + 1}

goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} = (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k)
[PROOF STEP]
using inorder(3,4)
[PROOF STATE]
proof (prove)
using this:
{i..j + 1} = {i..k} \<union> {k + 1..j + 1}
i \<le> k
k \<le> j

goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} = (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k)
[PROOF STEP]
by (simp add: sum_incr2 split_def sum.distrib sum_Un_nat finite_leaves l0
        sum_leaves[OF inorder(1)] sum_leaves[OF inorder(2)])
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} = (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} = (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k)

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>leaves i l \<union> leaves (k + 1) r. c * a k) + sum a {i..j + 1} = (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k)

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "sum ?b ?N + sum b {i..j}
     = sum ?b ?N + sum b ({i..k-1} \<union> {k+1..j}) + b k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) + b k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) + b k
[PROOF STEP]
have "{i..j} = {k} \<union> {i..k-1} \<union> {k+1..j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i..j} = {k} \<union> {i..k - 1} \<union> {k + 1..j}
[PROOF STEP]
using inorder(3,4)
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k \<le> j

goal (1 subgoal):
 1. {i..j} = {k} \<union> {i..k - 1} \<union> {k + 1..j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i..j} = {k} \<union> {i..k - 1} \<union> {k + 1..j}

goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) + b k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{i..j} = {k} \<union> {i..k - 1} \<union> {k + 1..j}

goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) + b k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) + b k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) + b k

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b {i..j} = (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) + b k

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "sum ?b ?N + sum b ({i..k-1} \<union> {k+1..j}) = sum ?b (incr2 ` ?N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) = (\<Sum>(k, c)\<in>incr2 ` (nodes l \<union> nodes r). c * b k)
[PROOF STEP]
by (simp add: sum_incr2 split_def sum.distrib sum_Un_nat finite_nodes n0
        sum_nodes[OF inorder(1)] sum_nodes[OF inorder(2)])
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) = (\<Sum>(k, c)\<in>incr2 ` (nodes l \<union> nodes r). c * b k)

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>nodes l \<union> nodes r. c * b k) + sum b ({i..k - 1} \<union> {k + 1..j}) = (\<Sum>(k, c)\<in>incr2 ` (nodes l \<union> nodes r). c * b k)

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "sum ?b (incr2 ` ?N) + b k = sum ?b ({(k,1)} \<union> incr2 ` ?N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>incr2 ` (nodes l \<union> nodes r). c * b k) + b k = (\<Sum>(k, c)\<in>{(k, 1)} \<union> incr2 ` (nodes l \<union> nodes r). c * b k)
[PROOF STEP]
by(simp, subst sum.insert, auto simp add: finite_nodes notin_nodes0)
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>incr2 ` (nodes l \<union> nodes r). c * b k) + b k = (\<Sum>(k, c)\<in>{(k, 1)} \<union> incr2 ` (nodes l \<union> nodes r). c * b k)

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>incr2 ` (nodes l \<union> nodes r). c * b k) + b k = (\<Sum>(k, c)\<in>{(k, 1)} \<union> incr2 ` (nodes l \<union> nodes r). c * b k)

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
have "sum ?b ({(k,1)} \<union> incr2 ` ?N) + sum ?a (incr2 ` ?L) = Wpl i \<langle>l,k,r\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, c)\<in>{(k, 1)} \<union> incr2 ` (nodes l \<union> nodes r). c * b k) + (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k) = Wpl i \<langle>l, k, r\<rangle>
[PROOF STEP]
by(simp add: Wpl_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, c)\<in>{(k, 1)} \<union> incr2 ` (nodes l \<union> nodes r). c * b k) + (\<Sum>(k, c)\<in>incr2 ` (leaves i l \<union> leaves (k + 1) r). c * a k) = Wpl i \<langle>l, k, r\<rangle>

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. inorder t1 = [i..j] \<Longrightarrow> wpl i j t1 = Wpl i t1; \<And>i j. inorder t2 = [i..j] \<Longrightarrow> wpl i j t2 = Wpl i t2; inorder \<langle>t1, x2, t2\<rangle> = [i..j]\<rbrakk> \<Longrightarrow> wpl i j \<langle>t1, x2, t2\<rangle> = Wpl i \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wpl i j \<langle>l, k, r\<rangle> = Wpl i \<langle>l, k, r\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wpl i j \<langle>l, k, r\<rangle> = Wpl i \<langle>l, k, r\<rangle>

goal (1 subgoal):
 1. wpl i j \<langle>l, k, r\<rangle> = Wpl i \<langle>l, k, r\<rangle>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wpl i j \<langle>l, k, r\<rangle> = Wpl i \<langle>l, k, r\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma REL_INTFI: "REL_INTF R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REL_INTF R I
[PROOF STEP]
by simp


[STATEMENT]
lemma finite_alphabet[simp]:
"finite (alphabet t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (alphabet t)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma exists_in_alphabet:
"\<exists>a. a \<in> alphabet t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. a \<in> alphabet t
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma tree_induct_consistent[consumes 1, case_names base step\<^sub>1 step\<^sub>2 step\<^sub>3]:
"\<lbrakk>consistent t;
  \<And>w\<^sub>b b a. P (Leaf w\<^sub>b b) a;
  \<And>w t\<^sub>1 t\<^sub>2 a.
     \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {};
      a \<in> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow>
     P (Node w t\<^sub>1 t\<^sub>2) a;
  \<And>w t\<^sub>1 t\<^sub>2 a.
     \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {};
      a \<notin> alphabet t\<^sub>1; a \<in> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow>
     P (Node w t\<^sub>1 t\<^sub>2) a;
  \<And>w t\<^sub>1 t\<^sub>2 a.
     \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {};
      a \<notin> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow>
     P (Node w t\<^sub>1 t\<^sub>2) a\<rbrakk> \<Longrightarrow>
 P t a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; \<And>w\<^sub>b b a. P (Leaf w\<^sub>b b) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<in> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<notin> alphabet t\<^sub>1; a \<in> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<notin> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a\<rbrakk> \<Longrightarrow> P t a
[PROOF STEP]
txt \<open>
The proof relies on the \textit{induction\_schema} and
\textit{lexicographic\_order} tactics, which automate the most tedious
aspects of deriving induction rules. The alternative would have been to perform
a standard structural induction on @{term t} and proceed by cases, which is
straightforward but long-winded.
\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; \<And>w\<^sub>b b a. P (Leaf w\<^sub>b b) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<in> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<notin> alphabet t\<^sub>1; a \<in> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<notin> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a\<rbrakk> \<Longrightarrow> P t a
[PROOF STEP]
apply rotate_tac
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>w\<^sub>b b a. P (Leaf w\<^sub>b b) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<in> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<notin> alphabet t\<^sub>1; a \<in> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a; \<And>w t\<^sub>1 t\<^sub>2 a. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<notin> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; P t\<^sub>1 a; P t\<^sub>2 a\<rbrakk> \<Longrightarrow> P (Node w t\<^sub>1 t\<^sub>2) a; consistent t\<rbrakk> \<Longrightarrow> P t a
[PROOF STEP]
apply induction_schema
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>P t a. \<lbrakk>consistent t; \<And>w\<^sub>b__ b__ aa__. \<lbrakk>t = Leaf w\<^sub>b__ b__; a = aa__\<rbrakk> \<Longrightarrow> P; \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; t = Node w__ t\<^sub>1__ t\<^sub>2__; a = aa__\<rbrakk> \<Longrightarrow> P; \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; t = Node w__ t\<^sub>1__ t\<^sub>2__; a = aa__\<rbrakk> \<Longrightarrow> P; \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; t = Node w__ t\<^sub>1__ t\<^sub>2__; a = aa__\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. wf ?R2
 3. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 4. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 5. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 6. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 7. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 8. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>t a. consistent t \<Longrightarrow> (\<exists>w\<^sub>b__ b__ aa__. t = Leaf w\<^sub>b__ b__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<in> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<in> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__)
 2. wf ?R2
 3. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 4. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 5. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 6. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 7. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 8. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply (case_tac t)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>t a x11 x12. \<lbrakk>consistent t; t = Leaf x11 x12\<rbrakk> \<Longrightarrow> (\<exists>w\<^sub>b__ b__ aa__. t = Leaf w\<^sub>b__ b__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<in> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<in> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__)
 2. \<And>t a x21 x22 x23. \<lbrakk>consistent t; t = Node x21 x22 x23\<rbrakk> \<Longrightarrow> (\<exists>w\<^sub>b__ b__ aa__. t = Leaf w\<^sub>b__ b__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<in> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<in> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__)
 3. wf ?R2
 4. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 5. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 6. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 7. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 8. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 9. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>t a x21 x22 x23. \<lbrakk>consistent t; t = Node x21 x22 x23\<rbrakk> \<Longrightarrow> (\<exists>w\<^sub>b__ b__ aa__. t = Leaf w\<^sub>b__ b__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<in> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<in> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__) \<or> (\<exists>w__ t\<^sub>1__ t\<^sub>2__ aa__. consistent t\<^sub>1__ \<and> consistent t\<^sub>2__ \<and> alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {} \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> t = Node w__ t\<^sub>1__ t\<^sub>2__ \<and> a = aa__)
 2. wf ?R2
 3. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 4. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 5. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 6. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 7. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 8. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. wf ?R2
 2. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 3. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 4. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 5. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 6. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>1__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
 7. \<And>w__ t\<^sub>1__ t\<^sub>2__ aa__. \<lbrakk>consistent t\<^sub>1__; consistent t\<^sub>2__; alphabet t\<^sub>1__ \<inter> alphabet t\<^sub>2__ = {}; aa__ \<notin> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
by lexicographic_order


[STATEMENT]
lemma depth_le_height:
"depth t a \<le> height t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. depth t a \<le> height t
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma exists_at_height:
"consistent t \<Longrightarrow> \<exists>a \<in> alphabet t. depth t a = height t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> \<exists>a\<in>alphabet t. depth t a = height t
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. consistent (Leaf x1 x2) \<Longrightarrow> \<exists>a\<in>alphabet (Leaf x1 x2). depth (Leaf x1 x2) a = height (Leaf x1 x2)
 2. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
consistent (Leaf x1_ x2_)

goal (2 subgoals):
 1. \<And>x1 x2. consistent (Leaf x1 x2) \<Longrightarrow> \<exists>a\<in>alphabet (Leaf x1 x2). depth (Leaf x1 x2) a = height (Leaf x1 x2)
 2. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
consistent (Leaf x1_ x2_)

goal (1 subgoal):
 1. \<exists>a\<in>alphabet (Leaf x1_ x2_). depth (Leaf x1_ x2_) a = height (Leaf x1_ x2_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>alphabet (Leaf x1_ x2_). depth (Leaf x1_ x2_) a = height (Leaf x1_ x2_)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
case (Node w t\<^sub>1 t\<^sub>2)
[PROOF STATE]
proof (state)
this:
consistent t\<^sub>1 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>1. depth t\<^sub>1 a = height t\<^sub>1
consistent t\<^sub>2 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>2. depth t\<^sub>2 a = height t\<^sub>2
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
note hyps = Node
[PROOF STATE]
proof (state)
this:
consistent t\<^sub>1 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>1. depth t\<^sub>1 a = height t\<^sub>1
consistent t\<^sub>2 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>2. depth t\<^sub>2 a = height t\<^sub>2
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
let ?t = "Node w t\<^sub>1 t\<^sub>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
from hyps
[PROOF STATE]
proof (chain)
picking this:
consistent t\<^sub>1 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>1. depth t\<^sub>1 a = height t\<^sub>1
consistent t\<^sub>2 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>2. depth t\<^sub>2 a = height t\<^sub>2
consistent (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
obtain b where b: "b \<in> alphabet t\<^sub>1" "depth t\<^sub>1 b = height t\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
consistent t\<^sub>1 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>1. depth t\<^sub>1 a = height t\<^sub>1
consistent t\<^sub>2 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>2. depth t\<^sub>2 a = height t\<^sub>2
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>b \<in> alphabet t\<^sub>1; depth t\<^sub>1 b = height t\<^sub>1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> alphabet t\<^sub>1
depth t\<^sub>1 b = height t\<^sub>1

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
from hyps
[PROOF STATE]
proof (chain)
picking this:
consistent t\<^sub>1 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>1. depth t\<^sub>1 a = height t\<^sub>1
consistent t\<^sub>2 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>2. depth t\<^sub>2 a = height t\<^sub>2
consistent (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
obtain c where c: "c \<in> alphabet t\<^sub>2" "depth t\<^sub>2 c = height t\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
consistent t\<^sub>1 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>1. depth t\<^sub>1 a = height t\<^sub>1
consistent t\<^sub>2 \<Longrightarrow> \<exists>a\<in>alphabet t\<^sub>2. depth t\<^sub>2 a = height t\<^sub>2
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> alphabet t\<^sub>2; depth t\<^sub>2 c = height t\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> alphabet t\<^sub>2
depth t\<^sub>2 c = height t\<^sub>2

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
let ?a = "if height t\<^sub>1 \<ge> height t\<^sub>2 then b else c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
from b c
[PROOF STATE]
proof (chain)
picking this:
b \<in> alphabet t\<^sub>1
depth t\<^sub>1 b = height t\<^sub>1
c \<in> alphabet t\<^sub>2
depth t\<^sub>2 c = height t\<^sub>2
[PROOF STEP]
have "?a \<in> alphabet ?t" "depth ?t ?a = height ?t"
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
depth t\<^sub>1 b = height t\<^sub>1
c \<in> alphabet t\<^sub>2
depth t\<^sub>2 c = height t\<^sub>2

goal (1 subgoal):
 1. (if height t\<^sub>2 \<le> height t\<^sub>1 then b else c) \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) &&& depth (Node w t\<^sub>1 t\<^sub>2) (if height t\<^sub>2 \<le> height t\<^sub>1 then b else c) = height (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
using \<open>consistent ?t\<close>
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
depth t\<^sub>1 b = height t\<^sub>1
c \<in> alphabet t\<^sub>2
depth t\<^sub>2 c = height t\<^sub>2
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. (if height t\<^sub>2 \<le> height t\<^sub>1 then b else c) \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) &&& depth (Node w t\<^sub>1 t\<^sub>2) (if height t\<^sub>2 \<le> height t\<^sub>1 then b else c) = height (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if height t\<^sub>2 \<le> height t\<^sub>1 then b else c) \<in> alphabet (Node w t\<^sub>1 t\<^sub>2)
depth (Node w t\<^sub>1 t\<^sub>2) (if height t\<^sub>2 \<le> height t\<^sub>1 then b else c) = height (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> \<exists>a\<in>alphabet t1. depth t1 a = height t1; consistent t2 \<Longrightarrow> \<exists>a\<in>alphabet t2. depth t2 a = height t2; consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> \<exists>a\<in>alphabet (Node x1 t1 t2). depth (Node x1 t1 t2) a = height (Node x1 t1 t2)
[PROOF STEP]
thus "\<exists>a \<in> alphabet ?t. depth ?t a = height ?t"
[PROOF STATE]
proof (prove)
using this:
(if height t\<^sub>2 \<le> height t\<^sub>1 then b else c) \<in> alphabet (Node w t\<^sub>1 t\<^sub>2)
depth (Node w t\<^sub>1 t\<^sub>2) (if height t\<^sub>2 \<le> height t\<^sub>1 then b else c) = height (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. \<exists>a\<in>alphabet (Node w t\<^sub>1 t\<^sub>2). depth (Node w t\<^sub>1 t\<^sub>2) a = height (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>alphabet (Node w t\<^sub>1 t\<^sub>2). depth (Node w t\<^sub>1 t\<^sub>2) a = height (Node w t\<^sub>1 t\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma depth_max_heightE_left[elim!]:
"\<lbrakk>depth t\<^sub>1 a = max (height t\<^sub>1) (height t\<^sub>2);
  \<lbrakk>depth t\<^sub>1 a = height t\<^sub>1; height t\<^sub>1 \<ge> height t\<^sub>2\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow>
 P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>depth t\<^sub>1 a = max (height t\<^sub>1) (height t\<^sub>2); \<lbrakk>depth t\<^sub>1 a = height t\<^sub>1; height t\<^sub>2 \<le> height t\<^sub>1\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (cut_tac t = t\<^sub>1 and a = a in depth_le_height) simp


[STATEMENT]
lemma depth_max_heightE_right[elim!]:
"\<lbrakk>depth t\<^sub>2 a = max (height t\<^sub>1) (height t\<^sub>2);
  \<lbrakk>depth t\<^sub>2 a = height t\<^sub>2; height t\<^sub>2 \<ge> height t\<^sub>1\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow>
 P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>depth t\<^sub>2 a = max (height t\<^sub>1) (height t\<^sub>2); \<lbrakk>depth t\<^sub>2 a = height t\<^sub>2; height t\<^sub>1 \<le> height t\<^sub>2\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (cut_tac t = t\<^sub>2 and a = a in depth_le_height) simp


[STATEMENT]
lemma height_gt_0_alphabet_eq_imp_height_gt_0:
assumes "height t > 0" "consistent t" "alphabet t = alphabet u"
shows "height u > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
proof (cases t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. t = Leaf x11 x12 \<Longrightarrow> 0 < height u
 2. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
t = Leaf x11_ x12_

goal (2 subgoals):
 1. \<And>x11 x12. t = Leaf x11 x12 \<Longrightarrow> 0 < height u
 2. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Leaf x11_ x12_

goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t = Leaf x11_ x12_
0 < height t
consistent t
alphabet t = alphabet u

goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < height u

goal (1 subgoal):
 1. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
case (Node w t\<^sub>1 t\<^sub>2)
[PROOF STATE]
proof (state)
this:
t = Node w t\<^sub>1 t\<^sub>2

goal (1 subgoal):
 1. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
note t = Node
[PROOF STATE]
proof (state)
this:
t = Node w t\<^sub>1 t\<^sub>2

goal (1 subgoal):
 1. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
from exists_in_alphabet
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. a \<in> alphabet ?t
[PROOF STEP]
obtain b where b: "b \<in> alphabet t\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. a \<in> alphabet ?t

goal (1 subgoal):
 1. (\<And>b. b \<in> alphabet t\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
b \<in> alphabet t\<^sub>1

goal (1 subgoal):
 1. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
from exists_in_alphabet
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. a \<in> alphabet ?t
[PROOF STEP]
obtain c where c: "c \<in> alphabet t\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. a \<in> alphabet ?t

goal (1 subgoal):
 1. (\<And>c. c \<in> alphabet t\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
c \<in> alphabet t\<^sub>2

goal (1 subgoal):
 1. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
from b c
[PROOF STATE]
proof (chain)
picking this:
b \<in> alphabet t\<^sub>1
c \<in> alphabet t\<^sub>2
[PROOF STEP]
have bc: "b \<noteq> c"
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
c \<in> alphabet t\<^sub>2

goal (1 subgoal):
 1. b \<noteq> c
[PROOF STEP]
using t \<open>consistent t\<close>
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
c \<in> alphabet t\<^sub>2
t = Node w t\<^sub>1 t\<^sub>2
consistent t

goal (1 subgoal):
 1. b \<noteq> c
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
b \<noteq> c

goal (1 subgoal):
 1. \<And>x21 x22 x23. t = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
proof (cases u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. u = Leaf x11 x12 \<Longrightarrow> 0 < height u
 2. \<And>x21 x22 x23. u = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
u = Leaf x11_ x12_

goal (2 subgoals):
 1. \<And>x11 x12. u = Leaf x11 x12 \<Longrightarrow> 0 < height u
 2. \<And>x21 x22 x23. u = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u = Leaf x11_ x12_

goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
using b c bc t assms
[PROOF STATE]
proof (prove)
using this:
u = Leaf x11_ x12_
b \<in> alphabet t\<^sub>1
c \<in> alphabet t\<^sub>2
b \<noteq> c
t = Node w t\<^sub>1 t\<^sub>2
0 < height t
consistent t
alphabet t = alphabet u

goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < height u

goal (1 subgoal):
 1. \<And>x21 x22 x23. u = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. u = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
case Node
[PROOF STATE]
proof (state)
this:
u = Node x21_ x22_ x23_

goal (1 subgoal):
 1. \<And>x21 x22 x23. u = Node x21 x22 x23 \<Longrightarrow> 0 < height u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u = Node x21_ x22_ x23_

goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < height u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < height u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma notin_alphabet_imp_freq_0[simp]:
"a \<notin> alphabet t \<Longrightarrow> freq t a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> alphabet t \<Longrightarrow> freq t a = 0
[PROOF STEP]
by (induct t) simp+


[STATEMENT]
lemma notin_alphabet\<^sub>F_imp_freq\<^sub>F_0[simp]:
"a \<notin> alphabet\<^sub>F ts \<Longrightarrow> freq\<^sub>F ts a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> alphabet\<^sub>F ts \<Longrightarrow> freq\<^sub>F ts a = 0
[PROOF STEP]
by (induct ts) simp+


[STATEMENT]
lemma freq_0_right[simp]:
"\<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<in> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow> freq t\<^sub>2 a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<in> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow> freq t\<^sub>2 a = 0
[PROOF STEP]
by (auto intro: notin_alphabet_imp_freq_0 simp: disjoint_iff_not_equal)


[STATEMENT]
lemma freq_0_left[simp]:
"\<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<in> alphabet t\<^sub>2\<rbrakk> \<Longrightarrow> freq t\<^sub>1 a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<in> alphabet t\<^sub>2\<rbrakk> \<Longrightarrow> freq t\<^sub>1 a = 0
[PROOF STEP]
by (auto simp: disjoint_iff_not_equal)


[STATEMENT]
lemma height\<^sub>F_0_imp_Leaf_freq\<^sub>F_in_set:
"\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow>
 Leaf (freq\<^sub>F ts a) a \<in> set ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F ts a) a \<in> set ts
[PROOF STEP]
proof (induct ts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>consistent\<^sub>F []; height\<^sub>F [] = 0; a \<in> alphabet\<^sub>F []\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F [] a) a \<in> set []
 2. \<And>aa ts. \<lbrakk>\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F ts a) a \<in> set ts; consistent\<^sub>F (aa # ts); height\<^sub>F (aa # ts) = 0; a \<in> alphabet\<^sub>F (aa # ts)\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F (aa # ts) a) a \<in> set (aa # ts)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
consistent\<^sub>F []
height\<^sub>F [] = 0
a \<in> alphabet\<^sub>F []

goal (2 subgoals):
 1. \<lbrakk>consistent\<^sub>F []; height\<^sub>F [] = 0; a \<in> alphabet\<^sub>F []\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F [] a) a \<in> set []
 2. \<And>aa ts. \<lbrakk>\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F ts a) a \<in> set ts; consistent\<^sub>F (aa # ts); height\<^sub>F (aa # ts) = 0; a \<in> alphabet\<^sub>F (aa # ts)\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F (aa # ts) a) a \<in> set (aa # ts)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
consistent\<^sub>F []
height\<^sub>F [] = 0
a \<in> alphabet\<^sub>F []

goal (1 subgoal):
 1. Leaf (freq\<^sub>F [] a) a \<in> set []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Leaf (freq\<^sub>F [] a) a \<in> set []

goal (1 subgoal):
 1. \<And>aa ts. \<lbrakk>\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F ts a) a \<in> set ts; consistent\<^sub>F (aa # ts); height\<^sub>F (aa # ts) = 0; a \<in> alphabet\<^sub>F (aa # ts)\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F (aa # ts) a) a \<in> set (aa # ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa ts. \<lbrakk>\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F ts a) a \<in> set ts; consistent\<^sub>F (aa # ts); height\<^sub>F (aa # ts) = 0; a \<in> alphabet\<^sub>F (aa # ts)\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F (aa # ts) a) a \<in> set (aa # ts)
[PROOF STEP]
case (Cons t ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F ts a) a \<in> set ts
consistent\<^sub>F (t # ts)
height\<^sub>F (t # ts) = 0
a \<in> alphabet\<^sub>F (t # ts)

goal (1 subgoal):
 1. \<And>aa ts. \<lbrakk>\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F ts a) a \<in> set ts; consistent\<^sub>F (aa # ts); height\<^sub>F (aa # ts) = 0; a \<in> alphabet\<^sub>F (aa # ts)\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F (aa # ts) a) a \<in> set (aa # ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Leaf (freq\<^sub>F (t # ts) a) a \<in> set (t # ts)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; a \<in> alphabet\<^sub>F ts\<rbrakk> \<Longrightarrow> Leaf (freq\<^sub>F ts a) a \<in> set ts
consistent\<^sub>F (t # ts)
height\<^sub>F (t # ts) = 0
a \<in> alphabet\<^sub>F (t # ts)

goal (1 subgoal):
 1. Leaf (freq\<^sub>F (t # ts) a) a \<in> set (t # ts)
[PROOF STEP]
by (cases t) auto
[PROOF STATE]
proof (state)
this:
Leaf (freq\<^sub>F (t # ts) a) a \<in> set (t # ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weight_eq_Sum_freq:
"consistent t \<Longrightarrow> weight t = (\<Sum>a \<in> alphabet t. freq t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> weight t = sum (freq t) (alphabet t)
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> weight t = sum (freq t) (alphabet t)
[PROOF STEP]
by (induct t) (auto simp: sum.union_disjoint)