Mercurial > hg > Gears > GearsAgda

changeset 785:c3cce455e4e7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Aug 2023 19:29:26 +0900
parents 2955d5b7debd
children 12e19644535e
files hoareBinaryTree1.agda logic.agdai
diffstat 2 files changed, 350 insertions(+), 190 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Aug 21 19:06:34 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Aug 21 19:29:26 2023 +0900
@@ -5,7 +5,7 @@
 open import Data.Nat hiding (compare)
 open import Data.Nat.Properties as NatProp
 open import Data.Maybe
-open import Data.Maybe.Properties
+-- open import Data.Maybe.Properties
 open import Data.Empty
 open import Data.List
 open import Data.Product
@@ -58,9 +58,9 @@
 --
 data stackInvariant {n : Level} {A : Set n}  (key : ℕ) : (top orig : bt A) → (stack  : List (bt A)) → Set n where
     s-nil :  {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
-    s-right :  {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
+    s-right :  (tree tree0 tree₁ : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
         → key₁ < key  →  stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
-    s-left :  {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
+    s-left :  (tree₁ tree0 tree : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
         → key  < key₁ →  stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
 
 data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt A ) → Set n where
@@ -94,25 +94,25 @@
 stack-last (x ∷ s) = stack-last s
 
 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
-stackInvariantTest1 = s-right (add< 3) (s-nil  )
+stackInvariantTest1 = s-right _ _ _ (add< 3) (s-nil  )
 
 si-property0 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
 si-property0  (s-nil  ) ()
-si-property0  (s-right x si) ()
-si-property0  (s-left x si) ()
+si-property0  (s-right _ _ _ x si) ()
+si-property0  (s-left _ _ _ x si) ()
 
 si-property1 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 (tree1 ∷ stack)
    → tree1 ≡ tree
 si-property1 (s-nil   ) = refl
-si-property1 (s-right _  si) = refl
-si-property1 (s-left _  si) = refl
+si-property1 (s-right _ _ _ _  si) = refl
+si-property1 (s-left _ _ _ _  si) = refl
 
 si-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-last stack ≡ just tree0
 si-property-last key t t0 (t ∷ [])  (s-nil )  = refl
-si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with  si-property1 si
+si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ _ _ _ si ) with  si-property1 si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
-si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with  si-property1  si
+si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
@@ -179,8 +179,8 @@
 findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st  Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st)
        ⟪ treeLeftDown tree tree₁ (proj1 Pre)  , findP1 a st (proj2 Pre) ⟫ depth-1< where
    findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
-   findP1 a (x ∷ st) si = s-left a si
-findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2<
+   findP1 a (x ∷ st) si = s-left _ _ _ a si
+findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right _ _ _ c (proj2 Pre) ⟫ depth-2<
 
 replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
@@ -212,8 +212,16 @@
      ri : replacedTree key value (child-replaced key tree ) repl
      ci : C tree repl stack     -- data continuation
    
+record replacePR' {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt A ) (stack : List (bt A))  : Set n where
+   field
+     tree repl : bt A
+     ti : treeInvariant orig
+     si : stackInvariant key tree orig stack
+     ri : replacedTree key value (child-replaced key tree) repl
+     --   treeInvariant of tree and repl is inferred from ti, si and ri.
+   
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
- → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
+    → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
     → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value (child-replaced key tree) tree1 → t) → t
 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf
 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P)
@@ -268,7 +276,7 @@
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where
     Post :  replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
     Post with replacePR.si Pre 
-    ... | s-right  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-right  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ leaf
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -281,7 +289,7 @@
         ... |  tri> ¬a ¬b c = refl
         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
-    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-left  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 leaf tree₁ 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -298,7 +306,7 @@
 ... | 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 ⊤) 
     Post with replacePR.si Pre 
-    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -322,7 +330,7 @@
             child-replaced key tree1 ∎  where open ≡-Reasoning
         repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value₁ repl right)
         repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04  (r-left a (replacePR.ri Pre)) 
