--- a/hoareBinaryTree1.agda	Fri May 05 10:14:53 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat May 06 01:25:46 2023 +0900
@@ -797,13 +797,28 @@
     insertCase1 with stackToPG tree orig stack si
     ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
     ... | case2 (case1 eq ) = ? where
-        insertCase12 : (orig : bt (Color ∧ A)) 
-          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree orig stack ) 
-          → stack ≡ tree ∷ orig ∷ [] → t
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ t1 tree) (s-right x s-nil) refl = exit rot repl rbir ? ? 
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ t1 tree) (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ tree t1) (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ tree t1) (s-left x s-nil) refl = ?
+        insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant to d  → to ≡ orig
+          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree to stack ) 
+          → stack ≡ tree ∷ to ∷ [] → t
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node k2 ⟪ Black , v2 ⟫ t1 t2)) (rb-right-red x₁ ro) eq (s-right x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) leaf) (rb-left-red x₁ ro) eq (s-right x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) (rb-node-red x₁ x₂ ro ro₁) eq (s-right x s-nil) refl = exit (node k1 ⟪ Red , v1 ⟫ t1 rot) (node k1 ⟪ Black , v1 ⟫ ? ?) (rb-node-black ? ? ? ?)
+           (subst₂ (λ j k → rotatedTree j k ) eq ? (rr-right ? rr-node rr-node roti))
+           (subst (λ k → replacedTree key ⟪ ? , value ⟫ ? ?) ? (r-right ? ri)) 
+           -- k1 < key
+           --     ⟪ red , k1 ⟫
+           --   t1            tree → rot → repl
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq (s-right x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq (s-right x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq (s-right x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ ro ro₁) eq (s-right x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node _ ⟪ Black , _ ⟫ _ _)) (rb-right-red x₁ ro) eq (s-left x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) leaf) (rb-left-red x₁ ro) eq (s-left x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x₁ x₂ ro ro₁) eq (s-left x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq (s-left x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq (s-left x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq (s-left x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ ro ro₁) eq (s-left x s-nil) refl = ?
     -- exit rot repl rbir ? ? 
     ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)