fun inorder :: "'a tree23 \ 'a list" where "inorder Leaf = []" | "inorder(Node2 l a r) = inorder l @ a # inorder r" | "inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r"
instantiation tree23 :: (type)height begin
fun height_tree23 :: "'a tree23 \ nat" where "height Leaf = 0" | "height (Node2 l _ r) = Suc(max (height l) (height r))" | "height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
instance ..
end
text\<open>Completeness:\<close>
fun complete :: "'a tree23 \ bool" where "complete Leaf = True" | "complete (Node2 l _ r) = (height l = height r \ complete l & complete r)" | "complete (Node3 l _ m _ r) =
(height l = height m & height m = height r & complete l & complete m & complete r)"
lemma ht_sz_if_complete: "complete t \ 2 ^ height t \ size t + 1" by (induction t) auto
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
