Mercurial > hg > Gears > GearsAgda
comparison hoareBinaryTree.agda @ 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 |
comparison
equal
deleted
inserted
replaced
| 625:074fb29ebf57 | 626:6465673df5bc |
|---|---|
| 250 TerminatingLoopS (bt A ∧ List (bt A) ) | 250 TerminatingLoopS (bt A ∧ List (bt A) ) |
| 251 {λ p → findPR (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p)) | 251 {λ p → findPR (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p)) |
| 252 ⟪ tree1 , [] ⟫ {!!} | 252 ⟪ tree1 , [] ⟫ {!!} |
| 253 $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) | 253 $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) |
| 254 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value {!!} where | 254 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value {!!} where |
| 255 lemma3 : ? | 255 lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } → |
| 256 lemma3 = ? | 256 replacedTree key value1 tree t1 → stackInvariant t1 tree s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → node-key t1 ≡ just key |
| 257 | 257 lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case1 ()) |
| 258 lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case2 x) = x | |
| 259 lemma7 {.key₁} {value1} {.(node key₁ value1 s1 s2)} {node key₁ value s1 s2} r-node s or = {!!} | |
| 260 lemma7 {key} {value1} {.(node key₁ value s1 _)} {node key₁ value s1 s2} (r-right x r) s or = {!!} | |
| 261 lemma7 {key} {value1} {.(node key₁ value _ s2)} {node key₁ value s1 s2} (r-left x r) s or = {!!} | |
| 262 |