[STATEMENT]
lemma sibling_swapLeaves_sibling[simp]:
"\<lbrakk>consistent t; sibling t b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow>
 sibling (swapLeaves t w\<^sub>a a w\<^sub>s (sibling t b)) a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; sibling t b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t w\<^sub>a a w\<^sub>s (sibling t b)) a = b
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>consistent (Leaf x1 x2); sibling (Leaf x1 x2) b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves (Leaf x1 x2) w\<^sub>a a w\<^sub>s (sibling (Leaf x1 x2) b)) a = b
 2. \<And>x1 t1 t2. \<lbrakk>\<lbrakk>consistent t1; sibling t1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t1 w\<^sub>a a w\<^sub>s (sibling t1 b)) a = b; \<lbrakk>consistent t2; sibling t2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t2 w\<^sub>a a w\<^sub>s (sibling t2 b)) a = b; consistent (Node x1 t1 t2); sibling (Node x1 t1 t2) b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves (Node x1 t1 t2) w\<^sub>a a w\<^sub>s (sibling (Node x1 t1 t2) b)) a = b
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
consistent (Leaf x1_ x2_)
sibling (Leaf x1_ x2_) b \<noteq> b
a \<noteq> b

goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>consistent (Leaf x1 x2); sibling (Leaf x1 x2) b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves (Leaf x1 x2) w\<^sub>a a w\<^sub>s (sibling (Leaf x1 x2) b)) a = b
 2. \<And>x1 t1 t2. \<lbrakk>\<lbrakk>consistent t1; sibling t1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t1 w\<^sub>a a w\<^sub>s (sibling t1 b)) a = b; \<lbrakk>consistent t2; sibling t2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t2 w\<^sub>a a w\<^sub>s (sibling t2 b)) a = b; consistent (Node x1 t1 t2); sibling (Node x1 t1 t2) b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves (Node x1 t1 t2) w\<^sub>a a w\<^sub>s (sibling (Node x1 t1 t2) b)) a = b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
