Mercurial > hg > Gears > GearsAgda

changeset 806:a11ebb914b7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Moririn
date Wed, 20 Dec 2023 15:25:28 +0900
parents 28323f2e6dc4
children 858655384dea
files hoareBinaryTree1.agda
diffstat 1 files changed, 11 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Dec 18 18:58:21 2023 +0900
+++ b/hoareBinaryTree1.agda	Wed Dec 20 15:25:28 2023 +0900
@@ -626,9 +626,14 @@
    → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
    → rotatedTree  (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
    (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
+   
 RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A)
 RightDown leaf = leaf
 RightDown (node key ⟪ c , value ⟫ t1 t2) = t2
+LeftDown : {n : Level} {A :  Set n} → bt (Color ∧ A) → bt (Color ∧ A)
+LeftDown leaf = leaf
+LeftDown (node key ⟪ c , value ⟫ t1 t2 ) = t1
+
 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
  →  (tleft tright : bt (Color ∧ A))
  → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
@@ -983,11 +988,13 @@
                ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri≈ ¬a b ¬c = {!!}
                ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim {!!}
                ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb | t = {!!} --red -red
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ ? ? ? ? ? ) ? , ? ⟫
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim ?
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ (LeftDown repl) leaf (RBtreeLeftDown (LeftDown repl) leaf (RBI.replrb r)) rb-leaf (RBI.replrb r)) (RBI.replrb r) , {!!} ⟫
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = ⊥-elim (¬c {!!})
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim {!!}
                ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ | t = {!!}　-- red-red
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | t = {!!} 
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | tri< a ¬b ¬c = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | tri≈ ¬a b ¬c = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | tri> ¬a ¬b c = ⊥-elim {!!}
                --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫
                --... | rb-left-black x x₁ t | refl | rb | t = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫
                --... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb | t = {!!}