-    ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁  
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -349,7 +357,7 @@
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st Post ≤-refl where 
     Post :  replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
     Post with replacePR.si Pre 
-    ... | s-right  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
+    ... | s-right  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁  left right)
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -363,7 +371,7 @@
         repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
         repl12 refl with repl09 
         ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
-    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
+    ... | s-left  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree tree₁ 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -380,7 +388,7 @@
 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) 
     Post with replacePR.si Pre 
-    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -404,7 +412,7 @@
             child-replaced key tree1 ∎  where open ≡-Reasoning
         repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value₁ left repl)
         repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) 
-    ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁  
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -522,47 +530,143 @@
     Red : Color
     Black : Color
 
-data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → (bd : ℕ) → Set n where
-    rb-leaf     : RBtreeInvariant leaf 0
-    rb-single : (key : ℕ) → (value : A) → (c : Color) →  RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) 1
-    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ }
-       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) d
-       → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) d
-    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ } {c : Color}
-       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) d
-       → RBtreeInvariant (node key  ⟪ Black , value  ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) (suc d) --この時点でbalanceしてる必要はない
-    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ }
-       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) d
-       → RBtreeInvariant (node key₁  ⟪ Red ,   value  ⟫ (node key ⟪ Black , value₁ ⟫ t t₁) leaf ) d
-    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ } {c : Color}
-       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) d
-       → RBtreeInvariant (node key₁  ⟪ Black , value  ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) (suc d)
-    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {d : ℕ}
-       → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) d
-       → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) d
-       → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) d
-    rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {d : ℕ}
+RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A     
+RB→bt {n} A leaf = leaf
+RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1))
+
+color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color
+color leaf = Black
+color (node key ⟪ C , value ⟫ rb rb₁) = C
+
+black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ
+black-depth leaf = 0
+black-depth (node key ⟪ Red , value ⟫  t t₁) = black-depth t  ⊔ black-depth t₁ 
+black-depth (node key ⟪ Black , value ⟫  t t₁) = suc (black-depth t  ⊔ black-depth t₁ )
+
+data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
+    rb-leaf : RBtreeInvariant leaf
+    rb-single : (key : ℕ) → (value : A) →  RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf)
+    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
+       → black-depth t ≡ black-depth t₁ 
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 
+       → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁))
+    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
+       → black-depth t ≡ black-depth t₁
+       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 
+       → RBtreeInvariant (node key  ⟪ Black , value  ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) 
+    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
+       → black-depth t ≡ black-depth t₁
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 
+       → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf ) 
+    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
+       → black-depth t ≡ black-depth t₁
+       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 
+       → RBtreeInvariant (node key  ⟪ Black , value  ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf) 
+    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
+       → black-depth t₁ ≡ black-depth t₂
+       → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂)
+       → black-depth t₃ ≡ black-depth t₄
+       → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)
+       → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄))
+    rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
        → {c c₁ : Color}
-       → RBtreeInvariant (node key  ⟪ c  , value  ⟫ t₁ t₂) d
-       → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) d
-       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) (suc d)
+       → black-depth t₁ ≡ black-depth t₂
+       → RBtreeInvariant (node key  ⟪ c  , value  ⟫ t₁ t₂)
+       → black-depth t₃ ≡ black-depth t₄
+       → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) 
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄))
 
 
--- This one can be very difficult
--- data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
---    rb-leaf : replacedRBTree key value leaf (node key ⟪ Black , value ⟫ leaf leaf)
+data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
+  rtt-node : {t : bt A } → rotatedTree t t
+  --     a              b
+  --   b   c          d   a
+  -- d   e              e   c
+  --                                                                                                                   
+  rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
+    --kd < kb < ke < ka< kc
+   → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A}
+   → kd < kb → kb < ke → ke < ka → ka < kc
+   → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
+   → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
+   → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
+   → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
+    (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
+
+  rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
+    --kd < kb < ke < ka< kc
+   → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child 
+   → kd < kb → kb < ke → ke < ka → ka < kc
+   → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
+   → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
+   → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
+   → rotatedTree  (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
+   (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
+
+RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
+ →  (tleft tright : bt (Color ∧ A))
+ → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) 
+ → RBtreeInvariant tleft
+RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf
+RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf
+RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf
+RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf
+RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
+RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti
+RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
+RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
+RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = til
+RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
+RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
+RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
 
-color : {n : Level} (A : Set n)  → (rb : bt (Color ∧ A)) → Color
-color {n} A leaf = Red
-color {n} A (node key ⟪ c , v ⟫ rb rb₁) = c
+RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color}
+ → (tleft tright : bt (Color ∧ A))
+ → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) 
+ → RBtreeInvariant tright 
+RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf
+RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti
+RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti
+RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti
+RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
+RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf
+RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
+RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
+RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = tir
+RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
+RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
+RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
 
