equal
deleted
inserted
replaced
30 |
30 |
31 instance .. |
31 instance .. |
32 |
32 |
33 end |
33 end |
34 |
34 |
35 text \<open>Balanced:\<close> |
35 text \<open>Completeness:\<close> |
36 |
36 |
37 fun complete :: "'a tree23 \<Rightarrow> bool" where |
37 fun complete :: "'a tree23 \<Rightarrow> bool" where |
38 "complete Leaf = True" | |
38 "complete Leaf = True" | |
39 "complete (Node2 l _ r) = (complete l & complete r & height l = height r)" | |
39 "complete (Node2 l _ r) = (complete l & complete r & height l = height r)" | |
40 "complete (Node3 l _ m _ r) = |
40 "complete (Node3 l _ m _ r) = |