Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Data_Structures/Tree23.thy
changeset 72586 e3ba2578ad9d
parent 72566 831f17da1aab 
--- a/src/HOL/Data_Structures/Tree23.thy	Thu Oct 22 15:18:08 2020 +0200
+++ b/src/HOL/Data_Structures/Tree23.thy	Thu Nov 12 12:44:17 2020 +0100
@@ -36,9 +36,9 @@
 
 fun complete :: "'a tree23 \<Rightarrow> bool" where
 "complete Leaf = True" |
-"complete (Node2 l _ r) = (complete l & complete r & height l = height r)" |
+"complete (Node2 l _ r) = (height l = height r \<and> complete l & complete r)" |
 "complete (Node3 l _ m _ r) =
-  (complete l & complete m & complete r & height l = height m & height m = height r)"
+  (height l = height m & height m = height r & complete l & complete m & complete r)"
 
 lemma ht_sz_if_complete: "complete t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
 by (induction t) auto
isabelle