--- a/hoareBinaryTree1.agda	Mon Aug 21 19:29:26 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Oct 02 18:44:21 2023 +0900
@@ -301,7 +301,8 @@
         ... |  tri≈ ¬a b ¬c = ⊥-elim (¬a x)
         ... |  tri> ¬a ¬b c = ⊥-elim (¬a x)
         repl12 : replacedTree key value (child-replaced key  tree1  ) repl
-        repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
+        repl12 = subst₂ {!!} {!!} {!!} {!!}
+       -- repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ 
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
@@ -927,23 +928,36 @@
       -- 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 record {  -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
-       od = {!!} ; d = {!!} ; rd = {!!}
-       ; tree = RBI.tree r ; rot = {!!}
-       ; origti = {!!}
-       ; origrb = {!!}
-       ; treerb = {!!}
-       ; replrb = {!!}
-       ; d=rd = {!!}
-       ; si = {!!}
-       ; rotated = {!!}
-       ; ri = {!!} }
-    ... | case2 (case1 eq ) = {!!} where
-        insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant orig   → to ≡ orig
-          → (rr : bt (Color ∧ A)) → {dr : ℕ} → RBtreeInvariant {!!}   → rr ≡ {!!}
-          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key {!!} to stack ) 
-          → stack ≡ {!!} ∷ to ∷ [] → t
-        insertCase12 = {!!}
+    ... | case1 eq = exit repl stack eq  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=rd r
+       ; si = RBI.si r
+       ; rotated = RBI.rotated r
+       ; ri = RBI.ri r } 
+    ... | case2 (case1 eq) = {!!} where -- insertCase12
+        insertCase12 : (to : bt (Color ∧ A)) → RBtreeInvariant orig   → to ≡ orig
+          → (rr : bt (Color ∧ A)) → RBtreeInvariant repl → rr ≡ repl
+          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key rr to stack ) 
+          → stack ≡ rr  ∷ to ∷ [] → t
+        insertCase12 to origrb to≡orig rr rrrb rr≡repl si s≡  = next rr stack 
+{-         record {
+         od = RBI.od r ; d = RBI.d r  ; rd = RBI.rd r ; --r
+         tree = rr ; rot = RBI.rot r
+         ; origti = RBI.origti r
+         ; origrb = RBI.origrb r
+         ; treerb = rrrb
+         ; replrb = rrrb
+         ; d=rd = RBI.d=rd r
+         ; si = si
+         ; rotated = RBI.rotated r
+         ; ri = {!!} }
+         -}
+         ? {!!}
     -- exit rot repl rbir ? ? 
     ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)