--- a/hoareBinaryTree1.agda	Mon May 08 13:32:42 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon May 08 18:49:57 2023 +0900
@@ -212,6 +212,14 @@
      ri : replacedTree key value (child-replaced key tree ) repl
      ci : C tree repl stack     -- data continuation
    
+record replacePR' {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt A ) (stack : List (bt A))  : Set n where
+   field
+     tree repl : bt A
+     ti : treeInvariant orig
+     si : stackInvariant key tree orig stack
+     ri : replacedTree key value (child-replaced key tree) repl
+     --   treeInvariant of tree and repl is inferred from ti, si and ri.
+   
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
     → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
     → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value (child-replaced key tree) tree1 → t) → t
@@ -547,6 +555,18 @@
        → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) d
        → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) (suc d)
 
+-- RBttreeInvariant tree bd → treeInvariant is easy
+
+RBti→ti : {n : Level} {A : Set n}  (tree : bt (Color ∧ A)) {bd : ℕ} → RBtreeInvariant tree bd → treeInvariant tree
+RBti→ti {n} {A} .leaf rb-leaf = t-leaf
+RBti→ti {n} {A} .(node key ⟪ Black , value ⟫ leaf leaf) (rb-single key value) = t-single ? ?
+RBti→ti {n} {A} .(node _ ⟪ Red , _ ⟫ leaf (node _ ⟪ Black , _ ⟫ _ _)) (rb-right-red x bd) = ?
+RBti→ti {n} {A} .(node _ ⟪ Black , _ ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x bd) = ?
+RBti→ti {n} {A} .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) leaf) (rb-left-red x bd) = ?
+RBti→ti {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x bd) = ?
+RBti→ti {n} {A} .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x x₁ _ bd bd₁) = ?
+RBti→ti {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x x₁ d bd bd₁) = ?
+
 tesr-rb-0 : RBtreeInvariant {_} {ℕ} leaf 0
 tesr-rb-0 = rb-leaf
 
@@ -613,20 +633,31 @@
 
 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
-     od d rd : ℕ
-     tree rot repl : bt (Color ∧ A)
-     origrb : RBtreeInvariant orig od
-     treerb : RBtreeInvariant tree d
-     replrb : RBtreeInvariant repl rd
-     d=rd : ( d ≡ rd ) ∨ ( suc d ≡ rd )
-     si : stackInvariant key tree orig stack
-     rotated : rotatedTree tree rot
-     ri : replacedRBTree key value (child-replaced key rot ) repl
+       od d rd : ℕ
+       tree rot repl : bt (Color ∧ A)
+       origrb : RBtreeInvariant orig od
+       treerb : RBtreeInvariant tree d
+       replrb : RBtreeInvariant repl rd
+       d=rd : ( d ≡ rd ) ∨ ( suc d ≡ rd )
+       si : stackInvariant key tree orig stack
+       rotated : rotatedTree tree rot
+       ri : replacedRBTree key value (child-replaced key rot ) repl
    
 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (tree orig : bt (Color ∧ A) )
            →  (stack : List (bt (Color ∧ A))) 
            →  stack ≡ tree ∷ orig ∷ [] → RBI key value orig stack → RBI key value orig (orig ∷ [])
-rbi-case1 {n} {A} {key} {value} tree₁ .(node _ _ t1 tree₁) (tree₁ ∷ .(node _ _ t1 tree₁) ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-right .tree₁ .(node _ _ t1 tree₁) t1 x s-nil) ; rotated = rotated ; ri = ri } = ?
+rbi-case1 {n} {A} {key} {value} tree₁ .(node k1 ⟪ Red , v1 ⟫ t1 tree₁) (tree₁ ∷ node k1 ⟪ Red , v1 ⟫ t1 tree₁ ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-right .tree₁ .(node _ ⟪ Red , v1 ⟫ t1 tree₁) t1 x s-nil) ; rotated = rotated ; ri = ri } = record {
+       od = od ; d = ? ; rd = ?
+     ; tree = node _ ⟪ Red , v1 ⟫ t1 tree₁ ; rot = ? ; repl = node k1 ⟪ Red , v1 ⟫ t1 repl
+     ; origrb = origrb
+     ; treerb = ?
+     ; replrb = ?
+     ; d=rd = ?
+     ; si = s-nil
+     ; rotated = ?
+     ; ri = ?
+   }
+rbi-case1 {n} {A} {key} {value} tree₁ .(node _ ⟪ Black , proj4 ⟫ t1 tree₁) (tree₁ ∷ node _ ⟪ Black , proj4 ⟫ t1 tree₁ ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-right .tree₁ .(node _ ⟪ Black , proj4 ⟫ t1 tree₁) t1 x s-nil) ; rotated = rotated ; ri = ri } = ?
 rbi-case1 {n} {A} {key} {value} tree₁ orig (tree₁ ∷ orig ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-left _ _ _ x si) ; rotated = rotated ; ri = ri } = ?
 
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )