Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 752:44837beece64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Apr 2023 13:12:31 +0900
parents 4ecad6cfef4b
children 7127770c2176
comparison
equal deleted inserted replaced
751:4ecad6cfef4b 752:44837beece64
696 ... | Black = ? -- tree stuctre is preserved 696 ... | Black = ? -- tree stuctre is preserved
697 ... | Red = ? where -- insertCase3 grand refl where 697 ... | Red = ? where -- insertCase3 grand refl where
698 -- 698 --
699 -- in some case, stack is poped and loop to replaceRBP 699 -- in some case, stack is poped and loop to replaceRBP
700 -- it means, we have to create replacedTree 700 -- it means, we have to create replacedTree
701 -- g
702 -- u p
703 -- _ s
701 insertCase3 : ( tp tg : bt (Color ∧ A) ) → tp ≡ parent → tg ≡ grand → t 704 insertCase3 : ( tp tg : bt (Color ∧ A) ) → tp ≡ parent → tg ≡ grand → t
702 insertCase3 tp leaf eq = ? 705 insertCase3 tp leaf tp=p tg=g = ?
703 insertCase3 tp (node kg value leaf tr₁) eq = ? 706 insertCase3 tp (node kg value leaf tr₁) tp=p tg=g = ?
704 insertCase3 tp (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku 707 insertCase3 leaf (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) tp=p tg=g = ? -- can't happen
708 insertCase3 (node kp value₁ tp tp₁) (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) tp=p tg=g with <-cmp ku kp
709 ... | tri< a ¬b ¬c = next ? ? ? ? ? ? ? ? ? ?
710 ... | tri≈ ¬a b ¬c = ? -- can't happen
711 ... | tri> ¬a ¬b c = next ? ? ? ? ? ? ? ? ? ?
712 insertCase3 leaf (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) tp=p tg=g = ? -- can't happen
713 insertCase3 (node kp value₁ tp tp₁) (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) tp=p tg=g with <-cmp ku kp
705 ... | tri< a ¬b ¬c = ? 714 ... | tri< a ¬b ¬c = ?
706 ... | tri≈ ¬a b ¬c = ? 715 ... | tri≈ ¬a b ¬c = ? -- can't happen
707 ... | tri> ¬a ¬b c = ?
708 insertCase3 tp (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
709 ... | tri< a ¬b ¬c = ?
710 ... | tri≈ ¬a b ¬c = ?
711 ... | tri> ¬a ¬b c = ? 716 ... | tri> ¬a ¬b c = ?
712 insertCase1 : t 717 insertCase1 : t
713 insertCase1 with stackToPG tree orig stack si 718 insertCase1 with stackToPG tree orig stack si
714 ... | case1 eq = ? 719 ... | case1 eq = ?
715 ... | case2 (case1 eq ) = ? 720 ... | case2 (case1 eq ) = ?