Mercurial > hg > Gears > GearsAgda
changeset 885:ecf594d7b731
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 May 2024 11:59:56 +0900 |
| parents | cff51057ddd8 |
| children | 0aac292a5e1c |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 13 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Fri May 10 19:06:34 2024 +0900 +++ b/hoareBinaryTree1.agda Sat May 11 11:59:56 2024 +0900 @@ -1336,7 +1336,19 @@ rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫ RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) .leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-single .kp .(⟪ Red , vp ⟫))) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 ⟪ <-trans x lt1 , ⟪ >-tr< x₂ lt1 , >-tr< x₃ lt1 ⟫ ⟫ tt tt tt (t-left _ _ x x₂ x₃ ti) (t-single _ _) RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf .(node key₂ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) .leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-right .kp key₂ x₆ x₇ x₈ ti₁)) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 ⟪ <-trans x lt1 , ⟪ >-tr< x₂ lt1 , >-tr< x₃ lt1 ⟫ ⟫ tt tt ⟪ <-trans lt2 x₆ , ⟪ <-tr> x₇ lt2 , <-tr> x₈ lt2 ⟫ ⟫ (t-left _ _ x x₂ x₃ ti) (t-right _ _ x₆ x₇ x₈ ti₁) -RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-left key₂ .kp x₆ x₇ x₈ ti₁)) (rbr-rotate-rl t₂ .leaf kg kp kn lt1 lt2 trb) = ? +RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-left key₂ .kp x₆ x₇ x₈ ti₁)) (rbr-rotate-rl t₂ .leaf kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₁ trb +... | t-single .kn .(⟪ Red , vn ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ? ? ? ? (t-left _ _ ? ? ? ?) (t-single _ _) where + rr00 : (kg < kn) ∧ ⊤ ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ? + rr01 : (kn < kp) ∧ ⊤ ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ? +... | t-left key₃ .kn {v1} {v3} {t₇} {t₃} x₉ x₁₀ x₁₁ ti₀ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt tt (t-node _ _ _ ? ? ? ? ? ? ti ti₀) (t-single _ _) where + rr00 : (kg < kn) ∧ ((kg < key₃) ∧ tr> kg t₇ ∧ tr> kg t₃) ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₃ < kp) ∧ tr< kp t₇ ∧ tr< kp t₃) ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ + rr03 = proj1 (proj2 rr01) RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-node key₂ .kp key₃ x₆ x₇ x₈ x₉ x₁₀ x₁₁ ti₁ ti₂)) (rbr-rotate-rl t₂ .leaf kg kp kn lt1 lt2 trb) = ? RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ t₅)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl t₂ .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ? RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ t₅)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl t₂ .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?