Mercurial > hg > Gears > GearsAgda
changeset 892:6eee2a7b5288
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 22 May 2024 10:58:34 +0900 |
| parents | e8e8ccfd6c44 |
| children | 78d98511779a |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 4 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Tue May 21 18:43:44 2024 +0900 +++ b/hoareBinaryTree1.agda Wed May 22 10:58:34 2024 +0900 @@ -883,8 +883,10 @@ → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) → ( black-depth t₁ ≡ black-depth t₂ ) ∧ ( black-depth t₁ ≡ black-depth t₃ ) to-black-node-eq {n} {A} {key} {.key} {t₂} {.t₂} rbr-leaf = ⟪ refl , refl ⟫ -to-black-node-eq {n} {A} {key} {.key} {t₂} {.t₂} (rbr-node eq) = ⟪ trans ? (⊔-idem _) , ? ⟫ -to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-right x x₁ rr) = ? +to-black-node-eq {n} {A} {key} {.key} {t₂} {.t₂} {_} {t₃} {t₄} (rbr-node eq) = + ⟪ trans (cong (λ k → black-depth t₃ ⊔ k) (sym eq) ) (⊔-idem _) , + trans (cong (λ k → k ⊔ black-depth t₄ ) eq ) (⊔-idem _) ⟫ +to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} {.(node t₁ ⟪ Red , t₃ ⟫ t₅ t₉)} {t₅} {node key₁ value t₆ t₇} (rbr-right {_} {_} {_} {.(node key₁ value t₆ t₇)} {.t₅} {t₉} x x₁ rr) = ? to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-left x x₁ rr) = ? to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-flip-ll x x₁ x₂ rr) = ? to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-flip-lr x x₁ x₂ x₃ rr) = ?