equal
deleted
inserted
replaced
85 qed |
85 qed |
86 |
86 |
87 lemma inorder2_leaves: "inorder2(leaves as) = as" |
87 lemma inorder2_leaves: "inorder2(leaves as) = as" |
88 by(induction as) auto |
88 by(induction as) auto |
89 |
89 |
90 lemma "inorder(tree23_of_list as) = as" |
90 lemma inorder: "inorder(tree23_of_list as) = as" |
91 by(simp add: tree23_of_list_def inorder_join_all inorder2_leaves) |
91 by(simp add: tree23_of_list_def inorder_join_all inorder2_leaves) |
92 |
92 |
93 subsubsection \<open>Completeness:\<close> |
93 subsubsection \<open>Completeness:\<close> |
94 |
94 |
95 lemma complete_join_adj: |
95 lemma complete_join_adj: |