# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1683434199 -32400
# Node ID 9cdf272ca38c42a560abef399cdf53b1e4baba81
# Parent  bc9063c6fef319c4f0c55e4af4cd38e3620dd10d
... we need another invariant on depth of black

diff -r bc9063c6fef3 -r 9cdf272ca38c hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Sat May 06 21:33:42 2023 +0900
+++ b/hoareBinaryTree1.agda	Sun May 07 13:36:39 2023 +0900
@@ -805,12 +805,13 @@
     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 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant to d  → to ≡ orig
+        insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant orig d  → to ≡ orig
+          → (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 (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₂ d ro ro₁) refl (s-right x s-nil) refl = exit rot1 repl1 rrb ins13 ins12 where
+        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)
@@ -819,9 +820,6 @@
              ins12 = ?
              ins13 : rotatedTree (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) rot1
              ins13 = rr-node 
-             rrb : RBtreeInvariant repl1 d
-             rrb with repl | rbir 
-             ... | r1 | r2 = ?
              -- -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 ? ? ? ?)
@@ -830,17 +828,17 @@
            -- 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₂ d1 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₂ d1 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₂ d1 ro ro₁) eq (s-left x s-nil) refl = ?
+        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 = ?
     -- exit rot repl rbir ? ? 
     ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)