Mercurial > hg > Gears > GearsAgda

changeset 876:f772362dde8d

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 Thu, 02 May 2024 19:29:15 +0900
parents d7e255dbaa84
children 100e9fd87d83
files hoareBinaryTree1.agda
diffstat 1 files changed, 17 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu May 02 11:43:24 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu May 02 19:29:15 2024 +0900
@@ -1228,7 +1228,23 @@
         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₂)) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-left .kp .kg x x₁ x₂ (t-node key₂ .kp .key₁ x₃ x₄ x₅ x₆ x₇ x₈ ti ti₁)) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
+RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ (node key₂ value₂ t₅ t₆) (node key₁ value₁ t₁ t₂)) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-left .kp .kg x x₁ x₂ (t-node key₂ .kp .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-single .kn .(⟪ Red , _ ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00)  , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫  tt tt tt (t-left _ _ x₃ x₅ x₆ ti) (t-single _ _) 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) ? ? ? ? ? (t-left _ _ ? ? ? ti) (t-left _ _ ? ? ? (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) where
+        rr00 : (kp < kn) ∧ ⊤ ∧ tr> kp (node key₃ v3 t₇ t₈)
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫
+        rr02 = proj1 (proj2 rr00)
+        rr01 : (kn < kg) ∧ ⊤ ∧ tr< kg (node key₃ v3 t₇ t₈)
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂
+        rr03 : ?
+        rr03 with RB-repl→ti _ _ _ _ ti₁ trb
+        ... | t-right .kn .key₃ x x₁ x₂ t = ?
+... | t-left key₃ .kn x₉ x₁₀ x₁₁ t = ?
+... | t-node key₃ .kn key₄ x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₃ = ?
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ t leaf) .(node key₂ _ _ _)) (node kn ⟪ Black , _ ⟫ (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) = ?
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ t (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , _ ⟫ (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) = ?
 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) = ?