-RB→bt : {n : Level} (A : Set n)  → (rb : bt (Color ∧ A)) → bt A
-RB→bt {n} A leaf = leaf
-RB→bt {n} A (node key ⟪ c , value ⟫ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
+findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) 
+           → (stack : List (bt (Color ∧ A)))
+           → treeInvariant tree ∧  stackInvariant key tree tree0 stack
+           → RBtreeInvariant tree
+           → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A)))
+                   → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
+                   → RBtreeInvariant tree1 
+                   → bt-depth tree1 < bt-depth tree → t )
+           → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) 
+                 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
+                 → RBtreeInvariant tree1 
+                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl)
+findRBT key n@(node key₁ value left right) tree0 stack ti  rb0 next exit with <-cmp key key₁
+findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c
+ = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left _ _ _ a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1<
+findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl)
+findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c
+ = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right _ _ _ c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2<
+
+
+data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
+    rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
+    rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁) 
+    rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
+          → k < key →  replacedRBTree key value t2 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t) 
+    rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
+          → k < key →  replacedRBTree key value t1 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) 
 
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
---self parent grand n の並び
--- n2 is uncle
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
         → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand 
     s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
@@ -572,23 +676,6 @@
     s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
         → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand 
 
--- with color
-data rotatedTree  {n : Level} {A : Set n}  : (before after : bt A ) → Set n where
-    rr-node : {t : bt A} → rotatedTree t t
-    --      a                 b 
-    --    b   c             d   a
-    --  d   e                 e   c
-    rr-right : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A}
-          → ka < kb
-          → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁
-          → rotatedTree (node ka va (node kb vb d e)  c) (node kb vb d₁ (node ka va e₁ c₁) ) 
-    --     b                  a 
-    --   d   a              b   c
-    --     e   c          d   e
-    rr-left : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A}
-          → ka < kb
-          → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁
-          → rotatedTree (node kb vb d (node ka va e c) ) (node ka va (node kb vb d₁ e₁)  c₁) 
 
 record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where
     field
@@ -597,159 +684,215 @@
        rest : List (bt A)
        stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
 
