[STATEMENT]
lemma invc2_joinR:
  "\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow>
  invc2 (joinR l x r)
  \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invc l; invh l; invc r; invh r; bheight r \<le> bheight l\<rbrakk> \<Longrightarrow> invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))
[PROOF STEP]
proof (induct l x 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; invc x23; invh x23; invc r; invh r; bheight r \<le> bheight x23\<rbrakk> \<Longrightarrow> invc2 (joinR x23 x r) \<and> (bheight x23 \<noteq> bheight r \<and> color x23 = Black \<longrightarrow> invc (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; invc x23; invh x23; invc r; invh r; bheight r \<le> bheight x23\<rbrakk> \<Longrightarrow> invc2 (joinR x23 x r) \<and> (bheight x23 \<noteq> bheight r \<and> color x23 = Black \<longrightarrow> invc (joinR x23 x r)); invc l; invh l; invc r; invh r; bheight r \<le> bheight l\<rbrakk> \<Longrightarrow> invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))
[PROOF STEP]
case (1 l x 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; invc ?x23.0; invh ?x23.0; invc r; invh r; bheight r \<le> bheight ?x23.0\<rbrakk> \<Longrightarrow> invc2 (joinR ?x23.0 x r) \<and> (bheight ?x23.0 \<noteq> bheight r \<and> color ?x23.0 = Black \<longrightarrow> invc (joinR ?x23.0 x r))
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Black; invc ?x23.0; invh ?x23.0; invc r; invh r; bheight r \<le> bheight ?x23.0\<rbrakk> \<Longrightarrow> invc2 (joinR ?x23.0 x r) \<and> (bheight ?x23.0 \<noteq> bheight r \<and> color ?x23.0 = Black \<longrightarrow> invc (joinR ?x23.0 x r))
invc l
invh l
invc r
invh r
bheight r \<le> bheight l

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; invc x23; invh x23; invc r; invh r; bheight r \<le> bheight x23\<rbrakk> \<Longrightarrow> invc2 (joinR x23 x r) \<and> (bheight x23 \<noteq> bheight r \<and> color x23 = Black \<longrightarrow> invc (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; invc x23; invh x23; invc r; invh r; bheight r \<le> bheight x23\<rbrakk> \<Longrightarrow> invc2 (joinR x23 x r) \<and> (bheight x23 \<noteq> bheight r \<and> color x23 = Black \<longrightarrow> invc (joinR x23 x r)); invc l; invh l; invc r; invh r; bheight r \<le> bheight l\<rbrakk> \<Longrightarrow> invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (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; invc ?x23.0; invh ?x23.0; invc r; invh r; bheight r \<le> bheight ?x23.0\<rbrakk> \<Longrightarrow> invc2 (joinR ?x23.0 x r) \<and> (bheight ?x23.0 \<noteq> bheight r \<and> color ?x23.0 = Black \<longrightarrow> invc (joinR ?x23.0 x r))
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Black; invc ?x23.0; invh ?x23.0; invc r; invh r; bheight r \<le> bheight ?x23.0\<rbrakk> \<Longrightarrow> invc2 (joinR ?x23.0 x r) \<and> (bheight ?x23.0 \<noteq> bheight r \<and> color ?x23.0 = Black \<longrightarrow> invc (joinR ?x23.0 x r))
invc l
invh l
invc r
invh r
bheight r \<le> bheight l

goal (1 subgoal):
 1. invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))
[PROOF STEP]
by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
[PROOF STATE]
proof (state)
this:
invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))

goal:
No subgoals!
[PROOF STEP]
qed