Mercurial > hg > Gears > GearsAgda
changeset 778:4d71d0894cfa
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 May 2023 19:06:08 +0900 |
| parents | 8e5159a02b76 |
| children | 7e5dfe642064 0b791ae19543 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 10 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Tue May 16 17:58:04 2023 +0900 +++ b/hoareBinaryTree1.agda Mon May 22 19:06:08 2023 +0900 @@ -731,12 +731,19 @@ → RBtreeInvariant tree ds ∧ RBtreeInvariant (PG.parent pg) dp ∧ RBtreeInvariant (PG.grand pg) dg PGtoRBinvariant = {!!} -findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree0 : bt (Color ∧ A) ) +findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) + → (stack : List (bt (Color ∧ A))) + → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack → {d : ℕ} → RBtreeInvariant tree0 d - → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) + → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → {d1 : ℕ} → RBtreeInvariant tree1 d1 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t -findRBT = {!!} +findRBT {_} {_} {A} {t} key tree0 leaf stack ti {d} rb0 exit = ? +findRBT {_} {_} {A} {t} key tree0 (node key₁ value left right) stack ti {d} rb0 exit with <-cmp key key₁ +... | tri< a ¬b ¬c = ? +... | tri≈ ¬a b ¬c = ? +... | tri> ¬a ¬b c = ? rotateLeft : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A)