tuned
authornipkow
Fri, 27 Dec 2019 10:54:15 +0100
changeset 71555 7a0a6c56015e
parent 71554 a956b769903e
child 71556 3c4c171344f4
tuned
src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Dec 24 21:50:02 2019 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Dec 27 10:54:15 2019 +0100
@@ -291,7 +291,7 @@
 by (cases c) auto
 
 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
-  height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
+  height t \<le> 2 * bheight t + (if color t = Black then 0 else 1)"
 by(induction t) (auto split: if_split_asm)
 
 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "