# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1683435467 -32400
# Node ID 1bb96bc9eb45af62730d50f820fb3fa389189266
# Parent  9cdf272ca38c42a560abef399cdf53b1e4baba81
...

diff -r 9cdf272ca38c -r 1bb96bc9eb45 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Sun May 07 13:36:39 2023 +0900
+++ b/hoareBinaryTree1.agda	Sun May 07 13:57:47 2023 +0900
@@ -809,36 +809,7 @@
           → (rr : bt (Color ∧ A)) → {dr : ℕ} → RBtreeInvariant repl dr  → rr ≡ repl
           → {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 rr rbi eqr (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) leaf) (rb-left-red x₁ ro) eq rr rbi eqr (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₂ d ro ro₁) refl rr rbi eqr (s-right x s-nil) refl = exit rot1 repl1 ? ins13 ins12 where
-             rot1 : bt (Color ∧ A)
-             rot1 = node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)
-             repl1 : bt (Color ∧ A)
-             repl1 = node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) repl 
-             ins12 : replacedRBTree key value  (child-replaced key rot1) repl1
-             ins12 = ?
-             ins13 : rotatedTree (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) rot1
-             ins13 = rr-node 
-             -- -subst (λ k → RBtreeInvariant k d ) ? (rb-node-red ? ? d ro (subst₂ (λ j k → RBtreeInvariant j k) ? ? rbir ))
-
-        -- 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 → replacedRBTree 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 rr rbi eqr (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq rr rbi eqr (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq rr rbi eqr (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ d1 ro ro₁) eq rr rbi eqr (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node _ ⟪ Black , _ ⟫ _ _)) (rb-right-red x₁ ro) eq rr rbi eqr (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) leaf) (rb-left-red x₁ ro) eq rr rbi eqr (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x₁ x₂ d1 ro ro₁) eq rr rbi eqr (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq rr rbi eqr (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq rr rbi eqr (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq rr rbi eqr (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ d1 ro ro₁) eq rr rbi eqr (s-left x s-nil) refl = ?
+        insertCase12 = ?
     -- exit rot repl rbir ? ? 
     ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)