Mercurial > hg > Gears > GearsAgda
changeset 873:0c36153cd08f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 May 2024 01:19:15 +0900 |
| parents | 2eed87eb01e3 |
| children | 3fd3ab3bff54 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 11 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Wed May 01 22:21:16 2024 +0900 +++ b/hoareBinaryTree1.agda Thu May 02 01:19:15 2024 +0900 @@ -1201,7 +1201,17 @@ RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ leaf leaf) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .kn _ (t-left .kp .kg x x₁ x₂ ti) (rbr-rotate-lr .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ (node key₁ value₁ t t₁) leaf) .leaf) (node kn ⟪ Black , v3 ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .kn .v3 (t-left .kp .kg x x₁ x₂ (t-left .key₁ .kp x₃ x₄ x₅ 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 tt (t-left _ _ x₃ x₄ x₅ ti) (t-single _ _) -RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ 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₂ ti) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) = ? +RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ .(⟪ Red , _ ⟫) .leaf .leaf)) .leaf) (node .key₁ ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .key₁ _ (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .leaf kg kp .key₁ lt1 lt2 rbr-node) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) +RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ value₁ t₁ t₂)) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ (node key₂ value₂ t₄ t₅) t₆)) key value (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .(node key₂ value₂ t₄ t₅) kg kp kn lt1 lt2 trb) = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt ? tt (t-single _ _) (t-left _ _ ? ? ? (treeRightDown _ _ ( RB-repl→ti _ _ _ _ ti trb))) where + rr00 : (kp < kn) ∧ ⊤ ∧ tr> kp (node key₂ value₂ t₄ t₅) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ + rr01 : (kn < kg) ∧ tr< kg leaf ∧ tr< kg (node key₂ value₂ t₄ t₅) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ +RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ value₁ t₁ t₂)) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ (node key₂ value₂ t₃ t₅)) (node kg ⟪ Red , _ ⟫ leaf _)) key value (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .(node key₂ value₂ t₃ t₅) .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ? +RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ value₁ t₁ t₂)) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ (node key₂ value₂ t₃ t₅)) (node kg ⟪ Red , _ ⟫ (node key₃ value₃ t₄ t₆) _)) key value (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .(node key₂ value₂ t₃ t₅) .(node key₃ value₃ t₄ t₆) kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ? +-- rr00 : (kp < kn) ∧ tr> kp t₃ ∧ tr> kp t₄ +-- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ +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 ⟫ 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) = ?