Mercurial > hg > Gears > GearsAgda
changeset 881:749e59e3c569
... case5 half done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 04 May 2024 15:30:11 +0900 |
| parents | 3b030eb540d9 |
| children | 9f62da6d787c |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 3 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sat May 04 12:31:47 2024 +0900 +++ b/hoareBinaryTree1.agda Sat May 04 15:30:11 2024 +0900 @@ -1303,13 +1303,15 @@ rr01 : (kn < kg) ∧ ((key₄ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ⊤ rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ rr03 = proj1 (proj2 rr01) -... | t-node key₄ .kn key₅ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀}x₁₂ x₁₃ x₁₄ x₁₅ x₁₆ x₁₇ t t₃ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ? ? ? ? (t-node _ _ _ ? ? ? ? ? ? ti t ) (t-node _ _ _ ? ? ? ? ? ? (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₂ trb)) ti₁ ) where +... | t-node key₄ .kn key₅ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀}x₁₂ x₁₃ x₁₄ x₁₅ x₁₆ x₁₇ t t₃ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₄ , x₁₅ ⟫ ⟫ ⟪ x₁₃ , ⟪ x₁₆ , x₁₇ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x₆ (proj1 rr02) x₈ x₉ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti t ) (t-node _ _ _ (proj1 rr04) x₁ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₄ x₅ (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₂ trb)) ti₁ ) where rr00 : (kp < kn) ∧ ((kp < key₄) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ((kp < key₅) ∧ tr> kp t₉ ∧ tr> kp t₁₀) rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ rr02 = proj1 (proj2 rr00) + rr05 = proj2 (proj2 rr00) rr01 : (kn < kg) ∧ ((key₄ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ((key₅ < kg) ∧ tr< kg t₉ ∧ tr< kg t₁₀) rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ rr03 = proj1 (proj2 rr01) + rr04 = proj2 (proj2 rr01) RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value ti (rbr-rotate-rl t₂ leaf kg kp kn lt1 lt2 trb) = ? RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value ti (rbr-rotate-rl t₂ (node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?