Mercurial > hg > Members > Moririn
changeset 641:14244de916f2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 16 Nov 2021 12:13:47 +0900 |
| parents | e0bea7a2bb4d |
| children | 6e319e44271b |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 5 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Tue Nov 16 11:08:59 2021 +0900 +++ b/hoareBinaryTree.agda Tue Nov 16 12:13:47 2021 +0900 @@ -153,10 +153,11 @@ stackTreeInvariant : {n : Level} {A : Set n} (repl tree : bt A) → (stack : List (bt A)) → treeInvariant tree → stackInvariant repl tree stack → treeInvariant repl -stackTreeInvariant repl .repl (.repl ∷ .[]) ti (s-single .repl) = ti -stackTreeInvariant repl leaf (.repl ∷ st) ti (s-right si) = {!!} -stackTreeInvariant repl (node key value tree tree₁) (.repl ∷ st) ti (s-right si) = {!!} -stackTreeInvariant repl tree (.repl ∷ st) ti (s-left si) = {!!} +stackTreeInvariant repl .repl .(repl ∷ []) ti (s-single .repl) = ti +stackTreeInvariant {_} {A} repl tree (.repl ∷ st) ti (s-right si) = si1 si where + si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant (node key₁ v1 tree₁ repl) tree st → treeInvariant repl + si1 si = ? +stackTreeInvariant repl tree .(repl ∷ _) ti (s-left si) = {!!} rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf ) rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()