[STATEMENT]
lemma weight_swapLeaves:
"\<lbrakk>consistent t; a \<noteq> b\<rbrakk> \<Longrightarrow>
 if a \<in> alphabet t then
   if b \<in> alphabet t then
     weight (swapLeaves t w\<^sub>a a w\<^sub>b b) + freq t a + freq t b =
         weight t + w\<^sub>a + w\<^sub>b
   else
     weight (swapLeaves t w\<^sub>a a w\<^sub>b b) + freq t a = weight t + w\<^sub>b
 else
   if b \<in> alphabet t then
     weight (swapLeaves t w\<^sub>a a w\<^sub>b b) + freq t b = weight t + w\<^sub>a
   else
     weight (swapLeaves t w\<^sub>a a w\<^sub>b b) = weight t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet t then if b \<in> alphabet t then weight (swapLeaves t w\<^sub>a a w\<^sub>b b) + freq t a + freq t b = weight t + w\<^sub>a + w\<^sub>b else weight (swapLeaves t w\<^sub>a a w\<^sub>b b) + freq t a = weight t + w\<^sub>b else if b \<in> alphabet t then weight (swapLeaves t w\<^sub>a a w\<^sub>b b) + freq t b = weight t + w\<^sub>a else weight (swapLeaves t w\<^sub>a a w\<^sub>b b) = weight t
[PROOF STEP]
proof (induct t a rule: tree_induct_consistent)
  \<comment> \<open>{\sc Base case:}\enspace $t = @{term "Leaf w b"}$\<close>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>w\<^sub>b' ba a. a \<noteq> b \<Longrightarrow> if a \<in> alphabet (Leaf w\<^sub>b' ba) then if b \<in> alphabet (Leaf w\<^sub>b' ba) then weight (swapLeaves (Leaf w\<^sub>b' ba) w\<^sub>a a w\<^sub>b b) + freq (Leaf w\<^sub>b' ba) a + freq (Leaf w\<^sub>b' ba) b = weight (Leaf w\<^sub>b' ba) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Leaf w\<^sub>b' ba) w\<^sub>a a w\<^sub>b b) + freq (Leaf w\<^sub>b' ba) a = weight (Leaf w\<^sub>b' ba) + w\<^sub>b else if b \<in> alphabet (Leaf w\<^sub>b' ba) then weight (swapLeaves (Leaf w\<^sub>b' ba) w\<^sub>a a w\<^sub>b b) + freq (Leaf w\<^sub>b' ba) b = weight (Leaf w\<^sub>b' ba) + w\<^sub>a else weight (swapLeaves (Leaf w\<^sub>b' ba) w\<^sub>a a w\<^sub>b b) = weight (Leaf w\<^sub>b' ba)
 2. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 3. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 4. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:
a_ \<noteq> b

goal (4 subgoals):
 1. \<And>w\<^sub>b' ba a. a \<noteq> b \<Longrightarrow> if a \<in> alphabet (Leaf w\<^sub>b' ba) then if b \<in> alphabet (Leaf w\<^sub>b' ba) then weight (swapLeaves (Leaf w\<^sub>b' ba) w\<^sub>a a w\<^sub>b b) + freq (Leaf w\<^sub>b' ba) a + freq (Leaf w\<^sub>b' ba) b = weight (Leaf w\<^sub>b' ba) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Leaf w\<^sub>b' ba) w\<^sub>a a w\<^sub>b b) + freq (Leaf w\<^sub>b' ba) a = weight (Leaf w\<^sub>b' ba) + w\<^sub>b else if b \<in> alphabet (Leaf w\<^sub>b' ba) then weight (swapLeaves (Leaf w\<^sub>b' ba) w\<^sub>a a w\<^sub>b b) + freq (Leaf w\<^sub>b' ba) b = weight (Leaf w\<^sub>b' ba) + w\<^sub>a else weight (swapLeaves (Leaf w\<^sub>b' ba) w\<^sub>a a w\<^sub>b b) = weight (Leaf w\<^sub>b' ba)
 2. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 3. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 4. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a_ \<noteq> b

goal (1 subgoal):
 1. if a_ \<in> alphabet (Leaf w\<^sub>b_ b_) then if b \<in> alphabet (Leaf w\<^sub>b_ b_) then weight (swapLeaves (Leaf w\<^sub>b_ b_) w\<^sub>a a_ w\<^sub>b b) + freq (Leaf w\<^sub>b_ b_) a_ + freq (Leaf w\<^sub>b_ b_) b = weight (Leaf w\<^sub>b_ b_) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Leaf w\<^sub>b_ b_) w\<^sub>a a_ w\<^sub>b b) + freq (Leaf w\<^sub>b_ b_) a_ = weight (Leaf w\<^sub>b_ b_) + w\<^sub>b else if b \<in> alphabet (Leaf w\<^sub>b_ b_) then weight (swapLeaves (Leaf w\<^sub>b_ b_) w\<^sub>a a_ w\<^sub>b b) + freq (Leaf w\<^sub>b_ b_) b = weight (Leaf w\<^sub>b_ b_) + w\<^sub>a else weight (swapLeaves (Leaf w\<^sub>b_ b_) w\<^sub>a a_ w\<^sub>b b) = weight (Leaf w\<^sub>b_ b_)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
if a_ \<in> alphabet (Leaf w\<^sub>b_ b_) then if b \<in> alphabet (Leaf w\<^sub>b_ b_) then weight (swapLeaves (Leaf w\<^sub>b_ b_) w\<^sub>a a_ w\<^sub>b b) + freq (Leaf w\<^sub>b_ b_) a_ + freq (Leaf w\<^sub>b_ b_) b = weight (Leaf w\<^sub>b_ b_) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Leaf w\<^sub>b_ b_) w\<^sub>a a_ w\<^sub>b b) + freq (Leaf w\<^sub>b_ b_) a_ = weight (Leaf w\<^sub>b_ b_) + w\<^sub>b else if b \<in> alphabet (Leaf w\<^sub>b_ b_) then weight (swapLeaves (Leaf w\<^sub>b_ b_) w\<^sub>a a_ w\<^sub>b b) + freq (Leaf w\<^sub>b_ b_) b = weight (Leaf w\<^sub>b_ b_) + w\<^sub>a else weight (swapLeaves (Leaf w\<^sub>b_ b_) w\<^sub>a a_ w\<^sub>b b) = weight (Leaf w\<^sub>b_ b_)

goal (3 subgoals):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 3. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
next
  \<comment> \<open>{\sc Induction step:}\enspace $t = @{term "Node w t\<^sub>1 t\<^sub>2"}$\<close>
  \<comment> \<open>{\sc Subcase 1:}\enspace $a$ belongs to @{term t\<^sub>1} but not to
        @{term t\<^sub>2}\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 3. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
case (step\<^sub>1 w t\<^sub>1 t\<^sub>2 a)
[PROOF STATE]
proof (state)
this:
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (3 subgoals):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 3. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
assume b: "b \<in> alphabet t\<^sub>1"
[PROOF STATE]
proof (state)
this:
b \<in> alphabet t\<^sub>1

goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
hence "b \<notin> alphabet t\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2
[PROOF STEP]
using step\<^sub>1
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>2

goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>2

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
using b step\<^sub>1
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>2
b \<in> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
assume "b \<notin> alphabet t\<^sub>1"
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
using step\<^sub>1
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal (2 subgoals):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
next
  \<comment> \<open>{\sc Subcase 2:}\enspace $a$ belongs to @{term t\<^sub>2} but not to
        @{term t\<^sub>1}\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
case (step\<^sub>2 w t\<^sub>1 t\<^sub>2 a)
[PROOF STATE]
proof (state)
this:
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (2 subgoals):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
assume b: "b \<in> alphabet t\<^sub>1"
[PROOF STATE]
proof (state)
this:
b \<in> alphabet t\<^sub>1

goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
hence "b \<notin> alphabet t\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2
[PROOF STEP]
using step\<^sub>2
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>2

goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>2

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
using b step\<^sub>2
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>2
b \<in> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
assume "b \<notin> alphabet t\<^sub>1"
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
using step\<^sub>2
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
next
  \<comment> \<open>{\sc Subcase 3:}\enspace $a$ belongs to neither @{term t\<^sub>1} nor
        @{term t\<^sub>2}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
case (step\<^sub>3 w t\<^sub>1 t\<^sub>2 a)
[PROOF STATE]
proof (state)
this:
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. \<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; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1; a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2; a \<noteq> b\<rbrakk> \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
assume b: "b \<in> alphabet t\<^sub>1"
[PROOF STATE]
proof (state)
this:
b \<in> alphabet t\<^sub>1

goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
hence "b \<notin> alphabet t\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2
[PROOF STEP]
using step\<^sub>3
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>2

goal (2 subgoals):
 1. ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
 2. \<not> ?P \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>2

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
using b step\<^sub>3
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>2
b \<in> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
assume "b \<notin> alphabet t\<^sub>1"
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
using step\<^sub>3
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>1
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
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>1 then if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 a = weight t\<^sub>1 + w\<^sub>b else if b \<in> alphabet t\<^sub>1 then weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>1 b = weight t\<^sub>1 + w\<^sub>a else weight (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>1
a \<noteq> b \<Longrightarrow> if a \<in> alphabet t\<^sub>2 then if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a + w\<^sub>b else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 a = weight t\<^sub>2 + w\<^sub>b else if b \<in> alphabet t\<^sub>2 then weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) + freq t\<^sub>2 b = weight t\<^sub>2 + w\<^sub>a else weight (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>b b) = weight t\<^sub>2
a \<noteq> b

goal (1 subgoal):
 1. if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
if a \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a + w\<^sub>b else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) a = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>b else if b \<in> alphabet (Node w t\<^sub>1 t\<^sub>2) then weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) + freq (Node w t\<^sub>1 t\<^sub>2) b = weight (Node w t\<^sub>1 t\<^sub>2) + w\<^sub>a else weight (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>b b) = weight (Node w t\<^sub>1 t\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed