Mercurial > hg > Members > Moririn
changeset 741:c44edea35126
..
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 23 Apr 2023 17:47:27 +0900 |
| parents | 9ff79715588e |
| children | 0e0a30f942ca |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 6 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sun Apr 23 14:29:09 2023 +0900 +++ b/hoareBinaryTree1.agda Sun Apr 23 17:47:27 2023 +0900 @@ -632,8 +632,12 @@ → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A stack stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right x s-nil) = case2 (case1 refl) -stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ grand ∷ rest) (s-right {t0} {t1} {t2} {k1} {v1} x (s-right {t3} {t4} {t5} {k2} {v2} x₁ si)) = case2 (case2 - record { self = tree ; parent = node k1 v1 t2 tree ; grand = grand ; pg = s2-1s2p refl ? ; rest = rest ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right {.tree} {.(node k2 v2 t5 (node k1 v1 t2 tree))} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.(node k2 v2 t5 (node k1 v1 t2 tree))} {t5} {k2} {v2} x₁ s-nil)) = case2 (case2 + record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right {.tree} {.orig} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.orig} {t5} {k2} {v2} x₁ (s-right x₂ si))) = case2 (case2 + record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right {.tree} {.orig} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.orig} {t5} {k2} {v2} x₁ (s-left x₂ si))) = case2 (case2 + record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node _ _ _ tree ∷ _) (s-right x (s-left x₁ si)) = ? stackToPG {n} {A} {key} tree orig .(tree ∷ _) (s-left x si) = ?