Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 753:7127770c2176

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 Fri, 28 Apr 2023 14:13:39 +0900
parents 44837beece64
children cda422725f79
comparison
equal deleted inserted replaced
752:44837beece64 753:7127770c2176
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 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 ? ? ? ? ? ? ? ? ? ? 709 ... | tri< a ¬b ¬c = next ? ? ? ? ? ? ? ? ? ?
710 ... | tri≈ ¬a b ¬c = ? -- can't happen 710 ... | tri≈ ¬a b ¬c = ? -- can't happen
711 ... | tri> ¬a ¬b c = next ? ? ? ? ? ? ? ? ? ? 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 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 713 insertCase3 (node kp value₁ tpl tpr) (node kg value (node ku ⟪ Black , vu ⟫ tgl tgr) tr₁) tp=p tg=g with <-cmp ku kp
714 ... | tri< a ¬b ¬c = ? 714 ... | tri< a ¬b ¬c = ? where
715 insertCase4 : ( right-tp left-tg : bt (Color ∧ A) ) → right-tp ≡ tpr → left-tg ≡ tgl → t
716 insertCase4 leaf lg eq1 eq2 = ?
717 insertCase4 (node krp value rp rp₁) leaf eq1 eq2 = ?
718 insertCase4 (node krp value rp rp₁) (node klg value₁ lg lg₁) eq1 eq2 with <-cmp key krp | <-cmp kp klg
719 ... | ttt4 | ttt5 = ? where
720 insertCase41 : ( left-tp right-tg : bt (Color ∧ A) ) → left-tp ≡ tpl → right-tg ≡ tgr → t
721 insertCase41 leaf rg eq3 eq4 = ?
722 insertCase41 (node klp value lp lp₁) leaf eq3 eq4 = ?
723 insertCase41 (node klp value lp lp₁) (node krg value₁ rg rg₁) eq3 eq4 with <-cmp key klp | <-cmp kp krg
724 ... | ttt4 | ttt5 = ? where
715 ... | tri≈ ¬a b ¬c = ? -- can't happen 725 ... | tri≈ ¬a b ¬c = ? -- can't happen
716 ... | tri> ¬a ¬b c = ? 726 ... | tri> ¬a ¬b c = ?
717 insertCase1 : t 727 insertCase1 : t
718 insertCase1 with stackToPG tree orig stack si 728 insertCase1 with stackToPG tree orig stack si
719 ... | case1 eq = ? 729 ... | case1 eq = ?