Mercurial > hg > Gears > GearsAgda

changeset 879:32e026c5f31f

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 Sat, 04 May 2024 00:44:56 +0900
parents feeb6982fd46
children 3b030eb540d9
files hoareBinaryTree1.agda
diffstat 1 files changed, 32 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri May 03 18:19:33 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat May 04 00:44:56 2024 +0900
@@ -1256,8 +1256,38 @@
         rr03 = proj2 (proj2 rr01)
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf leaf) (node key₂ value₂ t₅ t₆)) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ .leaf) (node kg ⟪ Red , _ ⟫ .leaf _)) .kn _ (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-single .kp .(⟪ Red , v2 ⟫)) ti₁) (rbr-rotate-lr .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt ⟪ <-trans lt2 x₁  , ⟪ <-tr> x₄ lt2  , <-tr> x₅ lt2 ⟫ ⟫  (t-single _ _) (t-right _ _ x₁ x₄ x₅ ti₁)
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .(node key _ _ _) leaf) (node key₂ value₂ t₅ t₆)) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ .leaf) (node kg ⟪ Red , _ ⟫ .leaf _)) .kn _ (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-left key .kp x₆ x₇ x₈ ti) ti₁) (rbr-rotate-lr .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 , v1 ⟫ (node kp ⟪ Red , v2 ⟫ t (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₁ trb
-... | t = ?
+RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-right .kp .key₁ x₆ x₇ x₈ ti) ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb
+... | t-single .kn .(⟪ Red , value₃ ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt tt ⟪ <-trans (proj1 rr01) x₁  , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫  (t-single _ _) (t-right _ _ x₁ x₄ x₅ ti₁) where
+        rr00 : (kp < kn) ∧ ⊤ ∧ ⊤
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫
+        rr01 : (kn < kg) ∧ ⊤ ∧ ⊤
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃
+... | t-right .kn key₃ {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫  ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01)  , <-tr> x₅ (proj1 rr01) ⟫ ⟫  (t-single _ _) (t-node _ _ _ (proj1 rr03) x₁ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₄ x₅  (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti trb)) ti₁) where
+        rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈)
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫
+        rr02 = proj1 (proj2 rr00)
+        rr01 : (kn < kg) ∧ ⊤ ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈)
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃
+        rr03 = proj2 (proj2 rr01)
+... | t-left key₃ .kn {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₉ , ⟪ x₁₀  , x₁₁ ⟫ ⟫ tt ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01)  , <-tr> x₅ (proj1 rr01) ⟫ ⟫  (t-right _ _  (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) (treeLeftDown _ _ (RB-repl→ti _ _ _ _  ti trb))) (t-right _ _ x₁ x₄ x₅ ti₁) where
+        rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ⊤
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫
+        rr02 = proj1 (proj2 rr00)
+        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) tt ?  ⟪ ? , ⟪ ? , ? ⟫ ⟫  ⟪ ?  , ⟪ ?  , ?  ⟫ ⟫  ? ? ? 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)
+        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 = proj2 (proj2 rr01)
+RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .(node key₃ _ _ _) (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-node key₃ .kp .key₁ x₆ x₇ x₈ x₉ x₁₀ x₁₁ ti ti₂) ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₂ trb
+... | t-single .kn .(⟪ Red , value₃ ⟫) = ?
+... | t-right .kn key₄ {t₇} {t₈} ₁₂ x₁₃ x₁₄ t = ?
+... | t-left key₄ .kn {t₇} {t₈} ₁₂ x₁₃ x₁₄ t = ?
+... | t-node key₄ .kn key₅ {v0} {v1} {v2} {t₇} {t₈} {t₉}  {t₁₀}x₁₂ x₁₃ x₁₄ x₁₅ x₁₆ x₁₇ t t₃ = ?
 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) = ?