--- a/hoareBinaryTree1.agda	Mon Oct 16 19:42:05 2023 +0900
+++ b/hoareBinaryTree1.agda	Thu Oct 19 11:49:58 2023 +0900
@@ -39,7 +39,7 @@
 bt-depth leaf = 0
 bt-depth (node key value t t₁) = suc (bt-depth t  ⊔ bt-depth t₁ )
 
-open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
+open import Data.Unit hiding ( _≟_ ) -- ;  _≤?_ ; _≤_)
 
 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
     t-leaf : treeInvariant leaf 
@@ -443,7 +443,7 @@
    → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t) → t
 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) 
-... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where 
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where 
     TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
     TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) 
     TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
@@ -801,6 +801,13 @@
            →  RBtreeInvariant tree ∧  RBtreeInvariant (PG.parent pg) ∧  RBtreeInvariant (PG.grand pg) 
 PGtoRBinvariant = {!!}
 
+RBI-child-replaced : {n : Level} {A : Set n} (tr : bt (Color ∧ A)) (key : ℕ) →  RBtreeInvariant tr → RBtreeInvariant (child-replaced key tr) 
+RBI-child-replaced {n} {A} leaf key rbi = rbi
+RBI-child-replaced {n} {A} (node key₁ value tr tr₁) key rbi with <-cmp key key₁
+... | tri< a ¬b ¬c = RBtreeLeftDown _ _ rbi
+... | tri≈ ¬a b ¬c = rbi
+... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
+
 -- findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) 
 --           → (stack : List (bt (Color ∧ A)))           → treeInvariant tree0 ∧  stackInvariant key tree tree0 stack
 --           → {d : ℕ} →  RBtreeInvariant tree0 
@@ -928,19 +935,19 @@
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
     insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
-    
-    ... | case1 eq  = exit repl stack eq r {- record { -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
-        od = RBI.od r ; d = RBI.d r  ; rd = RBI.rd r ; --r
-        tree = RBI.tree r ; rot = RBI.rot r
-       ; origti = RBI.origti r
-       ; origrb = RBI.origrb r 
-       ; treerb = RBI.treerb r
-       ; replrb = RBI.replrb r
-       ; d=rd = RBI.d=d r
-       ; si = RBI.si r
-       ; rotated = RBI.rotated r
-       ; ri = RBI.ri r }  -}
-    ... | case2 (case1 eq) = {!!} where -- insertCase12
+    ... | case1 eq  = exit repl stack eq r 
+    ... | case2 (case1 eq) = insertCase12 orig (RBI.origrb r) refl (child-replaced key orig) (RBI-child-replaced orig key (RBI.origrb r) ) refl 
+      ( child-replaced key orig ∷ orig ∷ []) (rb02 orig refl (RBI.si r)) refl where -- insertCase12
+        rb01 : stackInvariant key (RBI.tree r) orig stack
+        rb01 = RBI.si r
+        rb02 :  (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
+           → stackInvariant key (RBI.tree r) orig stack
+           → stackInvariant key (child-replaced key orig) orig (child-replaced key orig ∷ orig ∷ [])
+        rb02 leaf eq si = ?
+        rb02  (node key₁ value tr tr₁) eq si with <-cmp key key₁
+        ... | tri< a ¬b ¬c = s-left _ _ _ a ?
+        ... | tri≈ ¬a b ¬c = ?
+        ... | tri> ¬a ¬b c = s-right _ _ _ c ?
         insertCase12 : (to : bt (Color ∧ A)) → RBtreeInvariant orig   → to ≡ orig
           → (rr : bt (Color ∧ A)) → RBtreeInvariant rr  → rr ≡ (child-replaced key orig)
           → (stack1 : List (bt (Color ∧ A))) → (si : stackInvariant key rr to stack1 )