Mercurial > hg > Gears > GearsAgda
changeset 856:9964cec86483
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 31 Mar 2024 16:35:19 +0900 |
| parents | 189ab9e59035 |
| children | 022481623aea |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 5 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sun Mar 31 15:36:15 2024 +0900 +++ b/hoareBinaryTree1.agda Sun Mar 31 16:35:19 2024 +0900 @@ -1087,9 +1087,11 @@ rr00 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₂ lt) x₆ rr02 : treeInvariant (node key₃ ⟪ Red , c3 ⟫ t₂ t₄) rr02 = RB-repl→ti _ _ _ _ ti₁ (rbr-right lt trb) -RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ t t₁) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ t₁ leaf)) key value - (t-left _ _ x₁ x₂ x₃ ti) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt (RB-repl→ti _ _ _ _ (treeLeftDown _ _ ti) trb) (rr03 t₁ refl ti) where - rr03 : (tr : bt (Color ∧ A)) → tr ≡ t₁ → (tir : treeInvariant (node k2 ⟪ Red , c2 ⟫ t tr)) → treeInvariant (node k1 ⟪ Red , c1 ⟫ tr leaf) +RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-single .k2 .(⟪ Red , c2 ⟫))) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt (RB-repl→ti _ _ _ _ ? trb) ? +RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .(node key₂ _ _ _)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .(node key₂ _ _ _) leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-right .k2 key₂ x₄ x₅ x₆ ti)) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt ? ? +RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .(node key₂ _ _ _) .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-left key₂ .k2 x₄ x₅ x₆ ti)) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt (RB-repl→ti _ _ _ _ ? trb) ? +RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .(node key₃ _ _ _) leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-node key₂ .k2 key₃ x₄ x₅ x₆ x₇ x₈ x₉ ti ti₁)) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt ? ? where + rr03 : (tr : bt (Color ∧ A)) → tr ≡ ? → (tir : treeInvariant (node k2 ⟪ Red , c2 ⟫ ? tr)) → treeInvariant (node k1 ⟪ Red , c1 ⟫ tr leaf) rr03 leaf eq tri = RTtoTI0 _ _ _ _ (treeRightDown _ _ tri) r-leaf rr03 (node key₃ value₃ tr tr₁) refl tri = RTtoTI0 _ _ _ _ (t-left _ _ (proj1 x₃) (proj1 (proj2 x₃)) (proj2 (proj2 x₃)) (treeRightDown _ _ tri) ) (r-left (proj1 x₃) r-node)