+record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
+   field
+       od d rd : ℕ
+       tree rot : bt (Color ∧ A)
+       origti : treeInvariant orig 
+       origrb : RBtreeInvariant orig 
+       treerb : RBtreeInvariant tree 
+       replrb : RBtreeInvariant repl 
+       d=rd : ( d ≡ rd ) ∨ ( (suc d ≡ rd ) ∧ (color tree ≡ Red))
+       si : stackInvariant key tree orig stack
+       rotated : rotatedTree tree rot
+       ri : replacedRBTree key value (child-replaced key rot ) repl
+
+--   r (b , b)    inserting a node into black node does not change the black depth, but color may change
+--       → b (b , r ) ∨ b (r , b)
+--   b (b , b)    
+--       → b (b , r ) ∨ b (r , b)
+--   b (r , b)    inserting to right → b (r , r ) 
+--   b (r , b)    inserting to left may increse black depth, need rotation
+--      find b in left and move the b to the right (one down or two down)
+--
+rbi-case1 : {n : Level} {A : Set n} → {key d : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) ) 
+           → RBtreeInvariant parent 
+           → RBtreeInvariant repl 
+           → {left right : bt (Color ∧ A) } → parent ≡ node key ⟪ Black , value ⟫ left right
+           →    (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl  ) )
+             ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
+rbi-case1 {n} {A} {key} = {!!}
+
+rbi-case31 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) ) 
+           → RBtreeInvariant grand 
+           → RBtreeInvariant repl 
+           → {uncle left right : bt (Color ∧ A) } 
+           → grand  ≡ node kg ⟪ cg , vg ⟫ uncle parent
+           → parent ≡ node kp ⟪ Red , vp ⟫ left  right
+           → color uncle ≡ Red
+           →     (color left  ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) ) 
+              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  )) )
+rbi-case31 {n} {A} {key} = {!!}
+
+--
+-- case4 increase the black depth
+--
+rbi-case41 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) ) 
+           → RBtreeInvariant grand 
+           → RBtreeInvariant repl  
+           → {uncle left right : bt (Color ∧ A) } 
+           → grand  ≡ node kg ⟪ cg , vg ⟫ uncle parent
+           → parent ≡ node kp ⟪ Red , vp ⟫ left  right
+           → color uncle ≡ Black
+           →     (color left  ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right ))  )
+              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  ))  )
+rbi-case41 {n} {A} {key} = {!!}
+
+rbi-case51 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) ) 
+           → RBtreeInvariant grand 
+           → RBtreeInvariant repl  
+           → {uncle left right : bt (Color ∧ A) } 
+           → grand  ≡ node kg ⟪ cg , vg ⟫ uncle parent
+           → parent ≡ node kp ⟪ Red , vp ⟫ left  right
+           → color uncle ≡ Black
+           →     (color left  ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right ))  )
+              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  ))  )
+rbi-case51 {n} {A} {key} = {!!}
+
+--... | Black = record {
+--             d = ? ; od = RBI.od rbi ; rd = ? 
+--          ;  tree = ? ; rot = ? ; repl = ?
+--          ;  treerb = ? ; replrb = ?
+--          ;  d=rd = ? ; si = ? ; rotated = ? ; ri = ?
+--          ;  origti = RBI.origti rbi ; origrb = RBI.origrb rbi
+--       }
+--... | Red = ?
+
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
            →  (stack : List (bt A)) → stackInvariant key tree orig stack
            → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack
 stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl
-stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right x s-nil) = case2 (case1 refl)
-stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right {.tree} {.(node k2 v2 t5 (node k1 v1 t2 tree))} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.(node k2 v2 t5 (node k1 v1 t2 tree))} {t5} {k2} {v2} x₁ s-nil)) = case2 (case2 
+stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x s-nil) = case2 (case1 refl)
+stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right tree (node k2 v2 t5 (node k1 v1 t2 tree)) t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) (node k2 v2 t5 (node k1 v1 t2 tree)) t5 {k2} {v2} x₁ s-nil)) = case2 (case2 
     record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right {.tree} {.orig} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.orig} {t5} {k2} {v2} x₁ (s-right x₂ si))) = case2 (case2 
+stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2 
     record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right {.tree} {.orig} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.orig} {t5} {k2} {v2} x₁ (s-left x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ s-nil)) = case2 (case2
+stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ s-nil)) = case2 (case2
     record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ (s-right x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ (s-left x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left {_} {_} {t1} {k1} {v1} x s-nil) = case2 (case1 refl)
-stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ s-nil)) = case2 (case2
+stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left _ _ t1 {k1} {v1} x s-nil) = case2 (case1 refl)
+stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ s-nil)) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ (s-right x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ (s-left x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ s-nil)) = case2 (case2
+stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ s-nil)) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-right x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-left x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
 
+stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A }
+           →  {stack : List (bt A)} → stackInvariant key tree orig stack
+           →  stack ≡ orig ∷ [] → tree ≡ orig
+stackCase1 s-nil refl = refl
 
 PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) )
-           →  RBtreeInvariant orig d0 
+           →  RBtreeInvariant orig 
            →  (stack : List (bt (Color ∧ A)))  → (pg : PG (Color ∧ A) tree stack )
-           →  RBtreeInvariant tree ds ∧  RBtreeInvariant (PG.parent pg) dp ∧  RBtreeInvariant (PG.grand pg) dg 
+           →  RBtreeInvariant tree ∧  RBtreeInvariant (PG.parent pg) ∧  RBtreeInvariant (PG.grand pg) 
 PGtoRBinvariant = {!!}
 
-findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → {d d0 : ℕ}
-           →  RBtreeInvariant tree0 d0 
-           →  RBtreeInvariant tree d ∧ stackInvariant key tree tree0 stack  
-           → (next : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack
-                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
-findRBT = {!!}
+-- 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 
+--           → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) 
+--                 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
+--                 → {d1 : ℕ} → RBtreeInvariant tree1 
+--                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+--findRBT {_} {_} {A} {t} key tree0 leaf stack ti {d} rb0 exit = {!!}
+--findRBT {_} {_} {A} {t} key tree0 (node key₁ value left right) stack ti {d} rb0 exit with <-cmp key key₁
+--... | tri< a ¬b ¬c = {!!}
+--... | tri≈ ¬a b ¬c = {!!}
+--... | tri> ¬a ¬b c = {!!}
 
 rotateLeft : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
-     →  RBtreeInvariant orig d0 
-     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
-     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
-     → rotatedTree tree rot
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color} 
-        → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
-        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
-        → rotatedTree tr rot
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+     → (key : ℕ) → (value : A) 
+     → (orig tree : bt (Color ∧ A)) 
+     → (stack : List (bt (Color ∧ A))) 
+     → (r : RBI key value orig tree stack )
+     → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig current stack1 ) 
         → length stack1 < length stack  → t )
-     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
-        →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
-rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateLeft1 where
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  stack1 ≡ (orig ∷ [])
+        →  RBI key value orig repl stack1
+        → t ) → t
+rotateLeft {n} {m} {A} {t} key value = {!!} where
     rotateLeft1 : t
-    rotateLeft1 with stackToPG tree orig stack si
-    ... | case1 x = {!!}
+    rotateLeft1 with stackToPG {!!} {!!} {!!} {!!}
+    ... | case1 x = {!!} -- {!!} {!!} {!!} {!!} rr
     ... | case2 (case1 x) = {!!}
     ... | case2 (case2 pg) = {!!}
 
 rotateRight : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
-     →  RBtreeInvariant orig d0 
-     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
-     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
-     → rotatedTree tree rot
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color}  
-        → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
-        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
-        → rotatedTree tr rot
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+     → (key : ℕ) → (value : A) 
+     → (orig tree : bt (Color ∧ A)) 
+     → (stack : List (bt (Color ∧ A))) 
+     → (r : RBI key value orig tree stack )
+     → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig current stack1 ) 
         → length stack1 < length stack  → t )
-     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
-        →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
-rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateRight1 where
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  stack1 ≡ (orig ∷ [])
+        →  RBI key value orig repl stack1
+        → t ) → t
+rotateRight {n} {m} {A} {t} key value = {!!} where
     rotateRight1 : t
-    rotateRight1 with stackToPG tree orig stack si
+    rotateRight1 with stackToPG {!!} {!!} {!!} {!!}
     ... | case1 x = {!!}
     ... | case2 (case1 x) = {!!}
     ... | case2 (case2 pg) = {!!}
 
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
-     →  RBtreeInvariant orig d0 
-     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
-     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
-     → rotatedTree tree rot
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color}   
-        → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
-        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
-        → rotatedTree tr rot
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+     → (key : ℕ) → (value : A) 
+     → (orig tree : bt (Color ∧ A)) 
+     → (stack : List (bt (Color ∧ A))) 
+     → (r : RBI key value orig tree stack )
+     → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig tree1 stack1 ) 
         → length stack1 < length stack  → t )
