Mercurial > hg > Members > Moririn
changeset 626:6465673df5bc
connected
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Nov 2021 22:45:19 +0900 |
| parents | 074fb29ebf57 |
| children | 967547859521 |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 7 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Mon Nov 08 22:30:40 2021 +0900 +++ b/hoareBinaryTree.agda Mon Nov 08 22:45:19 2021 +0900 @@ -252,6 +252,11 @@ ⟪ tree1 , [] ⟫ {!!} $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value {!!} where - lemma3 : ? - lemma3 = ? + lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } → + replacedTree key value1 tree t1 → stackInvariant t1 tree s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → node-key t1 ≡ just key + lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case1 ()) + lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case2 x) = x + lemma7 {.key₁} {value1} {.(node key₁ value1 s1 s2)} {node key₁ value s1 s2} r-node s or = {!!} + lemma7 {key} {value1} {.(node key₁ value s1 _)} {node key₁ value s1 s2} (r-right x r) s or = {!!} + lemma7 {key} {value1} {.(node key₁ value _ s2)} {node key₁ value s1 s2} (r-left x r) s or = {!!}