Mercurial > hg > Gears > GearsAgda

changeset 880:3b030eb540d9

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 12:31:47 +0900
parents 32e026c5f31f
children 749e59e3c569
files hoareBinaryTree1.agda
diffstat 1 files changed, 27 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat May 04 00:44:56 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat May 04 12:31:47 2024 +0900
@@ -1276,7 +1276,7 @@
         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
+... | 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 ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫  ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫  ⟪ <-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-node _ _ _ (proj1 rr03) x₁ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₄ x₅ t₃ 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)
@@ -1284,10 +1284,32 @@
         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₃ = ?
+... | t-single .kn .(⟪ Red , value₃ ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00)  , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫  tt tt ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01)  , <-tr> x₅ (proj1 rr01) ⟫ ⟫  (t-left _ _ x₆ x₈ x₉ ti) (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) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫  tt ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫  ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫  (t-left _ _ x₆ x₈ x₉ ti) (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 = proj2 (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) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫  ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫  tt ⟪ <-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 (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) ? ? ? ? (t-node _ _ _ ? ? ? ? ? ? ti t ) (t-node _ _ _ ? ? ? ? ? ? (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)
+        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)
 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) = ?