| changeset 66302 | fd89f97c80c2 |
| parent 61679 | 1335462046e8 |
| child 70273 | acc1749c2be9 |
--- a/src/HOL/Data_Structures/Tree23.thy Tue Aug 01 07:26:23 2017 +0200 +++ b/src/HOL/Data_Structures/Tree23.thy Tue Aug 01 10:28:42 2017 +0200 @@ -40,4 +40,7 @@ "bal (Node3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" +lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1" +by (induction t) auto + end