[STATEMENT]
theorem cost_eq_Sum_freq_mult_depth:
"consistent t \<Longrightarrow> cost t = (\<Sum>a \<in> alphabet t. freq t a * depth t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> cost t = (\<Sum>a\<in>alphabet t. freq t a * depth t a)
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> cost t = (\<Sum>a\<in>alphabet t. freq t a * depth t a)
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. consistent (Leaf x1 x2) \<Longrightarrow> cost (Leaf x1 x2) = (\<Sum>a\<in>alphabet (Leaf x1 x2). freq (Leaf x1 x2) a * depth (Leaf x1 x2) a)
 2. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[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> cost (Leaf x1 x2) = (\<Sum>a\<in>alphabet (Leaf x1 x2). freq (Leaf x1 x2) a * depth (Leaf x1 x2) a)
 2. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
consistent (Leaf x1_ x2_)

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

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

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[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> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
let ?A = "alphabet ?t" and ?A\<^sub>1 = "alphabet t\<^sub>1" and ?A\<^sub>2 = "alphabet t\<^sub>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
note c = \<open>consistent ?t\<close>
[PROOF STATE]
proof (state)
this:
consistent (Node w t\<^sub>1 t\<^sub>2)

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

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have d\<^sub>2: "\<And>a. \<lbrakk>?A\<^sub>1 \<inter> ?A\<^sub>2 = {}; a \<in> ?A\<^sub>2\<rbrakk> \<Longrightarrow> depth ?t a = depth t\<^sub>2 a + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; a \<in> alphabet t\<^sub>2\<rbrakk> \<Longrightarrow> depth (Node w t\<^sub>1 t\<^sub>2) a = depth t\<^sub>2 a + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; ?a \<in> alphabet t\<^sub>2\<rbrakk> \<Longrightarrow> depth (Node w t\<^sub>1 t\<^sub>2) ?a = depth t\<^sub>2 ?a + 1

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have "cost ?t = weight t\<^sub>1 + cost t\<^sub>1 + weight t\<^sub>2 + cost t\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (Node w t\<^sub>1 t\<^sub>2) = weight t\<^sub>1 + cost t\<^sub>1 + weight t\<^sub>2 + cost t\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cost (Node w t\<^sub>1 t\<^sub>2) = weight t\<^sub>1 + cost t\<^sub>1 + weight t\<^sub>2 + cost t\<^sub>2

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cost (Node w t\<^sub>1 t\<^sub>2) = weight t\<^sub>1 + cost t\<^sub>1 + weight t\<^sub>2 + cost t\<^sub>2

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have "\<dots> = weight t\<^sub>1 + (\<Sum>a \<in> ?A\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a)
    + weight t\<^sub>2 + (\<Sum>a \<in> ?A\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight t\<^sub>1 + cost t\<^sub>1 + weight t\<^sub>2 + cost t\<^sub>2 = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a)
[PROOF STEP]
using hyps
[PROOF STATE]
proof (prove)
using this:
consistent t\<^sub>1 \<Longrightarrow> cost t\<^sub>1 = (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a)
consistent t\<^sub>2 \<Longrightarrow> cost t\<^sub>2 = (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a)
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. weight t\<^sub>1 + cost t\<^sub>1 + weight t\<^sub>2 + cost t\<^sub>2 = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
weight t\<^sub>1 + cost t\<^sub>1 + weight t\<^sub>2 + cost t\<^sub>2 = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
weight t\<^sub>1 + cost t\<^sub>1 + weight t\<^sub>2 + cost t\<^sub>2 = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have "\<dots> = weight t\<^sub>1 + (\<Sum>a \<in> ?A\<^sub>1. freq t\<^sub>1 a * (depth ?t a - 1))
    + weight t\<^sub>2 + (\<Sum>a \<in> ?A\<^sub>2. freq t\<^sub>2 a * (depth ?t a - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a) = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1))
[PROOF STEP]
using c d\<^sub>2
[PROOF STATE]
proof (prove)
using this:
consistent (Node w t\<^sub>1 t\<^sub>2)
\<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; ?a \<in> alphabet t\<^sub>2\<rbrakk> \<Longrightarrow> depth (Node w t\<^sub>1 t\<^sub>2) ?a = depth t\<^sub>2 ?a + 1

goal (1 subgoal):
 1. weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a) = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a) = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1))

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth t\<^sub>1 a) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth t\<^sub>2 a) = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1))

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have "\<dots> = weight t\<^sub>1 + (\<Sum>a \<in> ?A\<^sub>1. freq t\<^sub>1 a * depth ?t a)
    - (\<Sum>a \<in> ?A\<^sub>1. freq t\<^sub>1 a)
    + weight t\<^sub>2 + (\<Sum>a \<in> ?A\<^sub>2. freq t\<^sub>2 a * depth ?t a)
    - (\<Sum>a \<in> ?A\<^sub>2. freq t\<^sub>2 a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>1) (alphabet t\<^sub>1) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>2) (alphabet t\<^sub>2)
[PROOF STEP]
using c d\<^sub>2
[PROOF STATE]
proof (prove)
using this:
consistent (Node w t\<^sub>1 t\<^sub>2)
\<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; ?a \<in> alphabet t\<^sub>2\<rbrakk> \<Longrightarrow> depth (Node w t\<^sub>1 t\<^sub>2) ?a = depth t\<^sub>2 ?a + 1

goal (1 subgoal):
 1. weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>1) (alphabet t\<^sub>1) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>2) (alphabet t\<^sub>2)
[PROOF STEP]
by (simp add: sum.distrib)
[PROOF STATE]
proof (state)
this:
weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>1) (alphabet t\<^sub>1) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>2) (alphabet t\<^sub>2)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * (depth (Node w t\<^sub>1 t\<^sub>2) a - 1)) = weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>1) (alphabet t\<^sub>1) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>2) (alphabet t\<^sub>2)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have "\<dots> = (\<Sum>a \<in> ?A\<^sub>1. freq t\<^sub>1 a * depth ?t a)
    + (\<Sum>a \<in> ?A\<^sub>2. freq t\<^sub>2 a * depth ?t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>1) (alphabet t\<^sub>1) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>2) (alphabet t\<^sub>2) = (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a)
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>1) (alphabet t\<^sub>1) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>2) (alphabet t\<^sub>2) = (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a)
[PROOF STEP]
by (simp add: weight_eq_Sum_freq)
[PROOF STATE]
proof (state)
this:
weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>1) (alphabet t\<^sub>1) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>2) (alphabet t\<^sub>2) = (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
weight t\<^sub>1 + (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>1) (alphabet t\<^sub>1) + weight t\<^sub>2 + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) - sum (freq t\<^sub>2) (alphabet t\<^sub>2) = (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have "\<dots> = (\<Sum>a \<in> ?A\<^sub>1. freq ?t a * depth ?t a)
    + (\<Sum>a \<in> ?A\<^sub>2. freq ?t a * depth ?t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet t\<^sub>1. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. (\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet t\<^sub>1. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet t\<^sub>1. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>alphabet t\<^sub>1. freq t\<^sub>1 a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq t\<^sub>2 a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet t\<^sub>1. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have "\<dots> = (\<Sum>a \<in> ?A\<^sub>1 \<union> ?A\<^sub>2. freq ?t a * depth ?t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>alphabet t\<^sub>1. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet t\<^sub>1 \<union> alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
consistent (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. (\<Sum>a\<in>alphabet t\<^sub>1. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet t\<^sub>1 \<union> alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)
[PROOF STEP]
by (simp add: sum.union_disjoint)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>alphabet t\<^sub>1. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet t\<^sub>1 \<union> alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>alphabet t\<^sub>1. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) + (\<Sum>a\<in>alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet t\<^sub>1 \<union> alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
have "\<dots> = (\<Sum>a \<in> ?A. freq ?t a * depth ?t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>alphabet t\<^sub>1 \<union> alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet (Node w t\<^sub>1 t\<^sub>2). freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>alphabet t\<^sub>1 \<union> alphabet t\<^sub>2. freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a) = (\<Sum>a\<in>alphabet (Node w t\<^sub>1 t\<^sub>2). freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>consistent t1 \<Longrightarrow> cost t1 = (\<Sum>a\<in>alphabet t1. freq t1 a * depth t1 a); consistent t2 \<Longrightarrow> cost t2 = (\<Sum>a\<in>alphabet t2. freq t2 a * depth t2 a); consistent (Node x1 t1 t2)\<rbrakk> \<Longrightarrow> cost (Node x1 t1 t2) = (\<Sum>a\<in>alphabet (Node x1 t1 t2). freq (Node x1 t1 t2) a * depth (Node x1 t1 t2) a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cost (Node w t\<^sub>1 t\<^sub>2) = (\<Sum>a\<in>alphabet (Node w t\<^sub>1 t\<^sub>2). freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cost (Node w t\<^sub>1 t\<^sub>2) = (\<Sum>a\<in>alphabet (Node w t\<^sub>1 t\<^sub>2). freq (Node w t\<^sub>1 t\<^sub>2) a * depth (Node w t\<^sub>1 t\<^sub>2) a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma height_0_imp_cost_0[simp]:
"height t = 0 \<Longrightarrow> cost t = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. height t = 0 \<Longrightarrow> cost t = 0
[PROOF STEP]
by (case_tac t) simp+


[STATEMENT]
lemma height_0_imp_cachedWeight_eq_weight[simp]:
"height t = 0 \<Longrightarrow> cachedWeight t = weight t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. height t = 0 \<Longrightarrow> cachedWeight t = weight t
[PROOF STEP]
by (case_tac t) simp+


[STATEMENT]
lemma alphabet_uniteTrees[simp]:
"alphabet (uniteTrees t\<^sub>1 t\<^sub>2) = alphabet t\<^sub>1 \<union> alphabet t\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet (uniteTrees t\<^sub>1 t\<^sub>2) = alphabet t\<^sub>1 \<union> alphabet t\<^sub>2
[PROOF STEP]
by (simp add: uniteTrees_def)


[STATEMENT]
lemma consistent_uniteTrees[simp]:
"\<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}\<rbrakk> \<Longrightarrow>
 consistent (uniteTrees t\<^sub>1 t\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t\<^sub>1; consistent t\<^sub>2; alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}\<rbrakk> \<Longrightarrow> consistent (uniteTrees t\<^sub>1 t\<^sub>2)
[PROOF STEP]
by (simp add: uniteTrees_def)


[STATEMENT]
lemma freq_uniteTrees[simp]:
"freq (uniteTrees t\<^sub>1 t\<^sub>2) a = freq t\<^sub>1 a + freq t\<^sub>2 a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freq (uniteTrees t\<^sub>1 t\<^sub>2) a = freq t\<^sub>1 a + freq t\<^sub>2 a
[PROOF STEP]
by (simp add: uniteTrees_def)


[STATEMENT]
lemma length_insortTree[simp]:
"length (insortTree t ts) = length ts + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (insortTree t ts) = length ts + 1
[PROOF STEP]
by (induct ts) simp+


[STATEMENT]
lemma insortTree_ne_Nil[simp]:
"insortTree t ts \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insortTree t ts \<noteq> []
[PROOF STEP]
by (case_tac ts) simp+


[STATEMENT]
lemma alphabet\<^sub>F_insortTree[simp]:
"alphabet\<^sub>F (insortTree t ts) = alphabet t \<union> alphabet\<^sub>F ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet\<^sub>F (insortTree t ts) = alphabet t \<union> alphabet\<^sub>F ts
[PROOF STEP]
by (induct ts) auto


[STATEMENT]
lemma consistent\<^sub>F_insortTree[simp]:
"consistent\<^sub>F (insortTree t ts) = consistent\<^sub>F (t # ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent\<^sub>F (insortTree t ts) = consistent\<^sub>F (t # ts)
[PROOF STEP]
by (induct ts) auto


[STATEMENT]
lemma freq\<^sub>F_insortTree[simp]:
"freq\<^sub>F (insortTree t ts) = (\<lambda>a. freq t a + freq\<^sub>F ts a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freq\<^sub>F (insortTree t ts) = (\<lambda>a. freq t a + freq\<^sub>F ts a)
[PROOF STEP]
by (induct ts) (simp add: ext)+


[STATEMENT]
lemma height\<^sub>F_insortTree[simp]:
"height\<^sub>F (insortTree t ts) = max (height t) (height\<^sub>F ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. height\<^sub>F (insortTree t ts) = max (height t) (height\<^sub>F ts)
[PROOF STEP]
by (induct ts) auto


[STATEMENT]
theorem alphabet_huffman[simp]:
"ts \<noteq> [] \<Longrightarrow> alphabet (huffman ts) = alphabet\<^sub>F ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<noteq> [] \<Longrightarrow> alphabet (huffman ts) = alphabet\<^sub>F ts
[PROOF STEP]
by (induct ts rule: huffman.induct) auto


[STATEMENT]
theorem consistent_huffman[simp]:
"\<lbrakk>consistent\<^sub>F ts; ts \<noteq> []\<rbrakk> \<Longrightarrow> consistent (huffman ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent\<^sub>F ts; ts \<noteq> []\<rbrakk> \<Longrightarrow> consistent (huffman ts)
[PROOF STEP]
by (induct ts rule: huffman.induct) simp+


[STATEMENT]
theorem freq_huffman[simp]:
"ts \<noteq> [] \<Longrightarrow> freq (huffman ts) a = freq\<^sub>F ts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<noteq> [] \<Longrightarrow> freq (huffman ts) a = freq\<^sub>F ts a
[PROOF STEP]
by (induct ts rule: huffman.induct) auto


[STATEMENT]
lemma notin_alphabet_imp_sibling_id[simp]:
"a \<notin> alphabet t \<Longrightarrow> sibling t a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> alphabet t \<Longrightarrow> sibling t a = a
[PROOF STEP]
by (cases rule: sibling.cases[where x = "(t, a)"]) simp+


[STATEMENT]
lemma height_0_imp_sibling_id[simp]:
"height t = 0 \<Longrightarrow> sibling t a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. height t = 0 \<Longrightarrow> sibling t a = a
[PROOF STEP]
by (case_tac t) simp+


[STATEMENT]
lemma height_gt_0_in_alphabet_imp_sibling_right[simp]:
"\<lbrakk>height t\<^sub>2 > 0; a \<in> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow>
 sibling (Node w t\<^sub>1 t\<^sub>2) a = sibling t\<^sub>1 a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < height t\<^sub>2; a \<in> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow> sibling (Node w t\<^sub>1 t\<^sub>2) a = sibling t\<^sub>1 a
[PROOF STEP]
by (case_tac t\<^sub>2) simp+


[STATEMENT]
lemma height_gt_0_notin_alphabet_imp_sibling_left[simp]:
"\<lbrakk>height t\<^sub>1 > 0; a \<notin> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow>
 sibling (Node w t\<^sub>1 t\<^sub>2) a = sibling t\<^sub>2 a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < height t\<^sub>1; a \<notin> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow> sibling (Node w t\<^sub>1 t\<^sub>2) a = sibling t\<^sub>2 a
[PROOF STEP]
by (case_tac t\<^sub>1) simp+


[STATEMENT]
lemma height_gt_0_notin_alphabet_imp_sibling_right[simp]:
"\<lbrakk>height t\<^sub>2 > 0; a \<notin> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow>
 sibling (Node w t\<^sub>1 t\<^sub>2) a = sibling t\<^sub>2 a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < height t\<^sub>2; a \<notin> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow> sibling (Node w t\<^sub>1 t\<^sub>2) a = sibling t\<^sub>2 a
[PROOF STEP]
by (case_tac t\<^sub>2) simp+


[STATEMENT]
lemma either_height_gt_0_imp_sibling[simp]:
"height t\<^sub>1 > 0 \<or> height t\<^sub>2 > 0 \<Longrightarrow>
 sibling (Node w t\<^sub>1 t\<^sub>2) a =
     (if a \<in> alphabet t\<^sub>1 then sibling t\<^sub>1 a else sibling t\<^sub>2 a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2 \<Longrightarrow> sibling (Node w t\<^sub>1 t\<^sub>2) a = (if a \<in> alphabet t\<^sub>1 then sibling t\<^sub>1 a else sibling t\<^sub>2 a)
[PROOF STEP]
by auto


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


[STATEMENT]
lemma sibling_ne_imp_sibling_in_alphabet:
"sibling t a \<noteq> a \<Longrightarrow> sibling t a \<in> alphabet t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling t a \<noteq> a \<Longrightarrow> sibling t a \<in> alphabet t
[PROOF STEP]
by (metis notin_alphabet_imp_sibling_id in_alphabet_imp_sibling_in_alphabet)


[STATEMENT]
lemma sibling_induct_consistent[consumes 1,
  case_names base step\<^sub>1 step\<^sub>2\<^sub>1 step\<^sub>2\<^sub>2 step\<^sub>2\<^sub>3]:
"\<lbrakk>consistent t;
  \<And>w b a. P (Leaf w b) a;
  \<And>w w\<^sub>b b w\<^sub>c c a. b \<noteq> c \<Longrightarrow> P (Node w (Leaf w\<^sub>b b) (Leaf w\<^sub>c c)) 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 = {};
      height t\<^sub>1 > 0 \<or> height t\<^sub>2 > 0; a \<in> alphabet t\<^sub>1;
      sibling t\<^sub>1 a \<in> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2;
      sibling t\<^sub>1 a \<notin> alphabet t\<^sub>2; P t\<^sub>1 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 = {};
      height t\<^sub>1 > 0 \<or> height t\<^sub>2 > 0; a \<notin> alphabet t\<^sub>1;
      sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1; a \<in> alphabet t\<^sub>2;
      sibling t\<^sub>2 a \<in> alphabet t\<^sub>2; 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 = {};
      height t\<^sub>1 > 0 \<or> height t\<^sub>2 > 0; a \<notin> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2\<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 b a. P (Leaf w b) a; \<And>w w\<^sub>b b w\<^sub>c c a. b \<noteq> c \<Longrightarrow> P (Node w (Leaf w\<^sub>b b) (Leaf w\<^sub>c c)) 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 = {}; 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2; a \<in> alphabet t\<^sub>1; sibling t\<^sub>1 a \<in> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; sibling t\<^sub>1 a \<notin> alphabet t\<^sub>2; P t\<^sub>1 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 = {}; 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2; a \<notin> alphabet t\<^sub>1; sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1; a \<in> alphabet t\<^sub>2; sibling t\<^sub>2 a \<in> alphabet t\<^sub>2; 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 = {}; 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2; a \<notin> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2\<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 b a. P (Leaf w b) a; \<And>w w\<^sub>b b w\<^sub>c c a. b \<noteq> c \<Longrightarrow> P (Node w (Leaf w\<^sub>b b) (Leaf w\<^sub>c c)) 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 = {}; 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2; a \<in> alphabet t\<^sub>1; sibling t\<^sub>1 a \<in> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2; sibling t\<^sub>1 a \<notin> alphabet t\<^sub>2; P t\<^sub>1 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 = {}; 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2; a \<notin> alphabet t\<^sub>1; sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1; a \<in> alphabet t\<^sub>2; sibling t\<^sub>2 a \<in> alphabet t\<^sub>2; 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 = {}; 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2; a \<notin> alphabet t\<^sub>1; a \<notin> alphabet t\<^sub>2\<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 (4 subgoals):
 1. \<And>P t a. \<lbrakk>consistent t; \<And>w__ b__ aa__. \<lbrakk>t = Leaf w__ b__; a = aa__\<rbrakk> \<Longrightarrow> P; \<And>w__ w\<^sub>b__ b__ w\<^sub>c__ c__ aa__. \<lbrakk>b__ \<noteq> c__; t = Node w__ (Leaf w\<^sub>b__ b__) (Leaf w\<^sub>c__ c__); 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> 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 (4 subgoals):
 1. \<And>t a. consistent t \<Longrightarrow> (\<exists>w__ b__ aa__. t = Leaf w__ b__ \<and> a = aa__) \<or> (\<exists>w__ w\<^sub>b__ b__ w\<^sub>c__ c__ aa__. b__ \<noteq> c__ \<and> t = Node w__ (Leaf w\<^sub>b__ b__) (Leaf w\<^sub>c__ c__) \<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> (0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__) \<and> aa__ \<in> alphabet t\<^sub>1__ \<and> sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> sibling t\<^sub>1__ 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> (0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__) \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<in> alphabet t\<^sub>2__ \<and> sibling t\<^sub>2__ 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> (0 < height t\<^sub>1__ \<or> 0 < height 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> 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, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t a x21 x22 x23. \<lbrakk>consistent t; t = Node x21 x22 x23\<rbrakk> \<Longrightarrow> (\<exists>w__ b__ aa__. t = Leaf w__ b__ \<and> a = aa__) \<or> (\<exists>w__ w\<^sub>b__ b__ w\<^sub>c__ c__ aa__. b__ \<noteq> c__ \<and> t = Node w__ (Leaf w\<^sub>b__ b__) (Leaf w\<^sub>c__ c__) \<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> (0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__) \<and> aa__ \<in> alphabet t\<^sub>1__ \<and> sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__ \<and> aa__ \<notin> alphabet t\<^sub>2__ \<and> sibling t\<^sub>1__ 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> (0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__) \<and> aa__ \<notin> alphabet t\<^sub>1__ \<and> sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__ \<and> aa__ \<in> alphabet t\<^sub>2__ \<and> sibling t\<^sub>2__ 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> (0 < height t\<^sub>1__ \<or> 0 < height 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a x22 x23. \<lbrakk>alphabet x22 \<inter> alphabet x23 = {}; consistent x22; consistent x23; \<forall>w\<^sub>b__ b__. x22 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> x23 \<noteq> Leaf w\<^sub>c__ c__); sibling x22 a \<in> alphabet x22 \<longrightarrow> a \<in> alphabet x22 \<longrightarrow> height x22 = 0 \<and> height x23 = 0 \<or> a \<in> alphabet x23 \<or> sibling x22 a \<in> alphabet x23; height x22 = 0 \<and> height x23 = 0 \<or> a \<in> alphabet x22 \<or> a \<in> alphabet x23\<rbrakk> \<Longrightarrow> (0 < height x22 \<or> 0 < height x23) \<and> a \<notin> alphabet x22 \<and> sibling x23 a \<notin> alphabet x22 \<and> a \<in> alphabet x23 \<and> sibling x23 a \<in> alphabet x23
 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply (rename_tac a t\<^sub>1 t\<^sub>2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); sibling t\<^sub>1 a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>1 \<longrightarrow> height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>2 \<or> sibling t\<^sub>1 a \<in> alphabet t\<^sub>2; height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>1 \<or> a \<in> alphabet t\<^sub>2\<rbrakk> \<Longrightarrow> (0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2) \<and> a \<notin> alphabet t\<^sub>1 \<and> sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1 \<and> a \<in> alphabet t\<^sub>2 \<and> sibling t\<^sub>2 a \<in> alphabet t\<^sub>2
 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> 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 "height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); sibling t\<^sub>1 a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>1 \<longrightarrow> height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>2 \<or> sibling t\<^sub>1 a \<in> alphabet t\<^sub>2; height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>1 \<or> a \<in> alphabet t\<^sub>2; height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0\<rbrakk> \<Longrightarrow> (0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2) \<and> a \<notin> alphabet t\<^sub>1 \<and> sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1 \<and> a \<in> alphabet t\<^sub>2 \<and> sibling t\<^sub>2 a \<in> alphabet t\<^sub>2
 2. \<And>a t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); sibling t\<^sub>1 a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>1 \<longrightarrow> height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>2 \<or> sibling t\<^sub>1 a \<in> alphabet t\<^sub>2; height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>1 \<or> a \<in> alphabet t\<^sub>2; \<not> (height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0)\<rbrakk> \<Longrightarrow> (0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2) \<and> a \<notin> alphabet t\<^sub>1 \<and> sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1 \<and> a \<in> alphabet t\<^sub>2 \<and> sibling t\<^sub>2 a \<in> alphabet t\<^sub>2
 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>a t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); sibling t\<^sub>1 a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>1 \<longrightarrow> height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>2 \<or> sibling t\<^sub>1 a \<in> alphabet t\<^sub>2; height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>1 \<or> a \<in> alphabet t\<^sub>2; \<not> (height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0)\<rbrakk> \<Longrightarrow> (0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2) \<and> a \<notin> alphabet t\<^sub>1 \<and> sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1 \<and> a \<in> alphabet t\<^sub>2 \<and> sibling t\<^sub>2 a \<in> alphabet t\<^sub>2
 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> 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\<^sub>1)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 x11 x12. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0; t\<^sub>1 = Leaf x11 x12\<rbrakk> \<Longrightarrow> False
 2. \<And>t\<^sub>1 t\<^sub>2 x21 x22 x23. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0; t\<^sub>1 = Node x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>a t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); sibling t\<^sub>1 a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>1 \<longrightarrow> height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>2 \<or> sibling t\<^sub>1 a \<in> alphabet t\<^sub>2; height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>1 \<or> a \<in> alphabet t\<^sub>2; \<not> (height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0)\<rbrakk> \<Longrightarrow> (0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2) \<and> a \<notin> alphabet t\<^sub>1 \<and> sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1 \<and> a \<in> alphabet t\<^sub>2 \<and> sibling t\<^sub>2 a \<in> alphabet t\<^sub>2
 4. wf ?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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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
 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> 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\<^sub>2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 x11 x12 x11a x12a. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0; t\<^sub>1 = Leaf x11 x12; t\<^sub>2 = Leaf x11a x12a\<rbrakk> \<Longrightarrow> False
 2. \<And>t\<^sub>1 t\<^sub>2 x11 x12 x21 x22 x23. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0; t\<^sub>1 = Leaf x11 x12; t\<^sub>2 = Node x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>t\<^sub>1 t\<^sub>2 x21 x22 x23. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0; t\<^sub>1 = Node x21 x22 x23\<rbrakk> \<Longrightarrow> False
 4. \<And>a t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); sibling t\<^sub>1 a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>1 \<longrightarrow> height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>2 \<or> sibling t\<^sub>1 a \<in> alphabet t\<^sub>2; height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>1 \<or> a \<in> alphabet t\<^sub>2; \<not> (height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0)\<rbrakk> \<Longrightarrow> (0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2) \<and> a \<notin> alphabet t\<^sub>1 \<and> sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1 \<and> a \<in> alphabet t\<^sub>2 \<and> sibling t\<^sub>2 a \<in> alphabet t\<^sub>2
 5. wf ?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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> 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 (6 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 x11 x12 x21 x22 x23. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0; t\<^sub>1 = Leaf x11 x12; t\<^sub>2 = Node x21 x22 x23\<rbrakk> \<Longrightarrow> False
 2. \<And>t\<^sub>1 t\<^sub>2 x21 x22 x23. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0; t\<^sub>1 = Node x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>a t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); sibling t\<^sub>1 a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>1 \<longrightarrow> height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>2 \<or> sibling t\<^sub>1 a \<in> alphabet t\<^sub>2; height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0 \<or> a \<in> alphabet t\<^sub>1 \<or> a \<in> alphabet t\<^sub>2; \<not> (height t\<^sub>1 = 0 \<and> height t\<^sub>2 = 0)\<rbrakk> \<Longrightarrow> (0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2) \<and> a \<notin> alphabet t\<^sub>1 \<and> sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1 \<and> a \<in> alphabet t\<^sub>2 \<and> sibling t\<^sub>2 a \<in> alphabet t\<^sub>2
 4. wf ?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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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
 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a t\<^sub>1 t\<^sub>2. \<lbrakk>alphabet t\<^sub>1 \<inter> alphabet t\<^sub>2 = {}; consistent t\<^sub>1; consistent t\<^sub>2; \<forall>w\<^sub>b__ b__. t\<^sub>1 = Leaf w\<^sub>b__ b__ \<longrightarrow> (\<forall>w\<^sub>c__ c__. b__ = c__ \<or> t\<^sub>2 \<noteq> Leaf w\<^sub>c__ c__); sibling t\<^sub>1 a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>1 \<longrightarrow> a \<in> alphabet t\<^sub>2 \<or> sibling t\<^sub>1 a \<in> alphabet t\<^sub>2; a \<in> alphabet t\<^sub>1 \<or> a \<in> alphabet t\<^sub>2; 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2\<rbrakk> \<Longrightarrow> a \<notin> alphabet t\<^sub>1 \<and> sibling t\<^sub>2 a \<notin> alphabet t\<^sub>1 \<and> a \<in> alphabet t\<^sub>2 \<and> sibling t\<^sub>2 a \<in> alphabet t\<^sub>2
 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> alphabet t\<^sub>2__\<rbrakk> \<Longrightarrow> ((t\<^sub>2__, aa__), Node w__ t\<^sub>1__ t\<^sub>2__, aa__) \<in> ?R2
[PROOF STEP]
apply (auto intro: in_alphabet_imp_sibling_in_alphabet)[1]
[PROOF STATE]
proof (prove)
goal (3 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<in> alphabet t\<^sub>1__; sibling t\<^sub>1__ aa__ \<in> alphabet t\<^sub>1__; aa__ \<notin> alphabet t\<^sub>2__; sibling 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__ = {}; 0 < height t\<^sub>1__ \<or> 0 < height t\<^sub>2__; aa__ \<notin> alphabet t\<^sub>1__; sibling t\<^sub>2__ aa__ \<notin> alphabet t\<^sub>1__; aa__ \<in> alphabet t\<^sub>2__; sibling t\<^sub>2__ aa__ \<in> 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 sibling_sibling_id[simp]:
"consistent t \<Longrightarrow> sibling t (sibling t a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> sibling t (sibling t a) = a
[PROOF STEP]
by (induct t a rule: sibling_induct_consistent) simp+


[STATEMENT]
lemma sibling_reciprocal:
"\<lbrakk>consistent t; sibling t a = b\<rbrakk> \<Longrightarrow> sibling t b = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; sibling t a = b\<rbrakk> \<Longrightarrow> sibling t b = a
[PROOF STEP]
by auto


[STATEMENT]
lemma depth_height_imp_sibling_ne:
"\<lbrakk>consistent t; depth t a = height t; height t > 0; a \<in> alphabet t\<rbrakk> \<Longrightarrow>
 sibling t a \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; depth t a = height t; 0 < height t; a \<in> alphabet t\<rbrakk> \<Longrightarrow> sibling t a \<noteq> a
[PROOF STEP]
by (induct t a rule: sibling_induct_consistent) auto


[STATEMENT]
lemma depth_sibling[simp]:
"consistent t \<Longrightarrow> depth t (sibling t a) = depth t a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> depth t (sibling t a) = depth t a
[PROOF STEP]
by (induct t a rule: sibling_induct_consistent) simp+


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


[STATEMENT]
lemma swapLeaves_id[simp]:
"consistent t \<Longrightarrow> swapLeaves t (freq t a) a (freq t a) a = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> swapLeaves t (freq t a) a (freq t a) a = t
[PROOF STEP]
by (induct t a rule: tree_induct_consistent) simp+


[STATEMENT]
lemma alphabet_swapLeaves:
"alphabet (swapLeaves t w\<^sub>a a w\<^sub>b b) =
     (if a \<in> alphabet t then
        if b \<in> alphabet t then alphabet t else (alphabet t - {a}) \<union> {b}
      else
        if b \<in> alphabet t then (alphabet t - {b}) \<union> {a} else alphabet t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet (swapLeaves t w\<^sub>a a w\<^sub>b b) = (if a \<in> alphabet t then if b \<in> alphabet t then alphabet t else alphabet t - {a} \<union> {b} else if b \<in> alphabet t then alphabet t - {b} \<union> {a} else alphabet t)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma consistent_swapLeaves[simp]:
"consistent t \<Longrightarrow> consistent (swapLeaves t w\<^sub>a a w\<^sub>b b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> consistent (swapLeaves t w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by (induct t) (auto simp: alphabet_swapLeaves)


[STATEMENT]
lemma depth_swapLeaves_neither[simp]:
"\<lbrakk>consistent t; c \<noteq> a; c \<noteq> b\<rbrakk> \<Longrightarrow> depth (swapLeaves t w\<^sub>a a w\<^sub>b b) c = depth t c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; c \<noteq> a; c \<noteq> b\<rbrakk> \<Longrightarrow> depth (swapLeaves t w\<^sub>a a w\<^sub>b b) c = depth t c
[PROOF STEP]
by (induct t a rule: tree_induct_consistent) (auto simp: alphabet_swapLeaves)


[STATEMENT]
lemma height_swapLeaves[simp]:
"height (swapLeaves t w\<^sub>a a w\<^sub>b b) = height t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. height (swapLeaves t w\<^sub>a a w\<^sub>b b) = height t
[PROOF STEP]
by (induct t) simp+


[STATEMENT]
lemma freq_swapLeaves[simp]:
"\<lbrakk>consistent t; a \<noteq> b\<rbrakk> \<Longrightarrow>
 freq (swapLeaves t w\<^sub>a a w\<^sub>b b) =
     (\<lambda>c. if c = a then if b \<in> alphabet t then w\<^sub>a else 0
          else if c = b then if a \<in> alphabet t then w\<^sub>b else 0
          else freq t c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; a \<noteq> b\<rbrakk> \<Longrightarrow> freq (swapLeaves t w\<^sub>a a w\<^sub>b b) = (\<lambda>c. if c = a then if b \<in> alphabet t then w\<^sub>a else 0 else if c = b then if a \<in> alphabet t then w\<^sub>b else 0 else freq t c)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>consistent t; a \<noteq> b\<rbrakk> \<Longrightarrow> freq (swapLeaves t w\<^sub>a a w\<^sub>b b) c = (if c = a then if b \<in> alphabet t then w\<^sub>a else 0 else if c = b then if a \<in> alphabet t then w\<^sub>b else 0 else freq t c)
[PROOF STEP]
apply (induct t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 c. \<lbrakk>consistent (Leaf x1 x2); a \<noteq> b\<rbrakk> \<Longrightarrow> freq (swapLeaves (Leaf x1 x2) w\<^sub>a a w\<^sub>b b) c = (if c = a then if b \<in> alphabet (Leaf x1 x2) then w\<^sub>a else 0 else if c = b then if a \<in> alphabet (Leaf x1 x2) then w\<^sub>b else 0 else freq (Leaf x1 x2) c)
 2. \<And>x1 t1 t2 c. \<lbrakk>\<And>c. \<lbrakk>consistent t1; a \<noteq> b\<rbrakk> \<Longrightarrow> freq (swapLeaves t1 w\<^sub>a a w\<^sub>b b) c = (if c = a then if b \<in> alphabet t1 then w\<^sub>a else 0 else if c = b then if a \<in> alphabet t1 then w\<^sub>b else 0 else freq t1 c); \<And>c. \<lbrakk>consistent t2; a \<noteq> b\<rbrakk> \<Longrightarrow> freq (swapLeaves t2 w\<^sub>a a w\<^sub>b b) c = (if c = a then if b \<in> alphabet t2 then w\<^sub>a else 0 else if c = b then if a \<in> alphabet t2 then w\<^sub>b else 0 else freq t2 c); consistent (Node x1 t1 t2); a \<noteq> b\<rbrakk> \<Longrightarrow> freq (swapLeaves (Node x1 t1 t2) w\<^sub>a a w\<^sub>b b) c = (if c = a then if b \<in> alphabet (Node x1 t1 t2) then w\<^sub>a else 0 else if c = b then if a \<in> alphabet (Node x1 t1 t2) then w\<^sub>b else 0 else freq (Node x1 t1 t2) c)
[PROOF STEP]
by auto