Mercurial > hg > Gears > GearsAgda
changeset 820:317539bdba03
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Jan 2024 20:37:25 +0900 |
| parents | 66726208b9f4 |
| children | aeb14a056896 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 13 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Thu Jan 25 17:03:59 2024 +0900 +++ b/hoareBinaryTree1.agda Thu Jan 25 20:37:25 2024 +0900 @@ -932,8 +932,19 @@ -- node-key parent < node-key repl < node-key grand → rotateLeft parent then insertCase6 -- node-key grand < node-key repl < node-key parent → rotateRight parent then insertCase6 -- else insertCase6 - insertCase51 : t - insertCase51 = ? + insertCase51 : (tree1 grand : bt (Color ∧ A)) → tree1 ≡ tree → grand ≡ PG.grand pg → t + insertCase51 leaf grand teq geq = ? -- can't happen + insertCase51 (node key value tree1 tree2) leaf teq geq = ? -- can't happen + insertCase51 (node key value tree1 tree2) (node key₁ value₁ grand grand₁) teq geq with <-cmp key key₁ + ... | tri< a ¬b ¬c = ? where + insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t + insertCase511 leaf peq = ? -- can't happen + insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂ + ... | tri< a ¬b ¬c = insertCase6 key value orig ? stack ? pg ? ? + ... | tri≈ ¬a b ¬c = ? -- can't happen + ... | tri> ¬a ¬b c = ? --- rotareRight → insertCase6 key value orig ? stack ? pg next exit + ... | tri≈ ¬a b ¬c = ? -- can't happen + ... | tri> ¬a ¬b c = ?