Mercurial > hg > Gears > GearsAgda
changeset 903:d79ffbf8f450
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 31 May 2024 12:25:36 +0900 |
| parents | 20207255b094 |
| children | e86f6b9545fc |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 11 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Fri May 31 10:46:03 2024 +0900 +++ b/hoareBinaryTree1.agda Fri May 31 12:25:36 2024 +0900 @@ -1947,16 +1947,18 @@ suc (black-depth (PG.uncle pg)) ≡⟨ to-black-eq (PG.uncle pg) (cong color uneq ) ⟩ black-depth (to-black (PG.uncle pg)) ∎ where open ≡-Reasoning - rb16 : (tree : bt (Color ∧ A)) - → tree ≡ node kg vg (PG.parent pg) (PG.uncle pg) - → (ti : treeInvariant (node kg vg (PG.parent pg) (PG.uncle pg))) → child-replaced key tree ≡ PG.parent pg - rb16 leaf eq ti = ? - rb16 (node key₁ value tree tree₁) eq ti with <-cmp key key₁ - ... | tri< a ¬b ¬c = ? - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? + rb16 : kg < key + rb16 = ? rb14 : suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡ black-depth (child-replaced key (PG.grand pg)) - rb14 = ? + rb14 = begin + suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ cong (λ k → k ⊔ black-depth (to-black (PG.uncle pg))) rb12 ⟩ + black-depth (to-black (PG.uncle pg)) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ ⊔-idem _ ⟩ + black-depth (to-black (PG.uncle pg)) ≡⟨ sym (to-black-eq (PG.uncle pg) (cong color uneq )) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ sym (cong suc ( cong black-depth (child-replaced-right rb16 ))) ⟩ + suc (black-depth (child-replaced key (node kg vg (PG.parent pg) (PG.uncle pg)))) ≡⟨ cong (λ k → suc (black-depth (child-replaced key k))) (sym x₁) ⟩ + suc (black-depth (child-replaced key (PG.grand pg))) ≡⟨ ? ⟩ + black-depth (child-replaced key (PG.grand pg)) ∎ + where open ≡-Reasoning rb15 : suc (length (PG.rest pg)) < length stack rb15 = ?