-     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
-        →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
-insertCase5 {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = insertCase51 where
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  stack1 ≡ (orig ∷ [])
+        →  RBI key value orig repl stack1
+        → t ) → t
+insertCase5 {n} {m} {A} {t} key value = {!!} where
     insertCase51 : t
-    insertCase51 with stackToPG tree orig stack si
+    insertCase51 with stackToPG {!!} {!!} {!!} {!!}
     ... | case1 eq = {!!}
     ... | case2 (case1 eq ) = {!!}
     ... | case2 (case2 pg) with PG.pg pg
-    ... | s2-s1p2 x x₁ = rotateRight {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
+    ... | s2-s1p2 x x₁ = {!!} -- rotateRight {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
        -- x     : PG.parent pg ≡ node kp vp tree n1
        -- x₁    : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
-    ... | s2-1sp2 x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
-    ... | s2-s12p x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
-    ... | s2-1s2p x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
+    ... | s2-1sp2 x x₁ = {!!} -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
+    ... | s2-s12p x x₁ = {!!} -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
+    ... | s2-1s2p x x₁ = {!!} -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
     -- = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 
 
 
 -- if we have replacedNode on RBTree, we have RBtreeInvariant
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree repl : bt (Color ∧ A)) {d0 : ℕ}
-     →  RBtreeInvariant orig d0 
-     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
-     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tree) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color}   -- rotating case
-        → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
-        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
-        → rotatedTree tr rot
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+     → (key : ℕ) → (value : A) 
+     → (orig repl : bt (Color ∧ A)) 
+     → (stack : List (bt (Color ∧ A))) 
+     → (r : RBI key value orig repl stack )
+     → (next : (repl1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig repl1 stack1 ) 
         → length stack1 < length stack  → t )
-     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
-        →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
-replaceRBP {n} {m} {A} {t} key value orig tree repl rbio rbit rbir stack si ri next exit = insertCase1 where
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  stack1 ≡ (orig ∷ [])
+        →  RBI key value orig repl stack1
+        → t ) → t
+replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit = insertCase1 where
     insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 
       → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
       → (pg : ParentGrand tree parent uncle grand ) → t
@@ -757,35 +900,52 @@
     insertCase2 tree leaf uncle grand stack si (s2-1sp2 () x₁) 
     insertCase2 tree leaf uncle grand stack si (s2-s12p () x₁) 
     insertCase2 tree leaf uncle grand stack si (s2-1s2p () x₁) 
-    insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+    insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = {!!} -- next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
     insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = {!!}
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = 
-          insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = {!!} -- next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = {!!}
+          -- insertCase5 key value orig tree {!!} rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
       -- tree is left of parent, parent is left of grand
       --  node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
       --  grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = 
-          rotateLeft key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} 
-             (λ a b c d e f h i j k l m  → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = {!!}
+          -- rotateLeft key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} 
+          --   (λ a b c d e f h i j k l m  → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
       -- tree is right of parent, parent is left of grand  rotateLeft
       --  node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
       --  grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = 
-          rotateRight key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} 
-             (λ a b c d e f h i j k l m  → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = {!!}
+          -- rotateRight key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} 
+          --    (λ a b c d e f h i j k l m  → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
       -- tree is left of parent, parent is right of grand, rotateRight
       -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
       --  grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = 
-          insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = {!!}
+          -- insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
       -- tree is right of parent, parent is right of grand
       -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
-    insertCase1 with stackToPG tree orig stack si
-    ... | case1 eq = {!!}
-    ... | case2 (case1 eq ) = {!!}
-    ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 
+    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 = {!!}
+    -- exit rot repl rbir ? ? 
+    ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 
 
 
+
Binary file logic.agdai has changed