Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 877:100e9fd87d83

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 Fri, 03 May 2024 14:33:41 +0900
parents f772362dde8d
children feeb6982fd46
comparison
equal deleted inserted replaced
876:f772362dde8d 877:100e9fd87d83
1232 ... | 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 1232 ... | 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
1233 rr00 : (kp < kn) ∧ ⊤ ∧ ⊤ 1233 rr00 : (kp < kn) ∧ ⊤ ∧ ⊤
1234 rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ 1234 rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫
1235 rr01 : (kn < kg) ∧ ⊤ ∧ ⊤ 1235 rr01 : (kn < kg) ∧ ⊤ ∧ ⊤
1236 rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ 1236 rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂
1237 ... | 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 1237 ... | 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₁₁ ⟫ ⟫ tt (t-left _ _ x₃ x₅ x₆ ti) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) where
1238 rr00 : (kp < kn) ∧ ⊤ ∧ tr> kp (node key₃ v3 t₇ t₈) 1238 rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) -- tr> kp (node key₃ v3 t₇ t₈)
1239 rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ 1239 rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫
1240 rr02 = proj1 (proj2 rr00) 1240 rr02 = proj1 (proj2 rr00)
1241 rr01 : (kn < kg) ∧ ⊤ ∧ tr< kg (node key₃ v3 t₇ t₈) 1241 rr01 : (kn < kg) ∧ ⊤ ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) -- tr< kg (node key₃ v3 t₇ t₈)
1242 rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ 1242 rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂
1243 rr03 : ? 1243 rr03 = proj2 (proj2 rr01)
1244 rr03 with RB-repl→ti _ _ _ _ ti₁ trb 1244 ... | 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 tt (t-node key₂ kp key₃ x₃ (proj1 rr02) x₅ x₆ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) (t-single _ _) where
1245 ... | t-right .kn .key₃ x x₁ x₂ t = ? 1245 rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ⊤
1246 ... | t-left key₃ .kn x₉ x₁₀ x₁₁ t = ? 1246 rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫
1247 ... | t-node key₃ .kn key₄ x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₃ = ? 1247 rr02 = proj1 (proj2 rr00)
1248 rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ⊤
1249 rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂
1250 ... | 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₁₄ ⟫ ⟫ tt (t-node _ _ _ x₃ (proj1 rr02) x₅ x₆ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t₃) where
1251 rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ((kp < key₄) ∧ tr> kp t₉ ∧ tr> kp t₁₀)
1252 rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫
1253 rr02 = proj1 (proj2 rr00)
1254 rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ((key₄ < kg) ∧ tr< kg t₉ ∧ tr< kg t₁₀)
1255 rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂
1256 rr03 = proj2 (proj2 rr01)
1257
1248 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) = ? 1258 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) = ?
1249 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) = ? 1259 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) = ?
1250 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) = ? 1260 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) = ?
1251 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) = ? 1261 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) = ?
1252 1262