[STATEMENT]
lemma bst_joinR:
  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>y\<in>set_tree r. a < y \<rbrakk>
  \<Longrightarrow> bst (joinR l a r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Tree2.bst l; Tree2.bst r; \<forall>x\<in>Tree2.set_tree l. x < a; \<forall>y\<in>Tree2.set_tree r. a < y\<rbrakk> \<Longrightarrow> Tree2.bst (joinR l a r)
[PROOF STEP]
proof(induction l a r rule: joinR.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l x r. \<lbrakk>\<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Red; Tree2.bst x23; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree x23. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR x23 x r); \<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Black; Tree2.bst x23; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree x23. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR x23 x r); Tree2.bst l; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree l. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR l x r)
[PROOF STEP]
case (1 l a r)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Red; Tree2.bst ?x23.0; Tree2.bst r; \<forall>x\<in>Tree2.set_tree ?x23.0. x < a; \<forall>a\<in>Tree2.set_tree r. a < a\<rbrakk> \<Longrightarrow> Tree2.bst (joinR ?x23.0 a r)
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Black; Tree2.bst ?x23.0; Tree2.bst r; \<forall>x\<in>Tree2.set_tree ?x23.0. x < a; \<forall>a\<in>Tree2.set_tree r. a < a\<rbrakk> \<Longrightarrow> Tree2.bst (joinR ?x23.0 a r)
Tree2.bst l
Tree2.bst r
\<forall>x\<in>Tree2.set_tree l. x < a
\<forall>a\<in>Tree2.set_tree r. a < a

goal (1 subgoal):
 1. \<And>l x r. \<lbrakk>\<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Red; Tree2.bst x23; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree x23. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR x23 x r); \<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Black; Tree2.bst x23; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree x23. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR x23 x r); Tree2.bst l; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree l. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR l x r)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Red; Tree2.bst ?x23.0; Tree2.bst r; \<forall>x\<in>Tree2.set_tree ?x23.0. x < a; \<forall>a\<in>Tree2.set_tree r. a < a\<rbrakk> \<Longrightarrow> Tree2.bst (joinR ?x23.0 a r)
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Black; Tree2.bst ?x23.0; Tree2.bst r; \<forall>x\<in>Tree2.set_tree ?x23.0. x < a; \<forall>a\<in>Tree2.set_tree r. a < a\<rbrakk> \<Longrightarrow> Tree2.bst (joinR ?x23.0 a r)
Tree2.bst l
Tree2.bst r
\<forall>x\<in>Tree2.set_tree l. x < a
\<forall>a\<in>Tree2.set_tree r. a < a

goal (1 subgoal):
 1. Tree2.bst (joinR l a r)
[PROOF STEP]
by(auto simp: set_baliR joinR.simps[of l a r] set_joinR ball_Un intro!: bst_baliR
        split!: tree.splits color.splits)
[PROOF STATE]
proof (state)
this:
Tree2.bst (joinR l a r)

goal:
No subgoals!
[PROOF STEP]
qed