equal
deleted
inserted
replaced
38 "bal Leaf = True" | |
38 "bal Leaf = True" | |
39 "bal (Node2 l _ r) = (bal l & bal r & height l = height r)" | |
39 "bal (Node2 l _ r) = (bal l & bal r & height l = height r)" | |
40 "bal (Node3 l _ m _ r) = |
40 "bal (Node3 l _ m _ r) = |
41 (bal l & bal m & bal r & height l = height m & height m = height r)" |
41 (bal l & bal m & bal r & height l = height m & height m = height r)" |
42 |
42 |
|
43 lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1" |
|
44 by (induction t) auto |
|
45 |
43 end |
46 end |