consistent (Leaf x1_ x2_)
sibling (Leaf x1_ x2_) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Leaf x1_ x2_) w\<^sub>a a w\<^sub>s (sibling (Leaf x1_ x2_) b)) a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Leaf x1_ x2_) w\<^sub>a a w\<^sub>s (sibling (Leaf x1_ x2_) b)) a = b

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>\<lbrakk>consistent t1; sibling t1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t1 w\<^sub>a a w\<^sub>s (sibling t1 b)) a = b; \<lbrakk>consistent t2; sibling t2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t2 w\<^sub>a a w\<^sub>s (sibling t2 b)) a = b; consistent (Node x1 t1 t2); sibling (Node x1 t1 t2) b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves (Node x1 t1 t2) w\<^sub>a a w\<^sub>s (sibling (Node x1 t1 t2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>\<lbrakk>consistent t1; sibling t1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t1 w\<^sub>a a w\<^sub>s (sibling t1 b)) a = b; \<lbrakk>consistent t2; sibling t2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t2 w\<^sub>a a w\<^sub>s (sibling t2 b)) a = b; consistent (Node x1 t1 t2); sibling (Node x1 t1 t2) b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves (Node x1 t1 t2) w\<^sub>a a w\<^sub>s (sibling (Node x1 t1 t2) b)) a = b
[PROOF STEP]
case (Node w t\<^sub>1 t\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>\<lbrakk>consistent t1; sibling t1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t1 w\<^sub>a a w\<^sub>s (sibling t1 b)) a = b; \<lbrakk>consistent t2; sibling t2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t2 w\<^sub>a a w\<^sub>s (sibling t2 b)) a = b; consistent (Node x1 t1 t2); sibling (Node x1 t1 t2) b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves (Node x1 t1 t2) w\<^sub>a a w\<^sub>s (sibling (Node x1 t1 t2) b)) a = b
[PROOF STEP]
note hyps = Node
[PROOF STATE]
proof (state)
this:
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. \<And>x1 t1 t2. \<lbrakk>\<lbrakk>consistent t1; sibling t1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t1 w\<^sub>a a w\<^sub>s (sibling t1 b)) a = b; \<lbrakk>consistent t2; sibling t2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t2 w\<^sub>a a w\<^sub>s (sibling t2 b)) a = b; consistent (Node x1 t1 t2); sibling (Node x1 t1 t2) b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves (Node x1 t1 t2) w\<^sub>a a w\<^sub>s (sibling (Node x1 t1 t2) b)) a = b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof (cases "height t\<^sub>1 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. height t\<^sub>1 = 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. height t\<^sub>1 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
height t\<^sub>1 = 0

goal (2 subgoals):
 1. height t\<^sub>1 = 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. height t\<^sub>1 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note h\<^sub>1 = True
[PROOF STATE]
proof (state)
this:
height t\<^sub>1 = 0

goal (2 subgoals):
 1. height t\<^sub>1 = 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. height t\<^sub>1 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof (cases t\<^sub>1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>1 = Leaf x11 x12 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<And>x21 x22 x23. t\<^sub>1 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case (Leaf w\<^sub>c c)
[PROOF STATE]
proof (state)
this:
t\<^sub>1 = Leaf w\<^sub>c c

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>1 = Leaf x11 x12 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<And>x21 x22 x23. t\<^sub>1 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note l\<^sub>1 = Leaf
[PROOF STATE]
proof (state)
this:
t\<^sub>1 = Leaf w\<^sub>c c

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>1 = Leaf x11 x12 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<And>x21 x22 x23. t\<^sub>1 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof (cases "height t\<^sub>2 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. height t\<^sub>2 = 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
height t\<^sub>2 = 0

goal (2 subgoals):
 1. height t\<^sub>2 = 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note h\<^sub>2 = True
[PROOF STATE]
proof (state)
this:
height t\<^sub>2 = 0

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

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>2 = Leaf x11 x12 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t\<^sub>2 = Leaf x11_ x12_

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using l\<^sub>1 hyps
[PROOF STATE]
proof (prove)
using this:
t\<^sub>2 = Leaf x11_ x12_
t\<^sub>1 = Leaf w\<^sub>c c
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by auto metis+
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case Node
[PROOF STATE]
proof (state)
this:
t\<^sub>2 = Node x21_ x22_ x23_

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t\<^sub>2 = Node x21_ x22_ x23_

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using h\<^sub>2
[PROOF STATE]
proof (prove)
using this:
t\<^sub>2 = Node x21_ x22_ x23_
height t\<^sub>2 = 0

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
height t\<^sub>2 \<noteq> 0

goal (1 subgoal):
 1. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note h\<^sub>2 = False
[PROOF STATE]
proof (state)
this:
height t\<^sub>2 \<noteq> 0

goal (1 subgoal):
 1. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<not> ?P \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
assume "c = b"
[PROOF STATE]
proof (state)
this:
c = b

goal (2 subgoals):
 1. ?P \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<not> ?P \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c = b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using l\<^sub>1 h\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
c = b
t\<^sub>1 = Leaf w\<^sub>c c
height t\<^sub>2 \<noteq> 0
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. c \<noteq> b \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> b \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
assume "c \<noteq> b"
[PROOF STATE]
proof (state)
this:
c \<noteq> b

goal (1 subgoal):
 1. c \<noteq> b \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
have "sibling t\<^sub>2 b \<in> alphabet t\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling t\<^sub>2 b \<in> alphabet t\<^sub>2
[PROOF STEP]
using \<open>c \<noteq> b\<close> l\<^sub>1 h\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
c \<noteq> b
t\<^sub>1 = Leaf w\<^sub>c c
height t\<^sub>2 \<noteq> 0
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling t\<^sub>2 b \<in> alphabet t\<^sub>2
[PROOF STEP]
by (simp add: sibling_ne_imp_sibling_in_alphabet)
[PROOF STATE]
proof (state)
this:
sibling t\<^sub>2 b \<in> alphabet t\<^sub>2

goal (1 subgoal):
 1. c \<noteq> b \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sibling t\<^sub>2 b \<in> alphabet t\<^sub>2

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using \<open>c \<noteq> b\<close> l\<^sub>1 h\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
sibling t\<^sub>2 b \<in> alphabet t\<^sub>2
c \<noteq> b
t\<^sub>1 = Leaf w\<^sub>c c
height t\<^sub>2 \<noteq> 0
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>1 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>1 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case Node
[PROOF STATE]
proof (state)
this:
t\<^sub>1 = Node x21_ x22_ x23_

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>1 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t\<^sub>1 = Node x21_ x22_ x23_

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using h\<^sub>1
[PROOF STATE]
proof (prove)
using this:
t\<^sub>1 = Node x21_ x22_ x23_
height t\<^sub>1 = 0

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. height t\<^sub>1 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. height t\<^sub>1 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
height t\<^sub>1 \<noteq> 0

goal (1 subgoal):
 1. height t\<^sub>1 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note h\<^sub>1 = False
[PROOF STATE]
proof (state)
this:
height t\<^sub>1 \<noteq> 0

goal (1 subgoal):
 1. height t\<^sub>1 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof (cases "height t\<^sub>2 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. height t\<^sub>2 = 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
height t\<^sub>2 = 0

goal (2 subgoals):
 1. height t\<^sub>2 = 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note h\<^sub>2 = True
[PROOF STATE]
proof (state)
this:
height t\<^sub>2 = 0

goal (2 subgoals):
 1. height t\<^sub>2 = 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof (cases t\<^sub>2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>2 = Leaf x11 x12 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case (Leaf w\<^sub>d d)
[PROOF STATE]
proof (state)
this:
t\<^sub>2 = Leaf w\<^sub>d d

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>2 = Leaf x11 x12 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note l\<^sub>2 = Leaf
[PROOF STATE]
proof (state)
this:
t\<^sub>2 = Leaf w\<^sub>d d

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>2 = Leaf x11 x12 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<not> ?P \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
assume "d = b"
[PROOF STATE]
proof (state)
this:
d = b

goal (2 subgoals):
 1. ?P \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. \<not> ?P \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d = b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using h\<^sub>1 l\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
d = b
height t\<^sub>1 \<noteq> 0
t\<^sub>2 = Leaf w\<^sub>d d
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. d \<noteq> b \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d \<noteq> b \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
assume "d \<noteq> b"
[PROOF STATE]
proof (state)
this:
d \<noteq> b

goal (1 subgoal):
 1. d \<noteq> b \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof (cases "b \<in> alphabet t\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<in> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b \<in> alphabet t\<^sub>1

goal (2 subgoals):
 1. b \<in> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
hence "sibling t\<^sub>1 b \<in> alphabet t\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1

goal (1 subgoal):
 1. sibling t\<^sub>1 b \<in> alphabet t\<^sub>1
[PROOF STEP]
using \<open>d \<noteq> b\<close> h\<^sub>1 l\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
d \<noteq> b
height t\<^sub>1 \<noteq> 0
t\<^sub>2 = Leaf w\<^sub>d d
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling t\<^sub>1 b \<in> alphabet t\<^sub>1
[PROOF STEP]
by (simp add: sibling_ne_imp_sibling_in_alphabet)
[PROOF STATE]
proof (state)
this:
sibling t\<^sub>1 b \<in> alphabet t\<^sub>1

goal (2 subgoals):
 1. b \<in> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sibling t\<^sub>1 b \<in> alphabet t\<^sub>1

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using True \<open>d \<noteq> b\<close> h\<^sub>1 l\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
sibling t\<^sub>1 b \<in> alphabet t\<^sub>1
b \<in> alphabet t\<^sub>1
d \<noteq> b
height t\<^sub>1 \<noteq> 0
t\<^sub>2 = Leaf w\<^sub>d d
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by (simp add: alphabet_swapLeaves)
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using \<open>d \<noteq> b\<close> l\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>1
d \<noteq> b
t\<^sub>2 = Leaf w\<^sub>d d
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case Node
[PROOF STATE]
proof (state)
this:
t\<^sub>2 = Node x21_ x22_ x23_

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>2 = Node x21 x22 x23 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t\<^sub>2 = Node x21_ x22_ x23_

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using h\<^sub>2
[PROOF STATE]
proof (prove)
using this:
t\<^sub>2 = Node x21_ x22_ x23_
height t\<^sub>2 = 0

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
height t\<^sub>2 \<noteq> 0

goal (1 subgoal):
 1. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note h\<^sub>2 = False
[PROOF STATE]
proof (state)
this:
height t\<^sub>2 \<noteq> 0

goal (1 subgoal):
 1. height t\<^sub>2 \<noteq> 0 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof (cases "b \<in> alphabet t\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<in> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b \<in> alphabet t\<^sub>1

goal (2 subgoals):
 1. b \<in> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using h\<^sub>1 h\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>1
height t\<^sub>1 \<noteq> 0
height t\<^sub>2 \<noteq> 0
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
note b\<^sub>1 = False
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>1 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
proof (cases "b \<in> alphabet t\<^sub>2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<in> alphabet t\<^sub>2 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. b \<notin> alphabet t\<^sub>2 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b \<in> alphabet t\<^sub>2

goal (2 subgoals):
 1. b \<in> alphabet t\<^sub>2 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
 2. b \<notin> alphabet t\<^sub>2 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>2

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using b\<^sub>1 h\<^sub>1 h\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
b \<in> alphabet t\<^sub>2
b \<notin> alphabet t\<^sub>1
height t\<^sub>1 \<noteq> 0
height t\<^sub>2 \<noteq> 0
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by (auto simp: in_alphabet_imp_sibling_in_alphabet
                           alphabet_swapLeaves)
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<notin> alphabet t\<^sub>2

goal (1 subgoal):
 1. b \<notin> alphabet t\<^sub>2 \<Longrightarrow> sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>2

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
using b\<^sub>1 h\<^sub>1 h\<^sub>2 hyps
[PROOF STATE]
proof (prove)
using this:
b \<notin> alphabet t\<^sub>2
b \<notin> alphabet t\<^sub>1
height t\<^sub>1 \<noteq> 0
height t\<^sub>2 \<noteq> 0
\<lbrakk>consistent t\<^sub>1; sibling t\<^sub>1 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>1 w\<^sub>a a w\<^sub>s (sibling t\<^sub>1 b)) a = b
\<lbrakk>consistent t\<^sub>2; sibling t\<^sub>2 b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapLeaves t\<^sub>2 w\<^sub>a a w\<^sub>s (sibling t\<^sub>2 b)) a = b
consistent (Node w t\<^sub>1 t\<^sub>2)
sibling (Node w t\<^sub>1 t\<^sub>2) b \<noteq> b
a \<noteq> b

goal (1 subgoal):
 1. sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapLeaves (Node w t\<^sub>1 t\<^sub>2) w\<^sub>a a w\<^sub>s (sibling (Node w t\<^sub>1 t\<^sub>2) b)) a = b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma swapSyms_id[simp]:
"consistent t \<Longrightarrow> swapSyms t a a = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> swapSyms t a a = t
[PROOF STEP]
by (simp add: swapSyms_def)


[STATEMENT]
lemma alphabet_swapSyms[simp]:
"\<lbrakk>a \<in> alphabet t; b \<in> alphabet t\<rbrakk> \<Longrightarrow> alphabet (swapSyms t a b) = alphabet t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> alphabet t; b \<in> alphabet t\<rbrakk> \<Longrightarrow> alphabet (swapSyms t a b) = alphabet t
[PROOF STEP]
by (simp add: swapSyms_def alphabet_swapLeaves)


[STATEMENT]
lemma depth_swapSyms_neither[simp]:
"\<lbrakk>consistent t; c \<noteq> a; c \<noteq> b\<rbrakk> \<Longrightarrow>
 depth (swapSyms t a b) c = depth t c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; c \<noteq> a; c \<noteq> b\<rbrakk> \<Longrightarrow> depth (swapSyms t a b) c = depth t c
[PROOF STEP]
by (simp add: swapSyms_def)


[STATEMENT]
lemma freq_swapSyms[simp]:
"\<lbrakk>consistent t; a \<in> alphabet t; b \<in> alphabet t\<rbrakk> \<Longrightarrow>
 freq (swapSyms t a b) = freq t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; a \<in> alphabet t; b \<in> alphabet t\<rbrakk> \<Longrightarrow> freq (swapSyms t a b) = freq t
[PROOF STEP]
by (case_tac "a = b") (simp add: swapSyms_def ext)+


[STATEMENT]
lemma cost_swapSyms:
assumes "consistent t" "a \<in> alphabet t" "b \<in> alphabet t"
shows "cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b =
           cost t + freq t a * depth t b + freq t b * depth t a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
 2. \<not> ?P \<Longrightarrow> cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
assume "a = b"
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. ?P \<Longrightarrow> cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
 2. \<not> ?P \<Longrightarrow> cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = b
consistent t
a \<in> alphabet t
b \<in> alphabet t

goal (1 subgoal):
 1. cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
assume "a \<noteq> b"
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
hence "cost (swapLeaves t (freq t a) a (freq t b) b)
    + freq t a * depth t a + freq t b * depth t b =
    cost t + freq t a * depth t b + freq t b * depth t a"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. cost (swapLeaves t (freq t a) a (freq t b) b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b
consistent t
a \<in> alphabet t
b \<in> alphabet t

goal (1 subgoal):
 1. cost (swapLeaves t (freq t a) a (freq t b) b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
by (simp add: cost_swapLeaves)
[PROOF STATE]
proof (state)
this:
cost (swapLeaves t (freq t a) a (freq t b) b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cost (swapLeaves t (freq t a) a (freq t b) b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a

goal (1 subgoal):
 1. cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cost (swapLeaves t (freq t a) a (freq t b) b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
consistent t
a \<in> alphabet t
b \<in> alphabet t

goal (1 subgoal):
 1. cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a
[PROOF STEP]
by (simp add: swapSyms_def)
[PROOF STATE]
proof (state)
this:
cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b = cost t + freq t a * depth t b + freq t b * depth t a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma le_le_imp_sum_mult_le_sum_mult:
assumes "i \<le> j" "m \<le> (n::nat)"
shows "i * n + j * m \<le> i * m + j * n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i * n + j * m \<le> i * m + j * n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i * n + j * m \<le> i * m + j * n
[PROOF STEP]
have "i * m + i * (n - m) + j * m \<le> i * m + j * m + j * (n - m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i * m + i * (n - m) + j * m \<le> i * m + j * m + j * (n - m)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<le> j
m \<le> n

goal (1 subgoal):
 1. i * m + i * (n - m) + j * m \<le> i * m + j * m + j * (n - m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i * m + i * (n - m) + j * m \<le> i * m + j * m + j * (n - m)

goal (1 subgoal):
 1. i * n + j * m \<le> i * m + j * n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i * m + i * (n - m) + j * m \<le> i * m + j * m + j * (n - m)

goal (1 subgoal):
 1. i * n + j * m \<le> i * m + j * n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i * m + i * (n - m) + j * m \<le> i * m + j * m + j * (n - m)
i \<le> j
m \<le> n

goal (1 subgoal):
 1. i * n + j * m \<le> i * m + j * n
[PROOF STEP]
by (simp add: diff_mult_distrib2)
[PROOF STATE]
proof (state)
this:
i * n + j * m \<le> i * m + j * n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cost_swapSyms_le:
assumes "consistent t" "a \<in> alphabet t" "b \<in> alphabet t" "freq t a \<le> freq t b"
        "depth t a \<le> depth t b"
shows "cost (swapSyms t a b) \<le> cost t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
let ?aabb = "freq t a * depth t a + freq t b * depth t b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
let ?abba = "freq t a * depth t b + freq t b * depth t a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
have "?abba \<le> ?aabb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freq t a * depth t b + freq t b * depth t a \<le> freq t a * depth t a + freq t b * depth t b
[PROOF STEP]
using assms(4-5)
[PROOF STATE]
proof (prove)
using this:
freq t a \<le> freq t b
depth t a \<le> depth t b

goal (1 subgoal):
 1. freq t a * depth t b + freq t b * depth t a \<le> freq t a * depth t a + freq t b * depth t b
[PROOF STEP]
by (rule le_le_imp_sum_mult_le_sum_mult)
[PROOF STATE]
proof (state)
this:
freq t a * depth t b + freq t b * depth t a \<le> freq t a * depth t a + freq t b * depth t b

goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
have "cost (swapSyms t a b) + ?aabb = cost t + ?abba"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapSyms t a b) + (freq t a * depth t a + freq t b * depth t b) = cost t + (freq t a * depth t b + freq t b * depth t a)
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
consistent t
a \<in> alphabet t
b \<in> alphabet t

goal (1 subgoal):
 1. cost (swapSyms t a b) + (freq t a * depth t a + freq t b * depth t b) = cost t + (freq t a * depth t b + freq t b * depth t a)
[PROOF STEP]
by (simp add: cost_swapSyms add.assoc[THEN sym])
[PROOF STATE]
proof (state)
this:
cost (swapSyms t a b) + (freq t a * depth t a + freq t b * depth t b) = cost t + (freq t a * depth t b + freq t b * depth t a)

goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cost (swapSyms t a b) + (freq t a * depth t a + freq t b * depth t b) = cost t + (freq t a * depth t b + freq t b * depth t a)

goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
have "\<dots> \<le> cost t + ?aabb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost t + (freq t a * depth t b + freq t b * depth t a) \<le> cost t + (freq t a * depth t a + freq t b * depth t b)
[PROOF STEP]
using \<open>?abba \<le> ?aabb\<close>
[PROOF STATE]
proof (prove)
using this:
freq t a * depth t b + freq t b * depth t a \<le> freq t a * depth t a + freq t b * depth t b

goal (1 subgoal):
 1. cost t + (freq t a * depth t b + freq t b * depth t a) \<le> cost t + (freq t a * depth t a + freq t b * depth t b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cost t + (freq t a * depth t b + freq t b * depth t a) \<le> cost t + (freq t a * depth t a + freq t b * depth t b)

goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cost (swapSyms t a b) + (freq t a * depth t a + freq t b * depth t b) \<le> cost t + (freq t a * depth t a + freq t b * depth t b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cost (swapSyms t a b) + (freq t a * depth t a + freq t b * depth t b) \<le> cost t + (freq t a * depth t a + freq t b * depth t b)

goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
using assms(4-5)
[PROOF STATE]
proof (prove)
using this:
cost (swapSyms t a b) + (freq t a * depth t a + freq t b * depth t b) \<le> cost t + (freq t a * depth t a + freq t b * depth t b)
freq t a \<le> freq t b
depth t a \<le> depth t b

goal (1 subgoal):
 1. cost (swapSyms t a b) \<le> cost t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cost (swapSyms t a b) \<le> cost t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sibling_swapSyms_sibling[simp]:
"\<lbrakk>consistent t; sibling t b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow>
 sibling (swapSyms t a (sibling t b)) a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; sibling t b \<noteq> b; a \<noteq> b\<rbrakk> \<Longrightarrow> sibling (swapSyms t a (sibling t b)) a = b
[PROOF STEP]
by (simp add: swapSyms_def)


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


[STATEMENT]
lemma alphabet_swapFourSyms[simp]:
"\<lbrakk>a \<in> alphabet t; b \<in> alphabet t; c \<in> alphabet t; d \<in> alphabet t\<rbrakk> \<Longrightarrow>
 alphabet (swapFourSyms t a b c d) = alphabet t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> alphabet t; b \<in> alphabet t; c \<in> alphabet t; d \<in> alphabet t\<rbrakk> \<Longrightarrow> alphabet (swapFourSyms t a b c d) = alphabet t
[PROOF STEP]
by (simp add: swapFourSyms_def)


[STATEMENT]
lemma consistent_swapFourSyms[simp]:
"consistent t \<Longrightarrow> consistent (swapFourSyms t a b c d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> consistent (swapFourSyms t a b c d)
[PROOF STEP]
by (simp add: swapFourSyms_def)


[STATEMENT]
lemma freq_swapFourSyms[simp]:
"\<lbrakk>consistent t; a \<in> alphabet t; b \<in> alphabet t; c \<in> alphabet t;
  d \<in> alphabet t\<rbrakk> \<Longrightarrow>
 freq (swapFourSyms t a b c d) = freq t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; a \<in> alphabet t; b \<in> alphabet t; c \<in> alphabet t; d \<in> alphabet t\<rbrakk> \<Longrightarrow> freq (swapFourSyms t a b c d) = freq t
[PROOF STEP]
by (auto simp: swapFourSyms_def)


[STATEMENT]
lemma sibling_swapFourSyms_when_4th_is_sibling:
assumes "consistent t" "a \<in> alphabet t" "b \<in> alphabet t" "c \<in> alphabet t"
        "a \<noteq> b" "sibling t c \<noteq> c"
shows "sibling (swapFourSyms t a b c (sibling t c)) a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
proof (cases "a \<noteq> sibling t c \<and> b \<noteq> c")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<noteq> sibling t c \<and> b \<noteq> c \<Longrightarrow> sibling (swapFourSyms t a b c (sibling t c)) a = b
 2. \<not> (a \<noteq> sibling t c \<and> b \<noteq> c) \<Longrightarrow> sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<noteq> sibling t c \<and> b \<noteq> c

goal (2 subgoals):
 1. a \<noteq> sibling t c \<and> b \<noteq> c \<Longrightarrow> sibling (swapFourSyms t a b c (sibling t c)) a = b
 2. \<not> (a \<noteq> sibling t c \<and> b \<noteq> c) \<Longrightarrow> sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
let ?d = "sibling t c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
let ?t\<^sub>s = "swapFourSyms t a b c ?d"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
have abba: "(sibling ?t\<^sub>s a = b) = (sibling ?t\<^sub>s b = a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sibling (swapFourSyms t a b c (sibling t c)) a = b) = (sibling (swapFourSyms t a b c (sibling t c)) b = a)
[PROOF STEP]
using \<open>consistent t\<close>
[PROOF STATE]
proof (prove)
using this:
consistent t

goal (1 subgoal):
 1. (sibling (swapFourSyms t a b c (sibling t c)) a = b) = (sibling (swapFourSyms t a b c (sibling t c)) b = a)
[PROOF STEP]
by (metis consistent_swapFourSyms sibling_reciprocal)
[PROOF STATE]
proof (state)
this:
(sibling (swapFourSyms t a b c (sibling t c)) a = b) = (sibling (swapFourSyms t a b c (sibling t c)) b = a)

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
have s: "sibling t c = sibling (swapSyms t a c) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling t c = sibling (swapSyms t a c) a
[PROOF STEP]
using True assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> sibling t c \<and> b \<noteq> c
consistent t
a \<in> alphabet t
b \<in> alphabet t
c \<in> alphabet t
a \<noteq> b
sibling t c \<noteq> c

goal (1 subgoal):
 1. sibling t c = sibling (swapSyms t a c) a
[PROOF STEP]
by (metis sibling_reciprocal sibling_swapSyms_sibling)
[PROOF STATE]
proof (state)
this:
sibling t c = sibling (swapSyms t a c) a

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
have "sibling ?t\<^sub>s b = sibling (swapSyms t a c) ?d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) b = sibling (swapSyms t a c) (sibling t c)
[PROOF STEP]
using s True assms
[PROOF STATE]
proof (prove)
using this:
sibling t c = sibling (swapSyms t a c) a
a \<noteq> sibling t c \<and> b \<noteq> c
consistent t
a \<in> alphabet t
b \<in> alphabet t
c \<in> alphabet t
a \<noteq> b
sibling t c \<noteq> c

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) b = sibling (swapSyms t a c) (sibling t c)
[PROOF STEP]
by (auto simp: swapFourSyms_def)
[PROOF STATE]
proof (state)
this:
sibling (swapFourSyms t a b c (sibling t c)) b = sibling (swapSyms t a c) (sibling t c)

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sibling (swapFourSyms t a b c (sibling t c)) b = sibling (swapSyms t a c) (sibling t c)

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
have "\<dots> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapSyms t a c) (sibling t c) = a
[PROOF STEP]
using True assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> sibling t c \<and> b \<noteq> c
consistent t
a \<in> alphabet t
b \<in> alphabet t
c \<in> alphabet t
a \<noteq> b
sibling t c \<noteq> c

goal (1 subgoal):
 1. sibling (swapSyms t a c) (sibling t c) = a
[PROOF STEP]
by (metis sibling_reciprocal sibling_swapSyms_other_sibling swapLeaves_id swapSyms_def)
[PROOF STATE]
proof (state)
this:
sibling (swapSyms t a c) (sibling t c) = a

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sibling (swapFourSyms t a b c (sibling t c)) b = a
[PROOF STEP]
have "sibling ?t\<^sub>s b = a"
[PROOF STATE]
proof (prove)
using this:
sibling (swapFourSyms t a b c (sibling t c)) b = a

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) b = a
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sibling (swapFourSyms t a b c (sibling t c)) b = a

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
with abba
[PROOF STATE]
proof (chain)
picking this:
(sibling (swapFourSyms t a b c (sibling t c)) a = b) = (sibling (swapFourSyms t a b c (sibling t c)) b = a)
sibling (swapFourSyms t a b c (sibling t c)) b = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(sibling (swapFourSyms t a b c (sibling t c)) a = b) = (sibling (swapFourSyms t a b c (sibling t c)) b = a)
sibling (swapFourSyms t a b c (sibling t c)) b = a

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sibling (swapFourSyms t a b c (sibling t c)) a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sibling (swapFourSyms t a b c (sibling t c)) a = b

goal (1 subgoal):
 1. \<not> (a \<noteq> sibling t c \<and> b \<noteq> c) \<Longrightarrow> sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (a \<noteq> sibling t c \<and> b \<noteq> c) \<Longrightarrow> sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (a \<noteq> sibling t c \<and> b \<noteq> c)

goal (1 subgoal):
 1. \<not> (a \<noteq> sibling t c \<and> b \<noteq> c) \<Longrightarrow> sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (a \<noteq> sibling t c \<and> b \<noteq> c)

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> (a \<noteq> sibling t c \<and> b \<noteq> c)
consistent t
a \<in> alphabet t
b \<in> alphabet t
c \<in> alphabet t
a \<noteq> b
sibling t c \<noteq> c

goal (1 subgoal):
 1. sibling (swapFourSyms t a b c (sibling t c)) a = b
[PROOF STEP]
by (auto intro: sibling_reciprocal simp: swapFourSyms_def)
[PROOF STATE]
proof (state)
this:
sibling (swapFourSyms t a b c (sibling t c)) a = b

goal:
No subgoals!
[PROOF STEP]
qed


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


[STATEMENT]
lemma height_gt_0_imp_mergeSibling_left[simp]:
"height t\<^sub>1 > 0 \<Longrightarrow>
 mergeSibling (Node w t\<^sub>1 t\<^sub>2) a =
     Node w (mergeSibling t\<^sub>1 a) (mergeSibling t\<^sub>2 a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < height t\<^sub>1 \<Longrightarrow> mergeSibling (Node w t\<^sub>1 t\<^sub>2) a = Node w (mergeSibling t\<^sub>1 a) (mergeSibling t\<^sub>2 a)
[PROOF STEP]
by (case_tac t\<^sub>1) simp+


[STATEMENT]
lemma height_gt_0_imp_mergeSibling_right[simp]:
"height t\<^sub>2 > 0 \<Longrightarrow>
 mergeSibling (Node w t\<^sub>1 t\<^sub>2) a =
     Node w (mergeSibling t\<^sub>1 a) (mergeSibling t\<^sub>2 a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < height t\<^sub>2 \<Longrightarrow> mergeSibling (Node w t\<^sub>1 t\<^sub>2) a = Node w (mergeSibling t\<^sub>1 a) (mergeSibling t\<^sub>2 a)
[PROOF STEP]
by (case_tac t\<^sub>2) simp+


[STATEMENT]
lemma either_height_gt_0_imp_mergeSibling[simp]:
"height t\<^sub>1 > 0 \<or> height t\<^sub>2 > 0 \<Longrightarrow>
 mergeSibling (Node w t\<^sub>1 t\<^sub>2) a =
     Node w (mergeSibling t\<^sub>1 a) (mergeSibling t\<^sub>2 a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < height t\<^sub>1 \<or> 0 < height t\<^sub>2 \<Longrightarrow> mergeSibling (Node w t\<^sub>1 t\<^sub>2) a = Node w (mergeSibling t\<^sub>1 a) (mergeSibling t\<^sub>2 a)
[PROOF STEP]
by auto


[STATEMENT]
lemma alphabet_mergeSibling[simp]:
"\<lbrakk>consistent t; a \<in> alphabet t\<rbrakk> \<Longrightarrow>
 alphabet (mergeSibling t a) = (alphabet t - {sibling t a}) \<union> {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; a \<in> alphabet t\<rbrakk> \<Longrightarrow> alphabet (mergeSibling t a) = alphabet t - {sibling t a} \<union> {a}
[PROOF STEP]
by (induct t a rule: mergeSibling_induct_consistent) auto


[STATEMENT]
lemma consistent_mergeSibling[simp]:
"consistent t \<Longrightarrow> consistent (mergeSibling t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> consistent (mergeSibling t a)
[PROOF STEP]
by (induct t a rule: mergeSibling_induct_consistent) auto


[STATEMENT]
lemma freq_mergeSibling:
"\<lbrakk>consistent t; a \<in> alphabet t; sibling t a \<noteq> a\<rbrakk> \<Longrightarrow>
 freq (mergeSibling t a) =
     (\<lambda>c. if c = a then freq t a + freq t (sibling t a)
          else if c = sibling t a then 0
          else freq t c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; a \<in> alphabet t; sibling t a \<noteq> a\<rbrakk> \<Longrightarrow> freq (mergeSibling t a) = (\<lambda>c. if c = a then freq t a + freq t (sibling t a) else if c = sibling t a then 0 else freq t c)
[PROOF STEP]
by (induct t a rule: mergeSibling_induct_consistent) (auto simp: fun_eq_iff)


[STATEMENT]
lemma weight_mergeSibling[simp]:
"weight (mergeSibling t a) = weight t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (mergeSibling t a) = weight t
[PROOF STEP]
by (induct t a rule: mergeSibling.induct) simp+


[STATEMENT]
lemma cost_mergeSibling:
"\<lbrakk>consistent t; sibling t a \<noteq> a\<rbrakk> \<Longrightarrow>
 cost (mergeSibling t a) + freq t a + freq t (sibling t a) = cost t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; sibling t a \<noteq> a\<rbrakk> \<Longrightarrow> cost (mergeSibling t a) + freq t a + freq t (sibling t a) = cost t
[PROOF STEP]
by (induct t a rule: mergeSibling_induct_consistent) auto


[STATEMENT]
lemma notin_alphabet_imp_splitLeaf_id[simp]:
"a \<notin> alphabet t \<Longrightarrow> splitLeaf t w\<^sub>a a w\<^sub>b b = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> alphabet t \<Longrightarrow> splitLeaf t w\<^sub>a a w\<^sub>b b = t
[PROOF STEP]
by (induct t) simp+


[STATEMENT]
lemma notin_alphabet\<^sub>F_imp_splitLeaf\<^sub>F_id[simp]:
"a \<notin> alphabet\<^sub>F ts \<Longrightarrow> splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b = ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> alphabet\<^sub>F ts \<Longrightarrow> splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b = ts
[PROOF STEP]
by (induct ts) simp+


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


[STATEMENT]
lemma consistent_splitLeaf[simp]:
"\<lbrakk>consistent t; b \<notin> alphabet t\<rbrakk> \<Longrightarrow> consistent (splitLeaf t w\<^sub>a a w\<^sub>b b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; b \<notin> alphabet t\<rbrakk> \<Longrightarrow> consistent (splitLeaf t w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma freq_splitLeaf[simp]:
"\<lbrakk>consistent t; b \<notin> alphabet t\<rbrakk> \<Longrightarrow>
 freq (splitLeaf t w\<^sub>a a w\<^sub>b b) =
 (if a \<in> alphabet t then (\<lambda>c. if c = a then w\<^sub>a else if c = b then w\<^sub>b else freq t c)
  else freq t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; b \<notin> alphabet t\<rbrakk> \<Longrightarrow> freq (splitLeaf t w\<^sub>a a w\<^sub>b b) = (if a \<in> alphabet t then \<lambda>c. if c = a then w\<^sub>a else if c = b then w\<^sub>b else freq t c else freq t)
[PROOF STEP]
by (induct t b rule: tree_induct_consistent) (rule ext, auto)+


[STATEMENT]
lemma weight_splitLeaf[simp]:
"\<lbrakk>consistent t; a \<in> alphabet t; freq t a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow>
 weight (splitLeaf t w\<^sub>a a w\<^sub>b b) = weight t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; a \<in> alphabet t; freq t a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> weight (splitLeaf t w\<^sub>a a w\<^sub>b b) = weight t
[PROOF STEP]
by (induct t a rule: tree_induct_consistent) simp+


[STATEMENT]
lemma cost_splitLeaf[simp]:
"\<lbrakk>consistent t; a \<in> alphabet t; freq t a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow>
 cost (splitLeaf t w\<^sub>a a w\<^sub>b b) = cost t + w\<^sub>a + w\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent t; a \<in> alphabet t; freq t a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) = cost t + w\<^sub>a + w\<^sub>b
[PROOF STEP]
by (induct t a rule: tree_induct_consistent) simp+


[STATEMENT]
lemma sortedByWeight_Cons_imp_sortedByWeight:
"sortedByWeight (t # ts) \<Longrightarrow> sortedByWeight ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sortedByWeight (t # ts) \<Longrightarrow> sortedByWeight ts
[PROOF STEP]
by (case_tac ts) simp+


[STATEMENT]
lemma sortedByWeight_Cons_imp_forall_weight_ge:
"sortedByWeight (t # ts) \<Longrightarrow> \<forall>u \<in> set ts. weight u \<ge> weight t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sortedByWeight (t # ts) \<Longrightarrow> \<forall>u\<in>set ts. weight t \<le> weight u
[PROOF STEP]
by (induct ts arbitrary: t) force+


[STATEMENT]
lemma sortedByWeight_insortTree:
"\<lbrakk>sortedByWeight ts; height t = 0; height\<^sub>F ts = 0\<rbrakk> \<Longrightarrow>
 sortedByWeight (insortTree t ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sortedByWeight ts; height t = 0; height\<^sub>F ts = 0\<rbrakk> \<Longrightarrow> sortedByWeight (insortTree t ts)
[PROOF STEP]
by (induct ts rule: sortedByWeight.induct) auto


[STATEMENT]
lemma cost_swapFourSyms_le:
assumes
  "consistent t" "minima t a b" "c \<in> alphabet t" "d \<in> alphabet t"
  "depth t c = height t" "depth t d = height t" "c \<noteq> d"
shows "cost (swapFourSyms t a b c d) \<le> cost t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
note lems = swapFourSyms_def minima_def cost_swapSyms_le depth_le_height
[PROOF STATE]
proof (state)
this:
swapFourSyms ?t ?a ?b ?c ?d = (if ?a = ?d then swapSyms ?t ?b ?c else if ?b = ?c then swapSyms ?t ?a ?d else swapSyms (swapSyms ?t ?a ?c) ?b ?d)
minima ?t ?a ?b = (?a \<in> alphabet ?t \<and> ?b \<in> alphabet ?t \<and> ?a \<noteq> ?b \<and> (\<forall>c\<in>alphabet ?t. c \<noteq> ?a \<longrightarrow> c \<noteq> ?b \<longrightarrow> freq ?t ?a \<le> freq ?t c \<and> freq ?t ?b \<le> freq ?t c))
\<lbrakk>consistent ?t; ?a \<in> alphabet ?t; ?b \<in> alphabet ?t; freq ?t ?a \<le> freq ?t ?b; depth ?t ?a \<le> depth ?t ?b\<rbrakk> \<Longrightarrow> cost (swapSyms ?t ?a ?b) \<le> cost ?t
depth ?t ?a \<le> height ?t

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
proof (cases "a \<noteq> d \<and> b \<noteq> c")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<noteq> d \<and> b \<noteq> c \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
 2. \<not> (a \<noteq> d \<and> b \<noteq> c) \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<noteq> d \<and> b \<noteq> c

goal (2 subgoals):
 1. a \<noteq> d \<and> b \<noteq> c \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
 2. \<not> (a \<noteq> d \<and> b \<noteq> c) \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
 2. \<not> ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
assume "a = c"
[PROOF STATE]
proof (state)
this:
a = c

goal (2 subgoals):
 1. ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
 2. \<not> ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
 2. \<not> ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
assume "b = d"
[PROOF STATE]
proof (state)
this:
b = d

goal (2 subgoals):
 1. ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
 2. \<not> ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b = d

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
using \<open>a = c\<close> True assms
[PROOF STATE]
proof (prove)
using this:
b = d
a = c
a \<noteq> d \<and> b \<noteq> c
consistent t
minima t a b
c \<in> alphabet t
d \<in> alphabet t
depth t c = height t
depth t d = height t
c \<noteq> d

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
by (simp add: lems)
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
assume "b \<noteq> d"
[PROOF STATE]
proof (state)
this:
b \<noteq> d

goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<noteq> d

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
using \<open>a = c\<close> True assms
[PROOF STATE]
proof (prove)
using this:
b \<noteq> d
a = c
a \<noteq> d \<and> b \<noteq> c
consistent t
minima t a b
c \<in> alphabet t
d \<in> alphabet t
depth t c = height t
depth t d = height t
c \<noteq> d

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
by (simp add: lems)
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal (1 subgoal):
 1. a \<noteq> c \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> c \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
assume "a \<noteq> c"
[PROOF STATE]
proof (state)
this:
a \<noteq> c

goal (1 subgoal):
 1. a \<noteq> c \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
 2. \<not> ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
assume "b = d"
[PROOF STATE]
proof (state)
this:
b = d

goal (2 subgoals):
 1. ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
 2. \<not> ?P \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b = d

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
using \<open>a \<noteq> c\<close> True assms
[PROOF STATE]
proof (prove)
using this:
b = d
a \<noteq> c
a \<noteq> d \<and> b \<noteq> c
consistent t
minima t a b
c \<in> alphabet t
d \<in> alphabet t
depth t c = height t
depth t d = height t
c \<noteq> d

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
by (simp add: lems)
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
assume "b \<noteq> d"
[PROOF STATE]
proof (state)
this:
b \<noteq> d

goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
have "cost (swapFourSyms t a b c d) \<le> cost (swapSyms t a c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost (swapSyms t a c)
[PROOF STEP]
using \<open>b \<noteq> d\<close> \<open>a \<noteq> c\<close> True assms
[PROOF STATE]
proof (prove)
using this:
b \<noteq> d
a \<noteq> c
a \<noteq> d \<and> b \<noteq> c
consistent t
minima t a b
c \<in> alphabet t
d \<in> alphabet t
depth t c = height t
depth t d = height t
c \<noteq> d

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost (swapSyms t a c)
[PROOF STEP]
by (clarsimp simp: lems)
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost (swapSyms t a c)

goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost (swapSyms t a c)

goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
have "\<dots> \<le> cost t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapSyms t a c) \<le> cost t
[PROOF STEP]
using \<open>b \<noteq> d\<close> \<open>a \<noteq> c\<close> True assms
[PROOF STATE]
proof (prove)
using this:
b \<noteq> d
a \<noteq> c
a \<noteq> d \<and> b \<noteq> c
consistent t
minima t a b
c \<in> alphabet t
d \<in> alphabet t
depth t c = height t
depth t d = height t
c \<noteq> d

goal (1 subgoal):
 1. cost (swapSyms t a c) \<le> cost t
[PROOF STEP]
by (clarsimp simp: lems)
[PROOF STATE]
proof (state)
this:
cost (swapSyms t a c) \<le> cost t

goal (1 subgoal):
 1. b \<noteq> d \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cost (swapFourSyms t a b c d) \<le> cost t

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal (1 subgoal):
 1. \<not> (a \<noteq> d \<and> b \<noteq> c) \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (a \<noteq> d \<and> b \<noteq> c) \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (a \<noteq> d \<and> b \<noteq> c)

goal (1 subgoal):
 1. \<not> (a \<noteq> d \<and> b \<noteq> c) \<Longrightarrow> cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (a \<noteq> d \<and> b \<noteq> c)

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> (a \<noteq> d \<and> b \<noteq> c)
consistent t
minima t a b
c \<in> alphabet t
d \<in> alphabet t
depth t c = height t
depth t d = height t
c \<noteq> d

goal (1 subgoal):
 1. cost (swapFourSyms t a b c d) \<le> cost t
[PROOF STEP]
by (clarsimp simp: lems)
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms t a b c d) \<le> cost t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_freq_le_imp_minima:
"\<lbrakk>\<forall>c \<in> alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c;
  alphabet u = alphabet t \<union> {b}; a \<in> alphabet u; a \<noteq> b;
  freq u = (\<lambda>c. if c = a then w\<^sub>a else if c = b then w\<^sub>b else freq t c)\<rbrakk> \<Longrightarrow>
 minima u a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c; alphabet u = alphabet t \<union> {b}; a \<in> alphabet u; a \<noteq> b; freq u = (\<lambda>c. if c = a then w\<^sub>a else if c = b then w\<^sub>b else freq t c)\<rbrakk> \<Longrightarrow> minima u a b
[PROOF STEP]
by (simp add: minima_def)