# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1697701271 -32400
# Node ID 846663e9858be513db806ca66fd5e0172f07dfde
# Parent  3bf3433a32d1f60b7ee876421b65f73af5261c78
...

diff -r 3bf3433a32d1 -r 846663e9858b hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Thu Oct 19 12:01:08 2023 +0900
+++ b/hoareBinaryTree1.agda	Thu Oct 19 16:41:11 2023 +0900
@@ -579,7 +579,9 @@
 
 
 data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
-  rtt-node : {t : bt A } → rotatedTree t t
+  rtt-unit : {t : bt A} → rotatedTree t t
+  rtt-node : {left left' right right' : bt A} → {ke : ℕ} {ve : A} → 
+      rotatedTree left left' → rotatedTree right right' → rotatedTree (node ke ve left right) (node ke ve left' right')
   --     a              b
   --   b   c          d   a
   -- d   e              e   c
@@ -687,13 +689,11 @@
 
 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
-       od d rd : ℕ
        tree rot : bt (Color ∧ A)
        origti : treeInvariant orig
        origrb : RBtreeInvariant orig
        treerb : RBtreeInvariant tree
        replrb : RBtreeInvariant repl
-       d=rd : ( d ≡ rd ) ∨ ( (suc d ≡ rd ) ∧ (color tree ≡ Red))
        si : stackInvariant key tree orig stack
        rotated : rotatedTree tree rot
        ri : replacedRBTree key value (child-replaced key rot ) repl
@@ -942,22 +942,32 @@
         rb02 :  (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
            → stackInvariant key (RBI.tree r) orig stack
            → t
-        rb02 leaf eq si = ? -- can't happen
-        rb02  (node key₁ value left right) eq si with <-cmp key key₁
-        ... | tri< a ¬b ¬c = exit ? ? ?   record {
-             od = RBI.od r ; d = RBI.rd r  ; rd = RBI.rd r ; --r
-             tree = {!!} ; rot = RBI.rot r
+        rb02 leaf eq1 si = ? -- can't happen
+        rb02  (node key₁ value₁ left right) eq1 si with <-cmp key key₁
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a b ¬c = ? -- can't happen
+        ... | tri> ¬a ¬b c = rb03 value₁ refl where
+           rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → right ≡ RBI.tree r
+           rb04 (s-right tree ty tree₁ x s-nil) refl = ?
+           rb04 (s-left tree₁ ty tree x si) refl = ?
+           rb03 : (v : Color ∧ A ) → v ≡ value₁ → t
+           rb03 ⟪ Black , value₄ ⟫ eq2 = exit (node key₁ value₁ left (RBI.tree r)) (orig ∷ [])  refl record {
+             tree = orig ; rot = node key₁ value₁ left (RBI.rot r) 
              ; origti = RBI.origti r
              ; origrb = RBI.origrb r
-             ; treerb = {!!}  --subst (λ k → RBtreeInvariant k) (sym t≡o) (or)
-             ; replrb = ? --subst (λ k → RBtreeInvariant k) (sym t≡o) (RBI.origrb r)
-             ; d=rd = {!!}
-             ; si = {!!} --subst (λ k → stackInvariant key rr k stack1) (t≡o) (sti)
-             ; rotated = {!!}
-             ; ri = {!!} --subst (λ k → replacedRBTree key value (child-replaced key (RBI.rot r)) k) (sym t≡o) ({!ct!})
+             ; treerb = RBI.origrb r
+             ; replrb = ?
+             ; si = s-nil
+             ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) (
+                trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq))) eq1) (rtt-node rtt-unit (RBI.rotated r))
+             ; ri = {!!} 
              }
-        ... | tri≈ ¬a b ¬c = ? -- can't happen
-        ... | tri> ¬a ¬b c = ?
+           rb03 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
+           ... | Black = exit ? ? ? ? 
+           ... | Red = exit ? ? ? ?
+           --       r = orig                            RBI.tree b
+           --      / \                       =>         /    \
+           --     b   b → r RBI.tree r             r = orig   o (r/b)
     ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)