--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/BTree.agda	Sun Aug 18 20:02:03 2024 +0900
@@ -0,0 +1,1157 @@
+{-# OPTIONS --cubical-compatible --allow-unsolved-metas  #-}
+--  {-# OPTIONS --cubical-compatible --safe #-}
+
+module BTree where
+
+open import Level hiding (suc ; zero ; _⊔_ )
+
+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.Empty
+open import Data.List
+open import Data.Product
+
+open import Data.Maybe.Properties
+open import Data.List.Properties
+
+open import Function as F hiding (const)
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import logic
+open import nat
+
+
+--
+--
+--  no children , having left node , having right node , having both
+--
+data bt {n : Level} (A : Set n) : Set n where
+  leaf : bt A
+  node :  (key : ℕ) → (value : A) →
+    (left : bt A ) → (right : bt A ) → bt A
+
+node-key : {n : Level} {A : Set n} → bt A → Maybe ℕ
+node-key (node key _ _ _) = just key
+node-key _ = nothing
+
+node-value : {n : Level} {A : Set n} → bt A → Maybe A
+node-value (node _ value _ _) = just value
+node-value _ = nothing
+
+bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
+bt-depth leaf = 0
+bt-depth (node key value t t₁) = suc (bt-depth t  ⊔ bt-depth t₁ )
+
+bt-ne : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ : bt A} → ¬ ( leaf ≡ node key value t t₁ )
+bt-ne {n} {A} {key} {value} {t} {t₁} ()
+
+open import Data.Unit hiding ( _≟_ ) -- ;  _≤?_ ; _≤_)
+
+tr< : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
+tr< {_} {A} key leaf = ⊤
+tr< {_} {A} key (node key₁ value tr tr₁) = (key₁ < key ) ∧ tr< key tr  ∧  tr< key tr₁
+
+tr> : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
+tr> {_} {A} key leaf = ⊤
+tr> {_} {A} key (node key₁ value tr tr₁) = (key < key₁ ) ∧ tr> key tr  ∧  tr> key tr₁
+
+--
+--
+data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
+    t-leaf : treeInvariant leaf
+    t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf)
+    t-right : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁
+       → tr> key t₁
+       → tr> key t₂
+       → treeInvariant (node key₁ value₁ t₁ t₂)
+       → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
+    t-left  : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁
+       → tr< key₁ t₁
+       → tr< key₁ t₂
+       → treeInvariant (node key value t₁ t₂)
+       → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf )
+    t-node  : (key key₁ key₂ : ℕ) → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → key < key₁ → key₁ < key₂
+       → tr< key₁ t₁
+       → tr< key₁ t₂
+       → tr> key₁ t₃
+       → tr> key₁ t₄
+       → treeInvariant (node key value t₁ t₂)
+       → treeInvariant (node key₂ value₂ t₃ t₄)
+       → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
+
+--
+--  stack always contains original top at end (path of the tree)
+--
+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)}
+        → 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)}
+        → 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
+    r-leaf : replacedTree key value leaf (node key value leaf leaf)
+    r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
+    r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
+          → k < key →  replacedTree key value t2 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t)
+    r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
+          → key < k →  replacedTree key value t1 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t t2)
+
+add< : { i : ℕ } (j : ℕ ) → i < suc i + j
+add<  {i} j = begin
+        suc i ≤⟨ m≤m+n (suc i) j ⟩
+        suc i + j ∎  where open ≤-Reasoning
+
+treeTest1  : bt ℕ
+treeTest1  =  node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
+treeTest2  : bt ℕ
+treeTest2  =  node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
+
+treeInvariantTest1  : treeInvariant treeTest1
+treeInvariantTest1  = t-right _ _ (m≤m+n _ 2)
+    ⟪ add< _ , ⟪ ⟪ add< _ , _ ⟫ , _ ⟫ ⟫
+    ⟪ add< _ , ⟪ _ , _ ⟫ ⟫ (t-node _ _ _ (add< 0) (add< 1) ⟪ add< _ , ⟪ _ , _ ⟫ ⟫  _ _ _ (t-left _ _ (add< 0) _ _ (t-single 1 7)) (t-single 5 5) )
+
+stack-top :  {n : Level} {A : Set n} (stack  : List (bt A)) → Maybe (bt A)
+stack-top [] = nothing
+stack-top (x ∷ s) = just x
+
+stack-last :  {n : Level} {A : Set n} (stack  : List (bt A)) → Maybe (bt A)
+stack-last [] = nothing
+stack-last (x ∷ []) = just x
+stack-last (x ∷ s) = stack-last s
+
+stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
+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-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 {n} {A} {key} {tree} {tree0} {tree1} {stack} si = lem00 tree tree0 tree1 _ (tree1 ∷ stack) refl si where
+    lem00 : (tree tree0 tree1 : bt A) → (stack  stack1 : List (bt A)) → tree1 ∷ stack ≡ stack1  →  stackInvariant key tree tree0 stack1 → tree1 ≡ tree
+    lem00 tree .tree tree1 stack .(tree ∷ []) eq s-nil = ∷-injectiveˡ eq
+    lem00 tree tree0 tree1 stack .(tree ∷ _) eq (s-right .tree .tree0 tree₁ x si) = ∷-injectiveˡ eq
+    lem00 tree tree0 tree1 stack .(tree ∷ _) eq (s-left .tree .tree0 tree₁ x si) = ∷-injectiveˡ eq
+
+si-property2 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → (stack  : List (bt A)) →  stackInvariant key tree tree0 (tree1 ∷ stack)
+   → ¬ ( just leaf ≡ stack-last stack )
+si-property2 {n} {A} {key} {tree} {tree0} {tree1} [] si ()
+si-property2 {n} {A} {key} {tree} {tree0} {tree1} (x ∷ []) si eq with just-injective eq
+... | refl = lem00 (tree1 ∷ leaf ∷ [])  refl si  where
+    lem00 : (t : List (bt A)) → (tree1 ∷ leaf ∷ []) ≡ t → stackInvariant key tree tree0 t → ⊥
+    lem00 .(tree ∷ []) () s-nil
+    lem00 (tree ∷ _) () (s-right .tree .(node _ _ tree₁ tree) tree₁ x s-nil)
+    lem00 (tree ∷ _) () (s-right .tree .tree0 tree₁ x (s-right .(node _ _ tree₁ tree) .tree0 tree₂ x₁ si2))
+    lem00 (tree ∷ _) () (s-right .tree .tree0 tree₁ x (s-left .(node _ _ tree₁ tree) .tree0 tree₂ x₁ si2))
+    lem00 (tree₁ ∷ _) () (s-left .tree₁ .(node _ _ tree₁ tree) tree x s-nil)
+    lem00 (tree₁ ∷ _) () (s-left .tree₁ .tree0 tree x (s-right .(node _ _ tree₁ tree) .tree0 tree₂ x₁ si2))
+    lem00 (tree₁ ∷ _) () (s-left .tree₁ .tree0 tree x (s-left .(node _ _ tree₁ tree) .tree0 tree₂ x₁ si2))
+si-property2 {n} {A} {key} {tree} {tree0} {tree1} (x ∷ x₁ ∷ stack) si = lem00 (tree1 ∷ x ∷ x₁ ∷ stack) refl si where
+    lem00 : (t : List (bt A)) → (tree1 ∷ x ∷ x₁ ∷ stack) ≡ t → stackInvariant key tree tree0 t → ¬ just leaf ≡ stack-last (x₁ ∷ stack)
+    lem00 .(tree ∷ []) () s-nil
+    lem00 (tree ∷ []) () (s-right .tree .tree0 tree₁ x si)
+    lem00 (tree ∷ x₁ ∷ st) eq (s-right .tree .tree0 tree₁ x si) eq1 = si-property2 st si
+         (subst (λ k → just leaf ≡ stack-last k ) (∷-injectiveʳ (∷-injectiveʳ eq)) eq1 )
+    lem00 (tree ∷ []) () (s-left .tree .tree0 tree₁ x si)
+    lem00 (tree₁ ∷ x₁ ∷  st) eq (s-left .tree₁ .tree0 tree x si) eq1 = si-property2 st si
+         (subst (λ k → just leaf ≡ stack-last k ) (∷-injectiveʳ (∷-injectiveʳ eq)) eq1 )
+
+
+-- We cannot avoid warning: -W[no]UnsupportedIndexedMatcin tree-inject
+-- open import Function.Base using (_∋_; id; _∘_; _∘′_)
+-- just-injective1 : {n : Level } {A : Set n} {x y : A } → (Maybe A ∋ just x) ≡ just y → x ≡ y
+-- just-injective1 refl = refl
+
+node-left : {n : Level} {A : Set n} → bt A → Maybe (bt A)
+node-left (node _ _ left _) = just left
+node-left _ = nothing
+
+node-right : {n : Level} {A : Set n} → bt A → Maybe (bt A)
+node-right (node _ _ _ right) = just right
+node-right _ = nothing
+
+--   lem00 = just-injective (cong node-key eq)
+
+tree-injective-key : {n : Level} {A : Set n}
+    → (tr0 tr1 : bt A) → tr0 ≡ tr1 → node-key tr0 ≡ node-key tr1
+tree-injective-key {n} {A} tr0 tr1 eq = cong node-key eq
+
+ti-property2 :  {n : Level} {A : Set n} {key : ℕ} {value : A} {tree1 left right : bt A}
+   → tree1 ≡ node key value left right
+   → left ≡ right
+   → ( ¬ left  ≡ leaf ) ∨ ( ¬ right ≡ leaf )
+   → ¬ treeInvariant tree1
+ti-property2 {n} {A} {key} {value} {leaf} {left} {right} () eq1 x ti
+ti-property2 {n} {A} {key} {value} {node key₁ value₁ leaf t₁} {left} {right} eq eq1 (case1 eq2) _
+    = ⊥-elim ( eq2 (just-injective ( cong node-left (sym eq)  )))
+ti-property2 {n} {A} {key} {value} {node key₁ value₁ leaf t₁} {left} {right} eq eq1 (case2 eq2) _
+    = ⊥-elim ( eq2 (just-injective (trans (cong just (sym eq1)) ( cong node-left (sym eq)   ) ) ))
+ti-property2 {n} {A} {key} {value} {node key₁ value₁ (node key₂ value₂ t t₂) leaf} {left} {right} eq eq1 (case1 eq2) _
+    = ⊥-elim ( eq2 (just-injective (trans (cong just eq1) ( cong node-right (sym eq)   ) ) ))
+ti-property2 {n} {A} {key} {value} {node key₁ value₁ (node key₂ value₂ t t₂) leaf} {left} {right} eq eq1 (case2 eq2) _
+    = ⊥-elim ( eq2 (just-injective ( cong node-right (sym eq)  )))
+ti-property2 {n} {A} {key} {value} {node key₂ value₂ (node key₁ value₁ t₁ t₂) (node key₃ value₃ t₃ t₄)} {left} {right} eq eq1 eq2 ti
+     = ⊥-elim ( nat-≡< lem00 (lem03 _ _ _ refl lem01 lem02 ti) ) where
+   lem01 : node key₁ value₁ t₁ t₂ ≡ left
+   lem01 = just-injective ( cong node-left eq )
+   lem02 : node key₃ value₃ t₃ t₄ ≡ right
+   lem02 = just-injective ( cong node-right eq )
+   lem00 : key₁ ≡ key₃
+   lem00 = begin
+      key₁ ≡⟨ just-injective ( begin
+         just key₁  ≡⟨ cong node-key lem01 ⟩
+         node-key left ≡⟨ cong node-key eq1 ⟩
+         node-key right ≡⟨ cong node-key (sym lem02) ⟩
+         just key₃ ∎ ) ⟩
+      key₃ ∎ where open ≡-Reasoning
+   lem03 :  (key₁ key₃ : ℕ) → (tr : bt A) → tr ≡ node key₂ value₂ (node key₁ value₁ t₁ t₂) (node key₃ value₃ t₃ t₄)
+      → node key₁ value₁ t₁ t₂ ≡ left
+      → node key₃ value₃ t₃ t₄ ≡ right
+      → treeInvariant tr → key₁ < key₃
+   lem03 _ _ .leaf () _ _ t-leaf
+   lem03 _ _ .(node _ _ leaf leaf) () _ _ (t-single _ _)
+   lem03 _ _ .(node _ _ (node _ _ _ _) leaf) () _ _ (t-left _ _ _ _ _ _)
+   lem03 _ _ .(node _ _ leaf (node _ _ _ _)) () _ _ (t-right _ _ _ _ _ _)
+   lem03 key₁ key₃ (node key _ (node _ _ _ _) (node _ _ _ _)) eq3 el er (t-node key₄ key₅ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = lem04 where
+       lem04 : key₁ < key₃
+       lem04 = begin
+         suc key₁ ≡⟨ cong suc ( just-injective (cong node-key (just-injective (cong node-left (sym eq3)) ) ) ) ⟩
+         suc key₄ ≤⟨ <-trans x x₁ ⟩
+         key₂ ≡⟨ just-injective (cong node-key (just-injective (cong node-right eq3) ) )  ⟩
+         key₃ ∎ where open ≤-Reasoning
+
+si-property-< :  {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack  : List (bt A)}
+   → ¬ ( tree ≡ leaf )
+   → treeInvariant (node kp value₂ tree  tree₃ )
+   → stackInvariant key tree orig (tree ∷ node kp value₂ tree  tree₃ ∷ stack)
+   → key < kp
+si-property-< {n} {A} {key} {kp} {value₂} {tree} {orig} {tree₃} {stack} ne ti si =
+       lem00 (node kp value₂ tree  tree₃ ) (tree ∷ node kp value₂ tree  tree₃ ∷ stack) refl refl ti si where
+    lem00 : (tree1 : bt A) → (st : List (bt A)) →  (tree1 ≡ (node kp value₂ tree  tree₃ )) → (st ≡ tree ∷ node kp value₂ tree  tree₃ ∷ stack)
+       → treeInvariant tree1 → stackInvariant key tree orig st → key < kp
+    lem00 tree1 .(tree ∷ []) teq () ti s-nil
+    lem00 tree1 .(tree ∷ node key₁ v1 tree₁ tree ∷ []) teq seq ti₁ (s-right .tree .(node key₁ v1 tree₁ tree) tree₁ {key₁} {v1} x s-nil) = lem01 where
+        lem02 :  node key₁ v1 tree₁ tree  ≡ node kp value₂ tree tree₃
+        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
+        lem03 : tree₁ ≡ tree
+        lem03 = just-injective (cong node-left lem02)
+        lem01 : key < kp
+        lem01 = ⊥-elim ( ti-property2 (sym lem02) lem03 (case2 ne) ti )
+    lem00 tree1 .(tree ∷ node key₁ v1 tree₁ tree ∷ _) teq seq ti₁ (s-right .tree .orig tree₁ {key₁} {v1} x (s-right .(node _ _ tree₁ tree) .orig tree₂ {key₂} {v2} x₁ si)) = lem01 where
+        lem02 :  node key₁ v1 tree₁ tree  ≡ node kp value₂ tree tree₃
+        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
+        lem03 : tree₁ ≡ tree
+        lem03 = just-injective (cong node-left lem02)
+        lem01 : key < kp
+        lem01 = ⊥-elim ( ti-property2 (sym lem02) lem03 (case2 ne) ti )
+    lem00 tree1 (tree₂ ∷ node key₁ v1 tree₁ tree₂ ∷ _) teq seq ti₁ (s-right .tree₂ .orig tree₁ {key₁} {v1} x (s-left .(node _ _ tree₁ tree₂) .orig tree x₁ si)) = lem01 where
+        lem02 :  node key₁ v1 tree₁ tree₂ ≡ node kp value₂ tree₂ tree₃
+        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
+        lem03 : tree₁ ≡ tree₂
+        lem03 = just-injective (cong node-left lem02 )
+        lem01 : key < kp
+        lem01 = ⊥-elim ( ti-property2 (sym lem02) lem03 (case2 ne) ti )
+    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-left .tree₁ .(node _ _ tree₁ tree) tree {key₁} {v1} x s-nil) = subst( λ k → key < k ) lem03 x where
+        lem03 : key₁ ≡ kp
+        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
+    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-left .tree₁ .orig tree {key₁} {v1} x (s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) = subst( λ k → key < k ) lem03 x where
+        lem03 : key₁ ≡ kp
+        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
+    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-left .tree₁ .orig tree {key₁} {v1} x (s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) = subst( λ k → key < k ) lem03 x where
+        lem03 : key₁ ≡ kp
+        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
+
+si-property-> :  {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack  : List (bt A)}
+   → ¬ ( tree ≡ leaf )
+   → treeInvariant (node kp value₂ tree₃  tree )
+   → stackInvariant key tree orig (tree ∷ node kp value₂ tree₃  tree ∷ stack)
+   → kp < key
+si-property-> {n} {A} {key} {kp} {value₂} {tree} {orig} {tree₃} {stack} ne ti si =
+       lem00 (node kp value₂ tree₃  tree ) (tree ∷ node kp value₂ tree₃  tree ∷ stack) refl refl ti si where
+    lem00 : (tree1 : bt A) → (st : List (bt A)) →  (tree1 ≡ (node kp value₂ tree₃  tree )) → (st ≡ tree ∷ node kp value₂ tree₃  tree ∷ stack)
+       → treeInvariant tree1 → stackInvariant key tree orig st → kp < key
+    lem00 tree1 .(tree ∷ []) teq () ti s-nil
+    lem00 tree1 .(tree ∷ node key₁ v1 tree tree₁ ∷ []) teq seq ti₁ (s-left .tree .(node key₁ v1 tree tree₁) tree₁ {key₁} {v1} x s-nil) = lem01 where
+        lem02 :  node key₁ v1 tree tree₁  ≡ node kp value₂ tree₃ tree
+        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
+        lem03 : tree₁ ≡ tree
+        lem03 = just-injective (cong node-right lem02)
+        lem01 : kp < key
+        lem01 = ⊥-elim ( ti-property2 (sym lem02) (sym lem03) (case1 ne) ti )
+    lem00 tree1 .(tree ∷ node key₁ v1 tree tree₁ ∷ _) teq seq ti₁ (s-left .tree .orig tree₁ {key₁} {v1} x (s-left .(node _ _ tree tree₁) .orig tree₂ {key₂} {v2} x₁ si)) = lem01 where
+        lem02 :  node key₁ v1 tree tree₁  ≡ node kp value₂ tree₃ tree
+        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
+        lem03 : tree₁ ≡ tree
+        lem03 = just-injective (cong node-right lem02)
+        lem01 : kp < key
+        lem01 = ⊥-elim ( ti-property2 (sym lem02) (sym lem03) (case1 ne) ti )
+    lem00 tree1 (tree₂ ∷ node key₁ v1 tree₂ tree₁ ∷ _) teq seq ti₁ (s-left .tree₂ .orig tree₁ {key₁} {v1} x (s-right .(node _ _ tree₂ tree₁) .orig tree x₁ si)) = lem01 where
+        lem02 :  node key₁ v1 tree₂ tree₁  ≡ node kp value₂ tree₃ tree₂
+        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
+        lem03 : tree₁ ≡ tree₂
+        lem03 = just-injective (cong node-right lem02)
+        lem01 : kp < key
+        lem01 = ⊥-elim ( ti-property2 (sym lem02) (sym lem03) (case1 ne) ti )
+    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-right .tree₁ .(node _ _ tree tree₁) tree {key₁} {v1} x s-nil) = subst( λ k → k < key ) lem03 x where
+        lem03 : key₁ ≡ kp
+        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
+    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-right .tree₁ .orig tree {key₁} {v1} x (s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) = subst( λ k → k < key ) lem03 x where
+        lem03 : key₁ ≡ kp
+        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
+    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-right .tree₁ .orig tree {key₁} {v1} x (s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) = subst( λ k → k < key ) lem03 x where
+        lem03 : key₁ ≡ kp
+        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
+
+
+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 {n} {A} key tree .tree .(tree ∷ []) s-nil = refl
+si-property-last {n} {A} key tree tree0 (tree ∷ []) (s-right .tree .tree0 tree₁ x si) = ⊥-elim ( si-property0 si refl )
+si-property-last {n} {A} key tree tree0 (tree ∷ x₁ ∷ st) (s-right .tree .tree0 tree₁ x si) = 
+   si-property-last key _ tree0 (x₁ ∷ st)  si
+si-property-last {n} {A} key tree tree0 (tree ∷ []) (s-left .tree .tree0 tree₁ x si) = ⊥-elim ( si-property0 si refl )
+si-property-last {n} {A} key tree tree0 (tree ∷ x₁ ∷ st) (s-left .tree .tree0 tree₁ x si) = 
+   si-property-last key _ tree0 (x₁ ∷ st)  si
+
+si-property-pne :  {n : Level} {A : Set n}  {key key₁ : ℕ} {value₁ : A} (tree orig : bt A) → {left right x : bt A} → (stack  : List (bt A)) {rest : List (bt A)}
+    → stack ≡ x ∷ node key₁ value₁ left right ∷ rest
+    → stackInvariant key tree orig stack
+    → ¬ ( key ≡ key₁ )
+si-property-pne {_} {_} {key} {key₁} {value₁} tree orig {left} {right} (tree ∷ tree1 ∷ st) seq (s-right .tree .orig tree₁ {key₂} {v₂} x si) eq 
+    = ⊥-elim ( nat-≡< lem00 x ) where
+      lem01 : tree1 ≡ node key₂ v₂ tree₁ tree 
+      lem01 = si-property1 si
+      lem02 : node key₁ value₁ left right ≡ node key₂ v₂ tree₁ tree 
+      lem02 = trans ( ∷-injectiveˡ (∷-injectiveʳ (sym seq) ) ) lem01
+      lem00 : key₂ ≡ key
+      lem00 = trans (just-injective (cong node-key (sym lem02))) (sym eq)
+si-property-pne {_} {_} {key} {key₁} {value₁} tree orig {left} {right} (tree ∷ tree1 ∷ st) seq (s-left tree orig tree₁ {key₂} {v₂} x si) eq 
+    = ⊥-elim ( nat-≡< (sym lem00) x ) where
+      lem01 : tree1 ≡ node key₂ v₂ tree tree₁
+      lem01 = si-property1 si
+      lem02 : node key₁ value₁ left right ≡ node key₂ v₂ tree tree₁
+      lem02 = trans ( ∷-injectiveˡ (∷-injectiveʳ (sym seq) ) ) lem01
+      lem00 : key₂ ≡ key
+      lem00 = trans (just-injective (cong node-key (sym  lem02))) (sym eq)
+si-property-pne {_} {_} {key} {key₁} {value₁} tree .tree {left} {right} .(tree ∷ []) () s-nil eq
+
+
+-- si-property-parent-node :  {n : Level} {A : Set n}  {key : ℕ}  (tree orig : bt A) {x : bt A}
+--     → (stack  : List (bt A)) {rest : List (bt A)}
+--     → stackInvariant key tree orig stack
+--     → ¬ ( stack ≡ x ∷ leaf ∷ rest )
+-- si-property-parent-node {n} {A} tree orig = ?
+
+
+rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
+rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
+rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
+rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = λ ()
+rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = λ ()
+
+rt-property-leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {repl : bt A} → replacedTree key value leaf repl → repl ≡ node key value leaf leaf
+rt-property-leaf {n} {A} {key} {value} {repl} rt = lem00 leaf refl rt where
+   lem00 : (tree : bt A) → tree ≡ leaf → replacedTree key value tree repl → repl ≡ node key value leaf leaf
+   lem00 leaf eq r-leaf = refl
+   lem00 .(node key _ _ _) () r-node
+   lem00 .(node _ _ _ _) () (r-right x rt)
+   lem00 .(node _ _ _ _) () (r-left x rt)
+
+rt-property-¬leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {tree : bt A} → ¬ replacedTree key value tree leaf
+rt-property-¬leaf ()
+
+rt-property-key : {n : Level} {A : Set n} {key key₂ key₃ : ℕ} {value value₂ value₃ : A} {left left₁ right₂ right₃ : bt A}
+    →  replacedTree key value (node key₂ value₂ left right₂) (node key₃ value₃ left₁ right₃) → key₂ ≡ key₃
+rt-property-key {n} {A} {key} {key₂} {key₃} {value} {value₂} {value₃} {left} {left₁} {right₂} {right₃} rt 
+      = lem00 (node key₂ value₂ left right₂) (node key₃ value₃ left₁ right₃) refl refl rt where
+    lem00 : (tree tree1 : bt A) → tree ≡ node key₂ value₂ left right₂ → tree1 ≡  node key₃ value₃ left₁ right₃ → replacedTree key value tree tree1 → key₂ ≡ key₃
+    lem00 _ _ () eq2 r-leaf
+    lem00 _ _ eq1 eq2 r-node = trans (just-injective (cong node-key (sym eq1))) (just-injective (cong node-key eq2))
+    lem00 _ _ eq1 eq2 (r-right x rt1) = trans (just-injective (cong node-key (sym eq1))) (just-injective (cong node-key eq2))
+    lem00 _ _ eq1 eq2 (r-left x rt1) = trans (just-injective (cong node-key (sym eq1))) (just-injective (cong node-key eq2))
+
+
+open _∧_
+
+
+depth-1< : {i j : ℕ} →   suc i ≤ suc (i Data.Nat.⊔ j )
+depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
+
+depth-2< : {i j : ℕ} →   suc i ≤ suc (j Data.Nat.⊔ i )
+depth-2< {i} {j} = s≤s (m≤n⊔m j i)
+
+depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
+depth-3< {zero} = s≤s ( z≤n )
+depth-3< {suc i} = s≤s (depth-3< {i} )
+
+
+treeLeftDown  : {n : Level} {A : Set n} {k : ℕ} {v1 : A}  → (tree tree₁ : bt A )
+      → treeInvariant (node k v1 tree tree₁)
+      →      treeInvariant tree
+treeLeftDown {n} {A} {k} {v1} tree tree₁ ti = lem00 (node k v1 tree tree₁) refl ti  where
+    lem00 : ( tr : bt A ) → tr ≡ node k v1 tree tree₁ → treeInvariant tr → treeInvariant tree
+    lem00 .leaf () t-leaf
+    lem00 .(node key value leaf leaf) eq (t-single key value) = subst (λ k → treeInvariant k ) (just-injective (cong node-left eq)) t-leaf
+    lem00 .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ x x₁ x₂ ti) = subst (λ k → treeInvariant k ) (just-injective (cong node-left eq)) t-leaf
+    lem00 .(node key₁ _ (node key _ _ _) leaf) eq (t-left key key₁ x x₁ x₂ ti) = subst (λ k → treeInvariant k ) (just-injective (cong node-left eq)) ti
+    lem00 .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) eq (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = subst (λ k → treeInvariant k ) (just-injective (cong node-left eq)) ti
+
+treeRightDown  : {n : Level} {A : Set n} {k : ℕ} {v1 : A}  → (tree tree₁ : bt A )
+      → treeInvariant (node k v1 tree tree₁)
+      →      treeInvariant tree₁
+treeRightDown {n} {A} {k} {v1} tree tree₁ ti = lem00 (node k v1 tree tree₁) refl ti  where
+    lem00 : ( tr : bt A ) → tr ≡ node k v1 tree tree₁ → treeInvariant tr → treeInvariant tree₁
+    lem00 .leaf () t-leaf
+    lem00 .(node key value leaf leaf) eq (t-single key value) = subst (λ k → treeInvariant k ) (just-injective (cong node-right eq)) t-leaf
+    lem00 .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ x x₁ x₂ ti) = subst (λ k → treeInvariant k ) (just-injective (cong node-right eq)) ti
+    lem00 .(node key₁ _ (node key _ _ _) leaf) eq (t-left key key₁ x x₁ x₂ ti) = subst (λ k → treeInvariant k ) (just-injective (cong node-right eq)) t-leaf
+    lem00 .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) eq (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = subst (λ k → treeInvariant k ) (just-injective (cong node-right eq)) ti₁
+
+
+ti-property1 :  {n : Level} {A : Set n} {key₁ : ℕ} {value₂ : A} {left right : bt A} → treeInvariant (node key₁ value₂  left right ) →   tr< key₁ left ∧  tr> key₁ right
+ti-property1 {n} {A} {key₁} {value₂} {left} {right} ti = lem00 key₁ (node key₁ value₂ left right) refl ti where
+    lem00 : (key₁ : ℕ) → ( tree : bt A ) → tree ≡ node key₁ value₂ left right → treeInvariant tree → tr< key₁ left ∧  tr> key₁ right
+    lem00 - .leaf () t-leaf
+    lem00 key₁ .(node key value leaf leaf) eq (t-single key value) = subst₂ (λ j k → tr< key₁ j ∧ tr> key₁ k ) lem01 lem02 ⟪ tt , tt ⟫ where
+         lem01 : leaf ≡ left
+         lem01 = just-injective (cong node-left eq)
+         lem02 : leaf ≡ right
+         lem02 = just-injective (cong node-right eq)
+    lem00 key₂ .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ {value} {value₁} {t₁} {t₂} x x₁ x₂ ti) 
+         = subst₂ (λ j k → tr< key₂ j ∧ tr> key₂ k ) lem01 lem02 ⟪ tt , ⟪ subst (λ k → k < key₁) lem04 x , 
+              ⟪ subst (λ k → tr> k t₁) lem04 x₁ , subst (λ k → tr> k t₂) lem04 x₂ ⟫  ⟫ ⟫ where
+         lem01 : leaf ≡ left
+         lem01 = just-injective (cong node-left eq)
+         lem02 : node key₁ value₁ t₁ t₂ ≡ right
+         lem02 = just-injective (cong node-right eq)
+         lem04 : key ≡ key₂
+         lem04 = just-injective (cong node-key eq)
+    lem00 key₂ .(node key₁ _ (node key _ _ _) leaf) eq (t-left key key₁ {value} {value₁} {t₁} {t₂} x x₁ x₂ ti) 
+         = subst₂ (λ j k → tr< key₂ j ∧ tr> key₂ k ) lem02 lem01 ⟪ ⟪ subst (λ k → key < k) lem04 x , 
+              ⟪ subst (λ k → tr< k t₁) lem04 x₁  , subst (λ k → tr< k t₂) lem04 x₂  ⟫  ⟫ , tt ⟫ where
+         lem01 : leaf ≡ right
+         lem01 = just-injective (cong node-right eq)
+         lem02 : node key value t₁ t₂ ≡ left
+         lem02 = just-injective (cong node-left eq)
+         lem04 : key₁ ≡ key₂
+         lem04 = just-injective (cong node-key eq)
+    lem00 key₂ .(node key₁ _ (node key _ _ _) (node key₃ _ _ _)) eq (t-node key key₁ key₃ {value} {value₁} {value₂} 
+      {t₁} {t₂} {t₃} {t₄} x x₁ x₂ x₃ x₄ x₅ ti ti₁) 
+        = subst₂ (λ j k → tr< key₂ j ∧ tr> key₂ k ) lem01 lem02 ⟪ ⟪ subst (λ k → key < k) lem04 x , 
+             ⟪ subst (λ k → tr< k t₁) lem04 x₂ , subst (λ k → tr< k t₂) lem04 x₃ ⟫ ⟫   
+           , ⟪ subst (λ k → k < key₃) lem04 x₁  , ⟪  subst (λ k → tr> k t₃) lem04 x₄   , subst (λ k → tr> k t₄) lem04 x₅  ⟫  ⟫ ⟫ where
+         lem01 : node key value t₁ t₂  ≡ left
+         lem01 = just-injective (cong node-left eq)
+         lem02 : node key₃ value₂ t₃ t₄  ≡ right
+         lem02 = just-injective (cong node-right eq)
+         lem04 : key₁ ≡ key₂
+         lem04 = just-injective (cong node-key eq)
+
+
+
+
+findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
+           →  treeInvariant tree ∧ stackInvariant key tree tree0 stack
+           → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
+                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl)
+findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
+findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
+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 [] si = ⊥-elim ( si-property0 si refl )
+   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 {n} {A} {t} {t₁} k v1 value ti = lem00 (node k v1 t t₁) refl ti where
+   lem00 : (tree : bt A) → tree ≡ node k v1 t t₁ → treeInvariant tree → treeInvariant (node k value t t₁)
+   lem00 _ () t-leaf
+   lem00 .(node key v1 leaf leaf) eq (t-single key v1) = subst₂ (λ j k₁ → treeInvariant (node k value j k₁)) lem01 lem02 (t-single k value) where
+       lem01 : leaf ≡ t
+       lem01 = just-injective (cong node-left eq)
+       lem02 : leaf ≡ t₁
+       lem02 = just-injective (cong node-right eq)
+   lem00 .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ {value} {value₁} {t₁} {t₃} x x₁ x₂ ti) 
+      = subst₂ (λ j k₁ → treeInvariant (node _ _ j k₁)) lem01 lem02 (t-right _ _ (subst (λ j → j < key₁) lem03 x)  
+            (subst (λ j → tr> j t₁ ) lem03 x₁) (subst (λ j → tr> j t₃ ) lem03 x₂) ti) where
+       lem01 : leaf ≡ t
+       lem01 = just-injective (cong node-left eq)
+       lem02 : node key₁ value₁ t₁ t₃ ≡ _
+       lem02 = just-injective (cong node-right eq)
+       lem03 : key ≡ k
+       lem03 = just-injective (cong node-key eq)
+   lem00 .(node key₁ _ (node key _ _ _) leaf) eq (t-left key key₁  {value} {value₁} {t₁} {t₃} x x₁ x₂ ti) 
+      = subst₂ (λ j k₁ → treeInvariant (node _ _ j k₁)) lem02 lem01 (t-left _ _ (subst (λ j → key < j) lem03 x)  
+            (subst (λ j → tr< j t₁ ) lem03 x₁) (subst (λ j → tr< j t₃ ) lem03 x₂) ti) where
+       lem01 : leaf ≡ _
+       lem01 = just-injective (cong node-right eq)
+       lem02 : node key value t₁ t₃ ≡ _
+       lem02 = just-injective (cong node-left eq)
+       lem03 : key₁ ≡ k
+       lem03 = just-injective (cong node-key eq)
+   lem00 .(node key₁ _ (node key _ _ _) (node key₃ _ _ _)) eq (t-node key key₁ key₃  {value} {value₁} {value₂} 
+          {t₁} {t₂} {t₃} {t₄}  x x₁ x₂ x₃ x₄ x₅ ti ti₁) 
+      = subst₂ (λ j k₁ → treeInvariant (node _ _ j k₁)) lem01 lem02 (t-node _ _ _ (subst (λ j → key < j) lem04 x)  (subst (λ j → j < key₃)  lem04 x₁) 
+          (subst (λ j → tr< j t₁ ) lem04 x₂ ) 
+          (subst (λ j → tr< j _ ) lem04 x₃ ) 
+          (subst (λ j → tr> j _ ) lem04 x₄ ) 
+          (subst (λ j → tr> j _ ) lem04 x₅ ) 
+             ti ti₁ ) where
+       lem01 : node key value t₁ t₂  ≡ _
+       lem01 = just-injective (cong node-left eq)
+       lem02 : node _ value₂ t₃ t₄  ≡ _
+       lem02 = just-injective (cong node-right eq)
+       lem04 : key₁ ≡ _
+       lem04 = just-injective (cong node-key eq)
+
+open import Relation.Binary.Definitions
+
+child-replaced :  {n : Level} {A : Set n} (key : ℕ)   (tree : bt A) → bt A
+child-replaced key leaf = leaf
+child-replaced key (node key₁ value left right) with <-cmp key key₁
+... | tri< a ¬b ¬c = left
+... | tri≈ ¬a b ¬c = node key₁ value left right
+... | tri> ¬a ¬b c = right
+
+child-replaced-left :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}
+   → key < key₁
+   → child-replaced key (node key₁ value left right) ≡ left
+child-replaced-left {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
+     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key < key₁ → child-replaced key (node key₁ value left right) ≡ left
+     ch00 tree eq lt1 with <-cmp key key₁
+     ... | tri< a ¬b ¬c = refl
+     ... | tri≈ ¬a b ¬c = ⊥-elim (¬a lt1)
+     ... | tri> ¬a ¬b c = ⊥-elim (¬a lt1)
+
+child-replaced-right :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}
+   → key₁ < key
+   → child-replaced key (node key₁ value left right) ≡ right
+child-replaced-right {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
+     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ < key → child-replaced key (node key₁ value left right) ≡ right
+     ch00 tree eq lt1 with <-cmp key key₁
+     ... | tri< a ¬b ¬c = ⊥-elim (¬c lt1)
+     ... | tri≈ ¬a b ¬c = ⊥-elim (¬c lt1)
+     ... | tri> ¬a ¬b c = refl
+
+child-replaced-eq :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}
+   → key₁ ≡ key
+   → child-replaced key (node key₁ value left right) ≡ node key₁ value left right
+child-replaced-eq {n} {A} {key} {key₁} {value} {left} {right} keq = ch00 (node key₁ value left right) refl keq where
+     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ ≡ key → child-replaced key (node key₁ value left right) ≡ node key₁ value left right
+     ch00 tree eq keq with <-cmp key key₁
+     ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym keq))
+     ... | tri≈ ¬a b ¬c = refl
+     ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym keq))
+
+open _∧_
+
+ri-tr>  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key key₁ : ℕ) → (value : A)
+     → replacedTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl
+ri-tr> .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫
+ri-tr> .(node key _ _ _) .(node key value _ _) key key₁ value r-node a tgt = ⟪ a , ⟪ proj1 (proj2 tgt) , proj2 (proj2 tgt) ⟫ ⟫
+ri-tr> .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-right x ri) a tgt = ⟪ proj1 tgt , ⟪ proj1 (proj2 tgt) , ri-tr> _ _ _ _ _ ri a (proj2 (proj2 tgt)) ⟫ ⟫
+ri-tr> .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-left x ri) a tgt = ⟪ proj1 tgt , ⟪  ri-tr> _ _ _ _ _ ri a (proj1 (proj2 tgt)) , proj2 (proj2 tgt)  ⟫ ⟫
+
+ri-tr<  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key key₁ : ℕ) → (value : A)
+     → replacedTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl
+ri-tr< .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫
+ri-tr< .(node key _ _ _) .(node key value _ _) key key₁ value r-node a tgt = ⟪ a , ⟪ proj1 (proj2 tgt) , proj2 (proj2 tgt) ⟫ ⟫
+ri-tr< .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-right x ri) a tgt = ⟪ proj1 tgt , ⟪ proj1 (proj2 tgt) , ri-tr< _ _ _ _ _ ri a (proj2 (proj2 tgt)) ⟫ ⟫
+ri-tr< .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-left x ri) a tgt = ⟪ proj1 tgt , ⟪  ri-tr< _ _ _ _ _ ri a (proj1 (proj2 tgt)) , proj2 (proj2 tgt)  ⟫ ⟫
+
+<-tr>  : {n : Level} {A : Set n}  → {tree : bt A} → {key₁ key₂ : ℕ} → tr> key₁ tree → key₂ < key₁  → tr> key₂ tree
+<-tr> {n} {A} {leaf} {key₁} {key₂} tr lt = tt
+<-tr> {n} {A} {node key value t t₁} {key₁} {key₂} tr lt = ⟪ <-trans lt (proj1 tr) , ⟪ <-tr> (proj1 (proj2 tr)) lt , <-tr> (proj2 (proj2 tr)) lt ⟫ ⟫
+
+>-tr<  : {n : Level} {A : Set n}  → {tree : bt A} → {key₁ key₂ : ℕ} → tr< key₁ tree → key₁ < key₂  → tr< key₂ tree
+>-tr<  {n} {A} {leaf} {key₁} {key₂} tr lt = tt
+>-tr<  {n} {A} {node key value t t₁} {key₁} {key₂} tr lt = ⟪ <-trans (proj1 tr) lt , ⟪ >-tr< (proj1 (proj2 tr)) lt , >-tr< (proj2 (proj2 tr)) lt ⟫ ⟫
+
+RTtoTI0  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
+     → replacedTree key value tree repl → treeInvariant repl
+RTtoTI0 {n} {A} tree repl key value ti1 rt1 = lem00 tree _ _ _ refl ti1 rt1 where
+   lem00 : (tree tree1 : bt A) → (key : ℕ) → (value : A) → tree ≡ tree1 → treeInvariant tree  → replacedTree key value tree1 repl → treeInvariant repl
+   lem00 tree .leaf key value eq ti r-leaf = t-single key value
+   lem00 tree .(node key _ _ _) key value eq ti r-node = replaceTree1 key _ _ (subst (λ k → treeInvariant k) eq ti)
+   lem00 tree .(node _ _ _ _) key value eq1 ti (r-right {k₁} {v₁} {t₁} {t₂} {t₃} x rt) = lem03 _ ti eq1 lem02 rt where
+       lem01 : treeInvariant t₃
+       lem01 = treeRightDown _ _ (subst (λ k → treeInvariant k ) eq1 ti )
+       lem02 : treeInvariant t₁
+       lem02 = RTtoTI0 _ t₁ key value lem01 rt
+       lem03 : (tree : bt A) → treeInvariant tree → tree ≡ node k₁ v₁ t₂ t₃  → treeInvariant t₁ 
+            → replacedTree _ _ t₃ t₁ → treeInvariant (node k₁ v₁ t₂ t₁)
+       lem03 tree ti eq2 ti1 r-leaf = lem04 t₂ _ refl (subst (λ k → treeInvariant k) eq2 ti) where
+           lem04 : (t₂ tree : bt A) → tree ≡ node k₁ v₁ t₂ leaf → treeInvariant tree → treeInvariant (node k₁ v₁ t₂ (node key value leaf leaf))
+           lem04 t₂ _ () t-leaf
+           lem04 leaf _ eq (t-single key value) = t-right _ _ x _ _ (t-single _ _)
+           lem04 (node k v tl tr) _ () (t-single key value)
+           lem04 leaf _ () (t-left key key₁ x x₁ x₂ ti)
+           lem04 (node key₂ value t₂ t₃) _ eq (t-left key key₁ {_} {_} {t₄} {t₅} x₀ x₁ x₂ ti) = 
+               t-node _ _ _ lem06 x lem07 lem08 _ _ (subst (λ k → treeInvariant k) lem05 ti) (t-single _ _) where
+                  lem05 : node key _ t₄ t₅ ≡ node key₂ value t₂ t₃
+                  lem05 = just-injective (cong node-left eq)
+                  lem06 : key₂ < k₁
+                  lem06 = subst₂ (λ j k → j < k ) (just-injective (cong node-key lem05)) (just-injective (cong node-key eq)) x₀
+                  lem07 : tr< k₁ t₂
+                  lem07 = subst₂ (λ j k → tr< j k ) (just-injective (cong node-key eq)) (just-injective (cong node-left lem05)) x₁
+                  lem08 : tr< k₁ t₃
+                  lem08 = subst₂ (λ j k → tr< j k ) (just-injective (cong node-key eq)) (just-injective (cong node-right lem05)) x₂
+           lem04 t₂ _ () (t-right key key₁ x x₁ x₂ ti)
+           lem04 t₂ _ () (t-node key key₁ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁)
+       lem03 tree ti eq2 ti1 (r-node {value₁} {t} {t₁}) = lem04 t₂ _ refl (subst (λ k → treeInvariant k) eq2 ti) where
+           lem04 : (t₂ tree : bt A) → tree ≡ node k₁ v₁ t₂ (node key value₁ t t₁) → treeInvariant tree → treeInvariant (node k₁ v₁ t₂ (node key value t t₁ ))
+           lem04 t₂ .leaf () t-leaf
+           lem04 t₂ .(node key value leaf leaf) () (t-single key value)
+           lem04 (node k v _ _) .(node key value₂ leaf (node key₁ _ t₄ t₅)) () (t-right key key₁ {value₂} {_} {t₄} {t₅} x x₁ x₂ ti)
+           lem04 leaf .(node key value₂ leaf (node key₁ _ t₄ t₅)) eq (t-right key key₁ {value₂} {_} {t₄} {t₅} x₀ x₁ x₂ ti) = t-right _ _ x lem05 lem06 ti1 where
+                  lem05 : tr> k₁ t
+                  lem05 = subst₂ (λ j k → tr> j k) (just-injective (cong node-key eq)) (just-injective (cong node-left ( just-injective (cong node-right eq))))  x₁
+                  lem06 : tr> k₁ t₁
+                  lem06 = subst₂ (λ j k → tr> j k) (just-injective (cong node-key eq)) (just-injective (cong node-right ( just-injective (cong node-right eq))))  x₂
+           lem04 t₂ _ () (t-left key key₁ x x₁ x₂ ti)
+           lem04 leaf .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) () (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁)
+           lem04 (node key₃ value t₂ t₃) .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) eq (
+               t-node key key₁ key₂ {v₁} {v₂} {t₄} {t₅} {t₆} {t₇} {t₈} x x₁ x₂ x₃ x₄ x₅ ti ti₁) 
+                 = t-node _ _ _ lem06 lem07 lem08 lem09 lem10 lem11 (subst (λ k → treeInvariant k) lem05 ti) ti1 where
+                  lem05 : node key v₁ t₅ t₆ ≡ node key₃ value t₂ t₃
+                  lem05 = just-injective (cong node-left eq)
+                  lem06 :  key₃ < k₁
+                  lem06 = subst₂ (λ j k → j < k ) (just-injective (cong node-key lem05)) (just-injective (cong node-key eq)) x
+                  lem07 : k₁ < _
+                  lem07 = subst₂ (λ j k → j < k ) (just-injective (cong node-key eq)) (just-injective (cong node-key ( just-injective (cong node-right eq)))) x₁
+                  lem08 : tr< k₁ t₂
+                  lem08 = subst₂ (λ j k → tr< j k ) (just-injective (cong node-key eq)) (just-injective (cong node-left ( just-injective (cong node-left eq)))) x₂
+                  lem09 : tr< k₁ t₃
+                  lem09 = subst₂ (λ j k → tr< j k ) (just-injective (cong node-key eq)) (just-injective (cong node-right ( just-injective (cong node-left eq)))) x₃
+                  lem10 : tr> k₁ t
+                  lem10 = subst₂ (λ j k → tr> j k ) (just-injective (cong node-key eq)) (just-injective (cong node-left ( just-injective (cong node-right eq)))) x₄
+                  lem11 : tr> k₁ t₁
+                  lem11 = subst₂ (λ j k → tr> j k ) (just-injective (cong node-key eq)) (just-injective (cong node-right ( just-injective (cong node-right eq)))) x₅
+       lem03 tree ti eq2 ti1 (r-right {kr} {vr} {t₄} {t₅} {t₆} x rt1) = lem04 t₂ _ refl (subst (λ k → treeInvariant k) eq2 ti) where
+           lem04 : (t₂ tree : bt A) → tree ≡ node k₁ v₁ t₂ (node kr vr t₅ t₆) → treeInvariant tree → treeInvariant (node k₁ v₁ t₂ (node kr vr t₅ t₄))
+           lem04 t₂ _ () t-leaf
+           lem04 t₂ _ () (t-single key value)
+           lem04 t₂ _ () (t-left key key₁ x x₁ x₂ ti)
+           lem04 (node _ _ _ _) _ () (t-right key key₁ x x₁ x₂ ti1)
+           lem04 leaf .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ x x₁ x₂ ti2) = t-right _ _ lem05 lem06 lem07 ti1 where
+                  lem05 :  k₁ < kr 
+                  lem05 = subst₂ (λ j k → j < k ) (just-injective (cong node-key eq)) (just-injective (cong node-key ( just-injective (cong node-right eq)))) x 
+                  lem06 : tr> k₁ t₅
+                  lem06 = subst₂ (λ j k → tr> j k ) (just-injective (cong node-key eq)) (just-injective (cong node-left ( just-injective (cong node-right eq)))) x₁
+                  lem07 : tr> k₁ t₄
+                  lem07 = <-tr> (proj2 (ti-property1 ti1)) lem05
+           lem04 leaf .(node key₁ v₂ (node key v₁ t₈ t₉) (node key₂ t₇ t₁₀ t₁₁)) () (t-node key key₁ key₂ {v₁} {v₂} {t₇} {t₈} {t₉} {t₁₀} {t₁₁} x x₁ x₂ x₃ x₄ x₅ ti1 ti2)
+           lem04 (node key₃ value t₂ t₃) .(node key₁ v₂ (node key v₁ t₈ t₉) (node key₂ t₇ t₁₀ t₁₁)) eq 
+               (t-node key key₁ key₂ {v₁} {v₂} {t₇} {t₈} {t₉} {t₁₀} {t₁₁} x x₁ x₂ x₃ x₄ x₅ ti3 ti4) = t-node _ _ _ lem06 lem07 lem08 lem09 lem10 lem11 
+                       (subst (λ k → treeInvariant k) lem05 ti3) ti1 where
+                  lem05 : node key v₁ t₈ t₉ ≡ node key₃ value t₂ t₃
+                  lem05 = just-injective (cong node-left eq)
+                  lem06 : key₃ < k₁
+                  lem06 = subst₂ (λ j k → j < k ) (just-injective (cong node-key lem05)) (just-injective (cong node-key eq)) x
+                  lem07 : k₁ < kr
+                  lem07 = subst₂ (λ j k → j < k ) (just-injective (cong node-key eq)) (just-injective (cong node-key ( just-injective (cong node-right eq))) ) x₁
+                  lem08 : tr< k₁ t₂
+                  lem08 = subst₂ (λ j k → tr< j k ) (just-injective (cong node-key eq)) (just-injective (cong node-left ( just-injective (cong node-left eq))) ) x₂
+                  lem09 : tr< k₁ t₃
+                  lem09 = subst₂ (λ j k → tr< j k ) (just-injective (cong node-key eq)) (just-injective (cong node-right ( just-injective (cong node-left eq))) ) x₃
+                  lem10 : tr> k₁ t₅
+                  lem10 = subst₂ (λ j k → tr> j k ) (just-injective (cong node-key eq)) (just-injective (cong node-left ( just-injective (cong node-right eq))) ) x₄
+                  lem11 : tr> k₁ t₄
+                  lem11 = <-tr> (proj2 (ti-property1 ti1)) lem07
+       lem03 tree ti eq2 ti1 (r-left {kr} {vr} {t₄} {t₅} {t₆} x₃ rt1) = lem04 t₂ _ refl (subst (λ k → treeInvariant k) eq2 ti) where
+           lem04 : (t₂ tree : bt A) → tree ≡ node k₁ v₁ t₂ (node kr vr t₅ t₆) → treeInvariant tree → treeInvariant (node k₁ v₁ t₂ (node kr vr t₄ t₆))
+           lem04 t₂ _ () t-leaf
+           lem04 t₂ _ () (t-single key value)
+           lem04 t₂ _ () (t-left key key₁ x x₁ x₂ ti)
+           lem04 (node _ _ _ _) _ () (t-right key key₁ x x₁ x₂ ti)
+           lem04 leaf .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ {_} {_} {t₇} {t₈} x₀ x₁ x₂ ti) = t-right _ _ lem05 lem06 lem07 ti1 where
+                  lem05 :  k₁ < kr 
+                  lem05 = subst₂ (λ j k → j < k ) (just-injective (cong node-key eq)) (just-injective (cong node-key ( just-injective (cong node-right eq)))) x₀ 
+                  lem08 : key ≡ k₁
+                  lem08 = just-injective (cong node-key eq)
+                  lem09 : t₇ ≡ t₅
+                  lem09 = just-injective (cong node-left (just-injective (cong node-right eq)))
+                  lem10 : t₈ ≡ t₆
+                  lem10 = just-injective (cong node-right (just-injective (cong node-right eq)))
+                  lem06 : tr> k₁ t₄
+                  lem06 = proj1 ( proj2 ( ri-tr> _ _ _ _ _ rt x ⟪ <-trans x x₃ , ⟪ subst₂ (λ j k → tr> j k ) lem08 lem09 x₁  , subst₂ (λ j k → tr> j k ) lem08 lem10 x₂ ⟫ ⟫ )) 
+                  lem07 : tr> k₁ t₆
+                  lem07 = subst₂ (λ j k → tr> j k ) (just-injective (cong node-key eq)) (just-injective (cong node-right ( just-injective (cong node-right eq))) ) x₂
+           lem04 leaf _ () (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁)
+           lem04 (node key₃ value t₂ t₃) .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) eq 
+               (t-node key key₁ key₂ {v₁} {v₂} {t₇} {t₈} {t₉} {t₁₀} {t₁₁} x₀ x₁ x₂ x₃₃ x₄ x₅ ti ti₁) = 
+                t-node _ _ _ lem06 lem07 lem08 lem09 lem10 lem11 (subst (λ k → treeInvariant k) lem05 ti) ti1 where
+                  lem05 : node key v₁ t₈ t₉ ≡ node key₃ value t₂ t₃
+                  lem05 = just-injective (cong node-left eq)
+                  lem06 : key₃ < k₁
+                  lem06 = subst₂ (λ j k → j < k ) (just-injective (cong node-key lem05)) (just-injective (cong node-key eq)) x₀
+                  lem07 : k₁ < kr
+                  lem07 = subst₂ (λ j k → j < k ) (just-injective (cong node-key eq)) (just-injective (cong node-key ( just-injective (cong node-right eq))) ) x₁
+                  lem08 : tr< k₁ t₂
+                  lem08 = subst₂ (λ j k → tr< j k ) (just-injective (cong node-key eq)) (just-injective (cong node-left ( just-injective (cong node-left eq))) ) x₂
+                  lem09 : tr< k₁ t₃
+                  lem09 = subst₂ (λ j k → tr< j k ) (just-injective (cong node-key eq)) (just-injective (cong node-right ( just-injective (cong node-left eq))) ) x₃₃
+                  lem12 : key₁ ≡ k₁
+                  lem12 = just-injective (cong node-key eq)
+                  lem13 : t₁₀ ≡ t₅
+                  lem13 = just-injective (cong node-left (just-injective (cong node-right eq)))
+                  lem14 : t₁₁ ≡ t₆
+                  lem14 = just-injective (cong node-right (just-injective (cong node-right eq)))
+                  lem10 : tr> k₁ t₄
+                  lem10 = proj1 ( proj2 ( ri-tr> _ _ _ _ _ rt x ⟪ <-trans x x₃ , ⟪ subst₂ (λ j k → tr> j k ) lem12 lem13 x₄  , subst₂ (λ j k → tr> j k ) lem12 lem14 x₅ ⟫ ⟫ )) 
+                  lem11 : tr> k₁ t₆
+                  lem11 = <-tr> (proj2 (ti-property1 ti1)) lem07
+   lem00 tree .(node _ _ _ _) key value eq1 ti (r-left  {k₁} {v₁} {t₁} {t₂} {t₃} x rt) = lem03 _ ti eq1 lem02 rt where
+       lem01 : treeInvariant t₂
+       lem01 = treeLeftDown _ _ (subst (λ k → treeInvariant k ) eq1 ti )
+       lem02 : treeInvariant t₁
+       lem02 = RTtoTI0 _ t₁ key value lem01 rt
+       lem03 : (tree : bt A) → treeInvariant tree → tree ≡ node k₁ v₁ t₂ t₃  → treeInvariant t₁ 
+            → replacedTree _ _ t₂ t₁ →  treeInvariant (node k₁ v₁ t₁ t₃)
+       lem03 tree ti eq2 ti1 r-leaf = lem04 _ refl (subst (λ k → treeInvariant k) eq2 ti) where
+           lem04 : (tree : bt A) → tree ≡ node k₁ v₁ leaf t₃ → treeInvariant tree → treeInvariant (node k₁ v₁ (node key value leaf leaf) t₃)
+           lem04 _ () t-leaf
+           lem04 _ eq (t-single key value) = subst (λ k → treeInvariant (node k₁ v₁ (node _ _ leaf leaf) k)) 
+               (just-injective (cong node-right eq) ) (t-left _ _ x _ _ (t-single _ _) )
+           lem04 _ eq (t-left key key₁ {_} {_} {t₄} {t₅} x₀ x₁ x₂ ti) = subst (λ k → treeInvariant (node k₁ v₁ (node _ _ leaf leaf) k)) 
+               (just-injective (cong node-right eq) ) (t-left _ _ x _ _ (t-single _ _) )
+           lem04  _ eq (t-right key key₁ {_} {_} {t₄} {t₅} x₀ x₁ x₂ ti) = subst (λ k → treeInvariant (node k₁ v₁ (node _ _ leaf leaf) k)) 
+              (just-injective (cong node-right eq) ) ( t-node _ _ _ x (subst (λ j → j < key₁ ) lem05 x₀)  tt tt (subst (λ j → tr> j t₄) lem05 x₁) 
+                (subst (λ j → tr> j t₅) lem05 x₂)  (t-single _ _ ) ti) where
+                  lem05 : key  ≡ k₁
+                  lem05 = just-injective (cong node-key eq)
+           lem04 _ () (t-node key key₁ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁)
+       lem03 tree ti eq2 ti1 (r-node {value₁} {t} {t₁}) = lem04 _ refl (subst (λ k → treeInvariant k) eq2 ti) where
+           lem04 : (tree : bt A) → tree ≡ node k₁ v₁ (node key value₁ t t₁) t₃ → treeInvariant tree → treeInvariant (node k₁ v₁ (node  key value t t₁) t₃)
+           lem04 .leaf () t-leaf
+           lem04 .(node key value leaf leaf) () (t-single key value)
+           lem04 .(node key value₂ leaf (node key₁ _ t₄ t₅)) () (t-right key key₁ {value₂} {_} {t₄} {t₅} x x₁ x₂ ti)
+           lem04 _ eq (t-left key key₁ {value₂} {_} {t₄} {t₅} x₀ x₁ x₂ ti) = subst (λ k → treeInvariant (node k₁ v₁ (node _ _ t t₁) k))  
+               (just-injective (cong node-right eq) ) (t-left _ _ x (subst₂ (λ j k → tr< j k ) lem05 lem06 x₁)  (subst₂ (λ j k → tr< j k ) lem05 lem07 x₂) ti1 ) where
+                  lem05 : key₁ ≡ k₁
+                  lem05 = just-injective (cong node-key eq)
+                  lem06 : t₄ ≡ t
+                  lem06 = just-injective (cong node-left (just-injective (cong node-left eq)))
+                  lem07 : t₅ ≡ t₁
+                  lem07 = just-injective (cong node-right (just-injective (cong node-left eq)))
+           lem04 .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) eq (t-node key key₁ key₂ {v₁} {v₂} {t₇} {t₈} {t₉} {t₁₀} {t₁₁} x₀ x₁ x₂ x₃ x₄ x₅ ti ti₁) 
+             = subst (λ k → treeInvariant (node k₁ _ (node _ _ t t₁) k)) (just-injective (cong node-right eq) ) 
+                (t-node _ _ _ x (subst (λ j → j < key₂) lem05 x₁)  lem06 lem07 lem08 lem09 ti1 ti₁) where
+                  lem05 : key₁ ≡ k₁
+                  lem05 = just-injective (cong node-key eq)
+                  lem06 : tr< k₁ t
+                  lem06 = subst₂ (λ j k → tr< j k) lem05 (just-injective (cong node-left ( just-injective (cong node-left eq )))) x₂
+                  lem07 : tr< k₁ t₁
+                  lem07 = subst₂ (λ j k → tr< j k) lem05 (just-injective (cong node-right ( just-injective (cong node-left eq )))) x₃
+                  lem08 : tr> k₁ t₁₀
+                  lem08 = subst (λ j  → tr> j _) lem05 x₄
+                  lem09 : tr> k₁ t₁₁
+                  lem09 = subst (λ j  → tr> j _) lem05 x₅
+       lem03 tree ti eq2 ti1 (r-right {kr} {vr} {t₄} {t₅} {t₆} x₃ rt2) = lem04 _ _ refl (subst (λ k → treeInvariant k) eq2 ti) where
+           lem04 : (t₃ tree : bt A) → tree ≡  node k₁ v₁ (node kr vr t₅ t₆) t₃ → treeInvariant tree → treeInvariant (node k₁ v₁ (node kr vr t₅ t₄) t₃) 
+           lem04 t₃ _ () t-leaf
+           lem04 t₃ _ () (t-single key value)
+           lem04 t₃ _ eq (t-left key key₁ {value₂} {_} {t₆} {t₇} x₀ x₁ x₂ ti) = subst (λ k → treeInvariant (node k₁ v₁ (node kr vr t₅ t₄) k))
+               (just-injective (cong node-right eq) ) (t-left _ _ (subst₂ (λ j k → j < k ) lem06 lem05 x₀)  lem07 lem08 ti1) where
+                  lem05 : key₁ ≡ k₁
+                  lem05 = just-injective (cong node-key eq)
+                  lem06 : key ≡ kr
+                  lem06 = just-injective (cong node-key ( just-injective (cong node-left eq)))
+                  lem07 : tr< k₁ t₅
+                  lem07 = subst₂ (λ j k → tr< j k ) lem05 (just-injective (cong node-left (just-injective (cong node-left eq))) ) x₁
+                  lem08 : tr< k₁ t₄
+                  lem08 = ri-tr< _ _ _ _ _ rt2 x (subst₂ (λ j k → tr< j k ) lem05 (just-injective (cong node-right (just-injective (cong node-left eq)))) x₂)
+           lem04 (node _ _ _ _) _ () (t-right key key₁ x x₁ x₂ ti1)
+           lem04 leaf .(node key _ leaf (node key₁ _ _ _)) () (t-right key key₁ x x₁ x₂ ti2)
+           lem04 leaf .(node key₁ v₂ (node key v₁ t₈ t₉) (node key₂ t₇ t₁₀ t₁₁)) () (t-node key key₁ key₂ {v₁} {v₂} {t₇} {t₈} {t₉} {t₁₀} {t₁₁} x x₁ x₂ x₃ x₄ x₅ ti1 ti2)
+           lem04 (node key₃ value t₂ t₃) .(node key₁ v₂ (node key v₁ t₈ t₉) (node key₂ v₃ t₁₀ t₁₁)) eq 
+               (t-node key key₁ key₂ {v₁} {v₂} {v₃} {t₈} {t₉} {t₁₀} {t₁₁} x₀ x₁ x₂ x₃₃ x₄ x₅ ti3 ti4) 
+                 = t-node _ _ _ (<-trans x₃ x )  lem06 lem07 lem08 lem09 lem10 ti1 (subst (λ k → treeInvariant k) lem05 ti4) where
+                  lem05 : node key₂ v₃ t₁₀ t₁₁ ≡ node key₃ value t₂ t₃
+                  lem05 = just-injective (cong node-right eq)
+                  lem06 : k₁ < key₃ 
+                  lem06 = subst₂ (λ j k → j < k ) (just-injective (cong node-key eq)) (just-injective (cong node-key ( just-injective (cong node-right eq))) ) x₁
+                  lem18 : key₁ ≡ k₁
+                  lem18 = just-injective (cong node-key eq)
+                  lem07 : tr< k₁ t₅
+                  lem07 = subst₂ (λ j k → tr< j k ) lem18 (just-injective (cong node-left ( just-injective (cong node-left eq))) ) x₂
+                  lem08 : tr< k₁ t₄
+                  lem08 = ri-tr< _ _ _ _ _ rt2 x (subst₂ (λ j k → tr< j k ) lem18 (just-injective (cong node-right ( just-injective (cong node-left eq))) ) x₃₃ )
+                  lem09 : tr> k₁ t₂
+                  lem09 = subst₂ (λ j k → tr> j k ) lem18 (just-injective (cong node-left ( just-injective (cong node-right eq))) ) x₄ 
+                  lem10 : tr> k₁ t₃ 
+                  lem10 = subst₂ (λ j k → tr> j k ) lem18 (just-injective (cong node-right ( just-injective (cong node-right eq))) ) x₅ 
+       lem03 tree ti eq2 ti1 (r-left {kr} {vr} {t₄} {t₅} {t₆} x₃ rt1) = lem04 t₃ _ refl (subst (λ k → treeInvariant k) eq2 ti) where
+           lem04 : (t₃ tree : bt A) → tree ≡ node k₁ v₁ (node kr vr t₅ t₆) t₃ → treeInvariant tree → treeInvariant (node k₁ v₁ (node kr vr t₄ t₆) t₃)
+           lem04 t₃ _ () t-leaf
+           lem04 t₃ _ () (t-single key value)
+           lem04 t₃ _ () (t-right key key₁ x x₁ x₂ ti) 
+           lem04 (node key₃ value t₂ t₃) _ () (t-left key key₁ {_} {_} {t₇} {t₈} x₀ x₁ x₂ ti)
+           lem04 leaf _ eq (t-left key key₁ {_} {_} {t₇} {t₈} x₀ x₁ x₂ ti) = t-left _ _ lem05 lem06 lem07 ti1 where
+                  lem08 : key₁ ≡ k₁
+                  lem08 = just-injective (cong node-key eq)
+                  lem05 : kr < k₁  
+                  lem05 = subst₂ (λ j k → j < k ) (just-injective (cong node-key ( just-injective (cong node-left eq))) ) lem08 x₀
+                  lem06 : tr< k₁ t₄
+                  lem06 = ri-tr< _ _ _ _ _ rt1 x (subst₂ (λ j k → tr< j k ) lem08 (just-injective (cong node-left ( just-injective (cong node-left eq))) ) x₁)
+                  lem07 : tr< k₁ t₆
+                  lem07 = subst₂ (λ j k → tr< j k ) lem08 (just-injective (cong node-right ( just-injective (cong node-left eq))) ) x₂
+           lem04 leaf _ () (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁)
+           lem04 (node key₃ value t₂ t₃) .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) eq 
+              (t-node key key₁ key₂ {v₁} {v₂} {v₃} {t₈} {t₉} {t₁₀} {t₁₁} x₀ x₁ x₂ x₃ x₄ x₅ ti ti₁) = t-node _ _ _ lem05 lem06 lem07 lem09 lem10 lem11 
+                       ti1 (subst (λ k → treeInvariant k) (just-injective (cong node-right eq)) ti₁) where
+                  lem08 : key₁ ≡ k₁
+                  lem08 = just-injective (cong node-key eq)
+                  lem05 : kr < k₁  
+                  lem05 = subst₂ (λ j k → j < k ) (just-injective (cong node-key ( just-injective (cong node-left eq))) ) lem08 x₀
+                  lem06 : k₁ < key₃
+                  lem06 = subst₂ (λ j k → j < k ) (just-injective (cong node-key eq)) (just-injective (cong node-key ( just-injective (cong node-right eq))) ) x₁
+                  lem07 : tr< k₁ t₄
+                  lem07 = ri-tr< _ _ _ _ _ rt1 x (subst₂ (λ j k → tr< j k ) lem08 (just-injective (cong node-left ( just-injective (cong node-left eq))) ) x₂)
+                  lem09 : tr< k₁ t₆
+                  lem09 = subst₂ (λ j k → tr< j k ) lem08 (just-injective (cong node-right ( just-injective (cong node-left eq))) ) x₃
+                  lem10 : tr> k₁ t₂
+                  lem10 = subst₂ (λ j k → tr> j k ) (just-injective (cong node-key eq)) (just-injective (cong node-left ( just-injective (cong node-right eq))) ) x₄
+                  lem11 : tr> k₁ t₃
+                  lem11 = subst₂ (λ j k → tr> j k ) (just-injective (cong node-key eq)) (just-injective (cong node-right ( just-injective (cong node-right eq))) ) x₅
+
+
+
+
+popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt A))
+           → ( tree parent orig : bt A) →  (key : ℕ)
+           → stackInvariant key tree  orig ( tree ∷ parent ∷ rest )
+           → stackInvariant key parent orig (parent ∷ rest )
+popStackInvariant rest tree parent orig key = ?
+
+siToTreeinvariant : {n : Level} {A : Set n} → (rest : List ( bt A))
+           → ( tree orig : bt A) →  (key : ℕ)
+           → treeInvariant orig
+           → stackInvariant key tree  orig ( tree ∷ rest )
+           → treeInvariant tree
+siToTreeinvariant = ?
+
+record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
+   field
+     tree0 : bt A
+     ti : treeInvariant tree0
+     si : stackInvariant key tree tree0 stack
+     ri : replacedTree key value (child-replaced key tree ) repl
+     rti : treeInvariant repl
+     ci : C tree repl stack     -- data continuation
+
+replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
+    → (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 = ?
+--   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)
+--        (subst (λ j → replacedTree k v1 j  (node k v1 t t₁) ) repl00 r-node) where
+--            repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁)
+--            repl00 with <-cmp k k
+--            ... | tri< a ¬b ¬c = ⊥-elim (¬b refl)
+--            ... | tri≈ ¬a b ¬c = refl
+--            ... | tri> ¬a ¬b c = ⊥-elim (¬b refl)
+--
+
+replaceP : {n m : Level} {A : Set n} {t : Set m}
+     → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A)
+     → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤)
+     → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
+         → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
+     → (exit : (tree1 repl : bt A) → treeInvariant repl ∧ replacedTree key value tree1 repl → t) → t
+replaceP key value {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
+replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (replacePR.si Pre)-- tree0 ≡ leaf
+... | eq  =  exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ t-single _ _  ,  ? ⟫
+replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right )
+        ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where
+    repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right )
+    -- repl01 = ? --with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)
+    repl01 = ? where
+    -- | refl | refl = subst (λ k → replacedTree key value  (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where
+        repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
+        repl03 = replacePR.ri ?
+        repl02 : child-replaced key (node key₁ value₁ left right) ≡ left
+        repl02 with <-cmp key key₁
+        ... | tri< a ¬b ¬c = refl
+        ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a)
+        ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a)
+... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪  RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where
+    repl01 : replacedTree key value (replacePR.tree0 Pre) repl
+    --repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)
+    repl01 = ? where
+    --repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where
+        repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right
+        repl02 with <-cmp key key₁
+        ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b)
+        ... | tri≈ ¬a b ¬c = refl
+        ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b)
+... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl  ) ⟪  RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where
+    repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl )
+    -- repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)
+    repl01 = ? where
+    -- repl01 | refl | refl = subst (λ k → replacedTree key value  (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where
+        repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
+        repl03 = replacePR.ri ?
+        repl02 : child-replaced key (node key₁ value₁ left right) ≡ right
+        repl02 with <-cmp key key₁
+        ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c)
+        ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c)
+        ... | tri> ¬a ¬b c = refl
+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 = ? -- where with replacePR.si Pre
+--   -- ... | s-right  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ;
+--          rti = replacePR.rti Pre ; ci = lift tt } where
+--       repl09 : tree1 ≡ node key₂ v1 tree₁ leaf
+--       repl09 = si-property1 si
+--       repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
+--       repl10 with si-property1 si
+--       ... | refl = si
+--       repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf
+--       repl07 with <-cmp key key₂
+--       ... |  tri< a ¬b ¬c = ⊥-elim (¬c x)
+--       ... |  tri≈ ¬a b ¬c = ⊥-elim (¬c x)
+--       ... |  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 ; rti = replacePR.rti Pre ; 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)
+--       repl10 with si-property1 si
+--       ... | refl = si
+--       repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf
+--       repl07 with <-cmp key key₂
+--       ... |  tri< a ¬b ¬c = refl
+--       ... |  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
+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 ⊤)
+    Post = ? -- with replacePR.si Pre
+--    ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10
+--      ; rti = repl13
+--      ; 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)
+--        repl10 with si-property1 si
+--        ... | refl = si
+--        repl11 : stackInvariant key (node key₂ v1 tree₁ (node key₁ value₁ left right)) (replacePR.tree0 Pre) (node key₂ v1 tree₁ (node key₁ value₁ left right)∷ st1)
+--        repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10
+--        repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
+--        repl03 with <-cmp key key₁
+--        ... | tri< a1 ¬b ¬c = refl
+--        ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
+--        ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
+--        repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
+--        repl02 with repl09 | <-cmp key key₂
+--        ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
+--        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
+--        ... | refl | tri> ¬a ¬b c = refl
+--        repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
+--        repl04  = begin
+--            node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03  ⟩
+--            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+--            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+--            child-replaced key tree1 ∎  where open ≡-Reasoning
+--        repl05 : node key₁ value₁ left right ≡ child-replaced key tree1
+--        repl05  = begin
+--            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+--            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+--            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))
+--        repl13 : treeInvariant (node key₁ value₁ repl right)
+--        repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeRightDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12
+--    ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; 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)
+--        repl10 with si-property1 si
+--        ... | refl = si
+--        repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
+--        repl03 with <-cmp key key₁
+--        ... | tri< a1 ¬b ¬c = refl
+--        ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
+--        ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
+--        repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
+--        repl02 with repl09 | <-cmp key key₂
+--        ... | refl | tri< a ¬b ¬c = refl
+--        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
+--        ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
+--        repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
+--        repl04  = begin
+--            node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03  ⟩
+--            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+--            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+--            child-replaced key tree1 ∎  where open ≡-Reasoning
+--        repl05 : node key₁ value₁ left right ≡ child-replaced key tree1
+--        repl05  = begin
+--            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+--            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+--            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))
+--        repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10
+--        repl13 :  treeInvariant (node key₁ value₁ repl right)
+--        repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeLeftDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12
+... | 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 ; rti = repl13 ; 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)
+--        repl10 with si-property1 si
+--        ... | refl = si
+--        repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree
+--        repl07 with <-cmp key key₂
+--        ... |  tri< a ¬b ¬c = ⊥-elim (¬c x)
+--        ... |  tri≈ ¬a b ¬c = ⊥-elim (¬c x)
+--        ... |  tri> ¬a ¬b c = refl
+--        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
+--        repl13 : treeInvariant (node key₁ value left right)
+--        repl13 = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (replacePR.si Pre))  r-node
+--    ... | s-left  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; 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)
+--        repl10 with si-property1 si
+--        ... | refl = si
+--        repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree
+--        repl07 with <-cmp key key₂
+--        ... |  tri< a ¬b ¬c = refl
+--        ... |  tri≈ ¬a b ¬c = ⊥-elim (¬a x)
+--        ... |  tri> ¬a ¬b c = ⊥-elim (¬a x)
+--        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
+--        repl13 : treeInvariant (node key₁ value left right)
+--        repl13 = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (replacePR.si Pre))  r-node
+... | 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 ; rti = repl13 ; 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)
+--        repl10 with si-property1 si
+--        ... | refl = si
+--        repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
+--        repl03 with <-cmp key key₁
+--        ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
+--        ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
+--        ... | tri> ¬a ¬b c = refl
+--        repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
+--        repl02 with repl09 | <-cmp key key₂
+--        ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
+--        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
+--        ... | refl | tri> ¬a ¬b c = refl
+--        repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
+--        repl04  = begin
+--            node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
+--            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+--            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+--            child-replaced key tree1 ∎  where open ≡-Reasoning
+--        repl05 : node key₁ value₁ left right ≡ child-replaced key tree1
+--        repl05  = begin
+--            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+--            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+--            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))
+--        repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10
+--        repl13 : treeInvariant (node key₁ value₁ left repl)
+--        repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeRightDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12
+--    ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; 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)
+--        repl10 with si-property1 si
+--        ... | refl = si
+--        repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
+--        repl03 with <-cmp key key₁
+--        ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
+--        ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
+--        ... | tri> ¬a ¬b c = refl
+--        repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
+--        repl02 with repl09 | <-cmp key key₂
+--        ... | refl | tri< a ¬b ¬c = refl
+--        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
+--        ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
+--        repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
+--        repl04  = begin
+--            node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
+--            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+--            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+--            child-replaced key tree1 ∎  where open ≡-Reasoning
+--        repl05 : node key₁ value₁ left right ≡ child-replaced key tree1
+--        repl05  = begin
+--            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+--            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+--            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))
+--        repl13 : treeInvariant (node key₁ value₁ left repl)
+--        repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeLeftDown _ _
+--           (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10)) )) repl12
+
+TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
+   → (r : Index) → (p : Invraiant r)
+   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t) → t
+TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
+... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim ? ) --
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where
+    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
+    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim ?) -- (lemma5 n≤j lt1))
+    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
+    ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
+    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )
+
+
+insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
+     → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t
+insertTreeP {n} {m} {A} {t} tree key value P0 exit =
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫  ⟪ P0 , s-nil ⟫
+       $ λ p P loop → findP key (proj1 p)  tree (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt )
+       $ λ t s P C → replaceNodeP key value t C (proj1 P)
+       $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
+            {λ p → replacePR key value  (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p)  (λ _ _ _ → Lift n ⊤ ) }
+               (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; rti = P1 ; ri = R ; ci = lift tt }
+       $  λ p P1 loop → replaceP key value  (proj2 (proj2 p)) (proj1 p) P1
+            (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1  ⟫ ⟫ P2 lt )
+       $ λ tree repl P → exit tree repl P
+
+insertTestP1 = insertTreeP leaf 1 1 t-leaf
+  $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0)
+  $ λ _ x1 P1 → insertTreeP x1 3 2 (proj1 P1)
+  $ λ _ x2 P2 → insertTreeP x2 2 2 (proj1 P2) (λ _ x P  → x )
+
+-- is realy inserted?
+
+-- other element is preserved?
+
+-- deletion?
+

--- a/RBTree.agda	Tue Aug 13 23:03:40 2024 +0900
+++ b/RBTree.agda	Sun Aug 18 20:02:03 2024 +0900
@@ -1,6 +1,5 @@
-{-# OPTIONS --cubical-compatible --allow-unsolved-metas  #-}
---  {-# OPTIONS --cubical-compatible --safe #-}
-
+-- {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --cubical-compatible #-}
 module RBTree where
 
 open import Level hiding (suc ; zero ; _⊔_ )
@@ -8,14 +7,13 @@
 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.Unit
 open import Data.List
+open import Data.List.Properties
 open import Data.Product
 
-open import Data.Maybe.Properties
-open import Data.List.Properties
-
 open import Function as F hiding (const)
 
 open import Relation.Binary
@@ -24,912 +22,10 @@
 open import logic
 open import nat
 
-
---
---
---  no children , having left node , having right node , having both
---
-data bt {n : Level} (A : Set n) : Set n where
-  leaf : bt A
-  node :  (key : ℕ) → (value : A) →
-    (left : bt A ) → (right : bt A ) → bt A
-
-node-key : {n : Level} {A : Set n} → bt A → Maybe ℕ
-node-key (node key _ _ _) = just key
-node-key _ = nothing
-
-node-value : {n : Level} {A : Set n} → bt A → Maybe A
-node-value (node _ value _ _) = just value
-node-value _ = nothing
-
-bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
-bt-depth leaf = 0
-bt-depth (node key value t t₁) = suc (bt-depth t  ⊔ bt-depth t₁ )
-
-bt-ne : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ : bt A} → ¬ ( leaf ≡ node key value t t₁ )
-bt-ne {n} {A} {key} {value} {t} {t₁} ()
-
-open import Data.Unit hiding ( _≟_ ) -- ;  _≤?_ ; _≤_)
-
-tr< : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
-tr< {_} {A} key leaf = ⊤
-tr< {_} {A} key (node key₁ value tr tr₁) = (key₁ < key ) ∧ tr< key tr  ∧  tr< key tr₁
-
-tr> : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
-tr> {_} {A} key leaf = ⊤
-tr> {_} {A} key (node key₁ value tr tr₁) = (key < key₁ ) ∧ tr> key tr  ∧  tr> key tr₁
-
---
---
-data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
-    t-leaf : treeInvariant leaf
-    t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf)
-    t-right : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁
-       → tr> key t₁
-       → tr> key t₂
-       → treeInvariant (node key₁ value₁ t₁ t₂)
-       → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
-    t-left  : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁
-       → tr< key₁ t₁
-       → tr< key₁ t₂
-       → treeInvariant (node key value t₁ t₂)
-       → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf )
-    t-node  : (key key₁ key₂ : ℕ) → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → key < key₁ → key₁ < key₂
-       → tr< key₁ t₁
-       → tr< key₁ t₂
-       → tr> key₁ t₃
-       → tr> key₁ t₄
-       → treeInvariant (node key value t₁ t₂)
-       → treeInvariant (node key₂ value₂ t₃ t₄)
-       → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
-
---
---  stack always contains original top at end (path of the tree)
---
-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)}
-        → 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)}
-        → 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
-    r-leaf : replacedTree key value leaf (node key value leaf leaf)
-    r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
-    r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k < key →  replacedTree key value t2 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t)
-    r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → key < k →  replacedTree key value t1 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t t2)
-
-add< : { i : ℕ } (j : ℕ ) → i < suc i + j
-add<  {i} j = begin
-        suc i ≤⟨ m≤m+n (suc i) j ⟩
-        suc i + j ∎  where open ≤-Reasoning
-
-treeTest1  : bt ℕ
-treeTest1  =  node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
-treeTest2  : bt ℕ
-treeTest2  =  node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
-
-treeInvariantTest1  : treeInvariant treeTest1
-treeInvariantTest1  = t-right _ _ (m≤m+n _ 2)
-    ⟪ add< _ , ⟪ ⟪ add< _ , _ ⟫ , _ ⟫ ⟫
-    ⟪ add< _ , ⟪ _ , _ ⟫ ⟫ (t-node _ _ _ (add< 0) (add< 1) ⟪ add< _ , ⟪ _ , _ ⟫ ⟫  _ _ _ (t-left _ _ (add< 0) _ _ (t-single 1 7)) (t-single 5 5) )
-
-stack-top :  {n : Level} {A : Set n} (stack  : List (bt A)) → Maybe (bt A)
-stack-top [] = nothing
-stack-top (x ∷ s) = just x
-
-stack-last :  {n : Level} {A : Set n} (stack  : List (bt A)) → Maybe (bt A)
-stack-last [] = nothing
-stack-last (x ∷ []) = just x
-stack-last (x ∷ s) = stack-last s
-
-stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
-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-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 {n} {A} {key} {tree} {tree0} {tree1} {stack} si = lem00 tree tree0 tree1 _ (tree1 ∷ stack) refl si where
-    lem00 : (tree tree0 tree1 : bt A) → (stack  stack1 : List (bt A)) → tree1 ∷ stack ≡ stack1  →  stackInvariant key tree tree0 stack1 → tree1 ≡ tree
-    lem00 tree .tree tree1 stack .(tree ∷ []) eq s-nil = ∷-injectiveˡ eq
-    lem00 tree tree0 tree1 stack .(tree ∷ _) eq (s-right .tree .tree0 tree₁ x si) = ∷-injectiveˡ eq
-    lem00 tree tree0 tree1 stack .(tree ∷ _) eq (s-left .tree .tree0 tree₁ x si) = ∷-injectiveˡ eq
-
-si-property2 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → (stack  : List (bt A)) →  stackInvariant key tree tree0 (tree1 ∷ stack)
-   → ¬ ( just leaf ≡ stack-last stack )
-si-property2 {n} {A} {key} {tree} {tree0} {tree1} [] si ()
-si-property2 {n} {A} {key} {tree} {tree0} {tree1} (x ∷ []) si eq with just-injective eq
-... | refl = lem00 (tree1 ∷ leaf ∷ [])  refl si  where
-    lem00 : (t : List (bt A)) → (tree1 ∷ leaf ∷ []) ≡ t → stackInvariant key tree tree0 t → ⊥
-    lem00 .(tree ∷ []) () s-nil
-    lem00 (tree ∷ _) () (s-right .tree .(node _ _ tree₁ tree) tree₁ x s-nil)
-    lem00 (tree ∷ _) () (s-right .tree .tree0 tree₁ x (s-right .(node _ _ tree₁ tree) .tree0 tree₂ x₁ si2))
-    lem00 (tree ∷ _) () (s-right .tree .tree0 tree₁ x (s-left .(node _ _ tree₁ tree) .tree0 tree₂ x₁ si2))
-    lem00 (tree₁ ∷ _) () (s-left .tree₁ .(node _ _ tree₁ tree) tree x s-nil)
-    lem00 (tree₁ ∷ _) () (s-left .tree₁ .tree0 tree x (s-right .(node _ _ tree₁ tree) .tree0 tree₂ x₁ si2))
-    lem00 (tree₁ ∷ _) () (s-left .tree₁ .tree0 tree x (s-left .(node _ _ tree₁ tree) .tree0 tree₂ x₁ si2))
-si-property2 {n} {A} {key} {tree} {tree0} {tree1} (x ∷ x₁ ∷ stack) si = lem00 (tree1 ∷ x ∷ x₁ ∷ stack) refl si where
-    lem00 : (t : List (bt A)) → (tree1 ∷ x ∷ x₁ ∷ stack) ≡ t → stackInvariant key tree tree0 t → ¬ just leaf ≡ stack-last (x₁ ∷ stack)
-    lem00 .(tree ∷ []) () s-nil
-    lem00 (tree ∷ []) () (s-right .tree .tree0 tree₁ x si)
-    lem00 (tree ∷ x₁ ∷ st) eq (s-right .tree .tree0 tree₁ x si) eq1 = si-property2 st si
-         (subst (λ k → just leaf ≡ stack-last k ) (∷-injectiveʳ (∷-injectiveʳ eq)) eq1 )
-    lem00 (tree ∷ []) () (s-left .tree .tree0 tree₁ x si)
-    lem00 (tree₁ ∷ x₁ ∷  st) eq (s-left .tree₁ .tree0 tree x si) eq1 = si-property2 st si
-         (subst (λ k → just leaf ≡ stack-last k ) (∷-injectiveʳ (∷-injectiveʳ eq)) eq1 )
-
-
--- We cannot avoid warning: -W[no]UnsupportedIndexedMatcin tree-inject
--- open import Function.Base using (_∋_; id; _∘_; _∘′_)
--- just-injective1 : {n : Level } {A : Set n} {x y : A } → (Maybe A ∋ just x) ≡ just y → x ≡ y
--- just-injective1 refl = refl
-
-node-left : {n : Level} {A : Set n} → bt A → Maybe (bt A)
-node-left (node _ _ left _) = just left
-node-left _ = nothing
-
-node-right : {n : Level} {A : Set n} → bt A → Maybe (bt A)
-node-right (node _ _ _ right) = just right
-node-right _ = nothing
-
---   lem00 = just-injective (cong node-key eq)
-
-tree-injective-key : {n : Level} {A : Set n}
-    → (tr0 tr1 : bt A) → tr0 ≡ tr1 → node-key tr0 ≡ node-key tr1
-tree-injective-key {n} {A} tr0 tr1 eq = cong node-key eq
-
-ti-property2 :  {n : Level} {A : Set n} {key : ℕ} {value : A} {tree1 left right : bt A}
-   → tree1 ≡ node key value left right
-   → left ≡ right
-   → ( ¬ left  ≡ leaf ) ∨ ( ¬ right ≡ leaf )
-   → ¬ treeInvariant tree1
-ti-property2 {n} {A} {key} {value} {leaf} {left} {right} () eq1 x ti
-ti-property2 {n} {A} {key} {value} {node key₁ value₁ leaf t₁} {left} {right} eq eq1 (case1 eq2) _
-    = ⊥-elim ( eq2 (just-injective ( cong node-left (sym eq)  )))
-ti-property2 {n} {A} {key} {value} {node key₁ value₁ leaf t₁} {left} {right} eq eq1 (case2 eq2) _
-    = ⊥-elim ( eq2 (just-injective (trans (cong just (sym eq1)) ( cong node-left (sym eq)   ) ) ))
-ti-property2 {n} {A} {key} {value} {node key₁ value₁ (node key₂ value₂ t t₂) leaf} {left} {right} eq eq1 (case1 eq2) _
-    = ⊥-elim ( eq2 (just-injective (trans (cong just eq1) ( cong node-right (sym eq)   ) ) ))
-ti-property2 {n} {A} {key} {value} {node key₁ value₁ (node key₂ value₂ t t₂) leaf} {left} {right} eq eq1 (case2 eq2) _
-    = ⊥-elim ( eq2 (just-injective ( cong node-right (sym eq)  )))
-ti-property2 {n} {A} {key} {value} {node key₂ value₂ (node key₁ value₁ t₁ t₂) (node key₃ value₃ t₃ t₄)} {left} {right} eq eq1 eq2 ti
-     = ⊥-elim ( nat-≡< lem00 (lem03 _ _ _ refl lem01 lem02 ti) ) where
-   lem01 : node key₁ value₁ t₁ t₂ ≡ left
-   lem01 = just-injective ( cong node-left eq )
-   lem02 : node key₃ value₃ t₃ t₄ ≡ right
-   lem02 = just-injective ( cong node-right eq )
-   lem00 : key₁ ≡ key₃
-   lem00 = begin
-      key₁ ≡⟨ just-injective ( begin
-         just key₁  ≡⟨ cong node-key lem01 ⟩
-         node-key left ≡⟨ cong node-key eq1 ⟩
-         node-key right ≡⟨ cong node-key (sym lem02) ⟩
-         just key₃ ∎ ) ⟩
-      key₃ ∎ where open ≡-Reasoning
-   lem03 :  (key₁ key₃ : ℕ) → (tr : bt A) → tr ≡ node key₂ value₂ (node key₁ value₁ t₁ t₂) (node key₃ value₃ t₃ t₄)
-      → node key₁ value₁ t₁ t₂ ≡ left
-      → node key₃ value₃ t₃ t₄ ≡ right
-      → treeInvariant tr → key₁ < key₃
-   lem03 _ _ .leaf () _ _ t-leaf
-   lem03 _ _ .(node _ _ leaf leaf) () _ _ (t-single _ _)
-   lem03 _ _ .(node _ _ (node _ _ _ _) leaf) () _ _ (t-left _ _ _ _ _ _)
-   lem03 _ _ .(node _ _ leaf (node _ _ _ _)) () _ _ (t-right _ _ _ _ _ _)
-   lem03 key₁ key₃ (node key _ (node _ _ _ _) (node _ _ _ _)) eq3 el er (t-node key₄ key₅ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = lem04 where
-       lem04 : key₁ < key₃
-       lem04 = begin
-         suc key₁ ≡⟨ cong suc ( just-injective (cong node-key (just-injective (cong node-left (sym eq3)) ) ) ) ⟩
-         suc key₄ ≤⟨ <-trans x x₁ ⟩
-         key₂ ≡⟨ just-injective (cong node-key (just-injective (cong node-right eq3) ) )  ⟩
-         key₃ ∎ where open ≤-Reasoning
-
-si-property-< :  {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack  : List (bt A)}
-   → ¬ ( tree ≡ leaf )
-   → treeInvariant (node kp value₂ tree  tree₃ )
-   → stackInvariant key tree orig (tree ∷ node kp value₂ tree  tree₃ ∷ stack)
-   → key < kp
-si-property-< {n} {A} {key} {kp} {value₂} {tree} {orig} {tree₃} {stack} ne ti si =
-       lem00 (node kp value₂ tree  tree₃ ) (tree ∷ node kp value₂ tree  tree₃ ∷ stack) refl refl ti si where
-    lem00 : (tree1 : bt A) → (st : List (bt A)) →  (tree1 ≡ (node kp value₂ tree  tree₃ )) → (st ≡ tree ∷ node kp value₂ tree  tree₃ ∷ stack)
-       → treeInvariant tree1 → stackInvariant key tree orig st → key < kp
-    lem00 tree1 .(tree ∷ []) teq () ti s-nil
-    lem00 tree1 .(tree ∷ node key₁ v1 tree₁ tree ∷ []) teq seq ti₁ (s-right .tree .(node key₁ v1 tree₁ tree) tree₁ {key₁} {v1} x s-nil) = lem01 where
-        lem02 :  node key₁ v1 tree₁ tree  ≡ node kp value₂ tree tree₃
-        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
-        lem03 : tree₁ ≡ tree
-        lem03 = just-injective (cong node-left lem02)
-        lem01 : key < kp
-        lem01 = ⊥-elim ( ti-property2 (sym lem02) lem03 (case2 ne) ti )
-    lem00 tree1 .(tree ∷ node key₁ v1 tree₁ tree ∷ _) teq seq ti₁ (s-right .tree .orig tree₁ {key₁} {v1} x (s-right .(node _ _ tree₁ tree) .orig tree₂ {key₂} {v2} x₁ si)) = lem01 where
-        lem02 :  node key₁ v1 tree₁ tree  ≡ node kp value₂ tree tree₃
-        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
-        lem03 : tree₁ ≡ tree
-        lem03 = just-injective (cong node-left lem02)
-        lem01 : key < kp
-        lem01 = ⊥-elim ( ti-property2 (sym lem02) lem03 (case2 ne) ti )
-    lem00 tree1 (tree₂ ∷ node key₁ v1 tree₁ tree₂ ∷ _) teq seq ti₁ (s-right .tree₂ .orig tree₁ {key₁} {v1} x (s-left .(node _ _ tree₁ tree₂) .orig tree x₁ si)) = lem01 where
-        lem02 :  node key₁ v1 tree₁ tree₂ ≡ node kp value₂ tree₂ tree₃
-        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
-        lem03 : tree₁ ≡ tree₂
-        lem03 = just-injective (cong node-left lem02 )
-        lem01 : key < kp
-        lem01 = ⊥-elim ( ti-property2 (sym lem02) lem03 (case2 ne) ti )
-    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-left .tree₁ .(node _ _ tree₁ tree) tree {key₁} {v1} x s-nil) = subst( λ k → key < k ) lem03 x where
-        lem03 : key₁ ≡ kp
-        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
-    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-left .tree₁ .orig tree {key₁} {v1} x (s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) = subst( λ k → key < k ) lem03 x where
-        lem03 : key₁ ≡ kp
-        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
-    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-left .tree₁ .orig tree {key₁} {v1} x (s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) = subst( λ k → key < k ) lem03 x where
-        lem03 : key₁ ≡ kp
-        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
-
-si-property-> :  {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack  : List (bt A)}
-   → ¬ ( tree ≡ leaf )
-   → treeInvariant (node kp value₂ tree₃  tree )
-   → stackInvariant key tree orig (tree ∷ node kp value₂ tree₃  tree ∷ stack)
-   → kp < key
-si-property-> {n} {A} {key} {kp} {value₂} {tree} {orig} {tree₃} {stack} ne ti si =
-       lem00 (node kp value₂ tree₃  tree ) (tree ∷ node kp value₂ tree₃  tree ∷ stack) refl refl ti si where
-    lem00 : (tree1 : bt A) → (st : List (bt A)) →  (tree1 ≡ (node kp value₂ tree₃  tree )) → (st ≡ tree ∷ node kp value₂ tree₃  tree ∷ stack)
-       → treeInvariant tree1 → stackInvariant key tree orig st → kp < key
-    lem00 tree1 .(tree ∷ []) teq () ti s-nil
-    lem00 tree1 .(tree ∷ node key₁ v1 tree tree₁ ∷ []) teq seq ti₁ (s-left .tree .(node key₁ v1 tree tree₁) tree₁ {key₁} {v1} x s-nil) = lem01 where
-        lem02 :  node key₁ v1 tree tree₁  ≡ node kp value₂ tree₃ tree
-        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
-        lem03 : tree₁ ≡ tree
-        lem03 = just-injective (cong node-right lem02)
-        lem01 : kp < key
-        lem01 = ⊥-elim ( ti-property2 (sym lem02) (sym lem03) (case1 ne) ti )
-    lem00 tree1 .(tree ∷ node key₁ v1 tree tree₁ ∷ _) teq seq ti₁ (s-left .tree .orig tree₁ {key₁} {v1} x (s-left .(node _ _ tree tree₁) .orig tree₂ {key₂} {v2} x₁ si)) = lem01 where
-        lem02 :  node key₁ v1 tree tree₁  ≡ node kp value₂ tree₃ tree
-        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
-        lem03 : tree₁ ≡ tree
-        lem03 = just-injective (cong node-right lem02)
-        lem01 : kp < key
-        lem01 = ⊥-elim ( ti-property2 (sym lem02) (sym lem03) (case1 ne) ti )
-    lem00 tree1 (tree₂ ∷ node key₁ v1 tree₂ tree₁ ∷ _) teq seq ti₁ (s-left .tree₂ .orig tree₁ {key₁} {v1} x (s-right .(node _ _ tree₂ tree₁) .orig tree x₁ si)) = lem01 where
-        lem02 :  node key₁ v1 tree₂ tree₁  ≡ node kp value₂ tree₃ tree₂
-        lem02 = ∷-injectiveˡ ( ∷-injectiveʳ seq )
-        lem03 : tree₁ ≡ tree₂
-        lem03 = just-injective (cong node-right lem02)
-        lem01 : kp < key
-        lem01 = ⊥-elim ( ti-property2 (sym lem02) (sym lem03) (case1 ne) ti )
-    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-right .tree₁ .(node _ _ tree tree₁) tree {key₁} {v1} x s-nil) = subst( λ k → k < key ) lem03 x where
-        lem03 : key₁ ≡ kp
-        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
-    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-right .tree₁ .orig tree {key₁} {v1} x (s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) = subst( λ k → k < key ) lem03 x where
-        lem03 : key₁ ≡ kp
-        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
-    lem00 tree1 (tree₁ ∷ _) teq seq ti₁ (s-right .tree₁ .orig tree {key₁} {v1} x (s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) = subst( λ k → k < key ) lem03 x where
-        lem03 : key₁ ≡ kp
-        lem03 = just-injective (cong node-key (∷-injectiveˡ ( ∷-injectiveʳ seq )))
-
-
-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 {n} {A} key tree .tree .(tree ∷ []) s-nil = refl
-si-property-last {n} {A} key tree tree0 (tree ∷ []) (s-right .tree .tree0 tree₁ x si) = ⊥-elim ( si-property0 si refl )
-si-property-last {n} {A} key tree tree0 (tree ∷ x₁ ∷ st) (s-right .tree .tree0 tree₁ x si) = 
-   si-property-last key _ tree0 (x₁ ∷ st)  si
-si-property-last {n} {A} key tree tree0 (tree ∷ []) (s-left .tree .tree0 tree₁ x si) = ⊥-elim ( si-property0 si refl )
-si-property-last {n} {A} key tree tree0 (tree ∷ x₁ ∷ st) (s-left .tree .tree0 tree₁ x si) = 
-   si-property-last key _ tree0 (x₁ ∷ st)  si
-
-si-property-pne :  {n : Level} {A : Set n}  {key key₁ : ℕ} {value₁ : A} (tree orig : bt A) → {left right x : bt A} → (stack  : List (bt A)) {rest : List (bt A)}
-    → stack ≡ x ∷ node key₁ value₁ left right ∷ rest
-    → stackInvariant key tree orig stack
-    → ¬ ( key ≡ key₁ )
-si-property-pne {_} {_} {key} {key₁} {value₁} tree orig {left} {right} (tree ∷ tree1 ∷ st) seq (s-right .tree .orig tree₁ {key₂} {v₂} x si) eq 
-    = ⊥-elim ( nat-≡< lem00 x ) where
-      lem01 : tree1 ≡ node key₂ v₂ tree₁ tree 
-      lem01 = si-property1 si
-      lem02 : node key₁ value₁ left right ≡ node key₂ v₂ tree₁ tree 
-      lem02 = trans ( ∷-injectiveˡ (∷-injectiveʳ (sym seq) ) ) lem01
-      lem00 : key₂ ≡ key
-      lem00 = trans (just-injective (cong node-key (sym lem02))) (sym eq)
-si-property-pne {_} {_} {key} {key₁} {value₁} tree orig {left} {right} (tree ∷ tree1 ∷ st) seq (s-left tree orig tree₁ {key₂} {v₂} x si) eq 
-    = ⊥-elim ( nat-≡< (sym lem00) x ) where
-      lem01 : tree1 ≡ node key₂ v₂ tree tree₁
-      lem01 = si-property1 si
-      lem02 : node key₁ value₁ left right ≡ node key₂ v₂ tree tree₁
-      lem02 = trans ( ∷-injectiveˡ (∷-injectiveʳ (sym seq) ) ) lem01
-      lem00 : key₂ ≡ key
-      lem00 = trans (just-injective (cong node-key (sym  lem02))) (sym eq)
-si-property-pne {_} {_} {key} {key₁} {value₁} tree .tree {left} {right} .(tree ∷ []) () s-nil eq
-
-
--- si-property-parent-node :  {n : Level} {A : Set n}  {key : ℕ}  (tree orig : bt A) {x : bt A}
---     → (stack  : List (bt A)) {rest : List (bt A)}
---     → stackInvariant key tree orig stack
---     → ¬ ( stack ≡ x ∷ leaf ∷ rest )
--- si-property-parent-node {n} {A} tree orig = ?
-
-
-rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
-rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
-rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
-rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = λ ()
-rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = λ ()
-
-rt-property-leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {repl : bt A} → replacedTree key value leaf repl → repl ≡ node key value leaf leaf
-rt-property-leaf {n} {A} {key} {value} {repl} rt = lem00 leaf refl rt where
-   lem00 : (tree : bt A) → tree ≡ leaf → replacedTree key value tree repl → repl ≡ node key value leaf leaf
-   lem00 leaf eq r-leaf = refl
-   lem00 .(node key _ _ _) () r-node
-   lem00 .(node _ _ _ _) () (r-right x rt)
-   lem00 .(node _ _ _ _) () (r-left x rt)
-
-rt-property-¬leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {tree : bt A} → ¬ replacedTree key value tree leaf
-rt-property-¬leaf ()
-
-rt-property-key : {n : Level} {A : Set n} {key key₂ key₃ : ℕ} {value value₂ value₃ : A} {left left₁ right₂ right₃ : bt A}
-    →  replacedTree key value (node key₂ value₂ left right₂) (node key₃ value₃ left₁ right₃) → key₂ ≡ key₃
-rt-property-key {n} {A} {key} {key₂} {key₃} {value} {value₂} {value₃} {left} {left₁} {right₂} {right₃} rt 
-      = lem00 (node key₂ value₂ left right₂) (node key₃ value₃ left₁ right₃) refl refl rt where
-    lem00 : (tree tree1 : bt A) → tree ≡ node key₂ value₂ left right₂ → tree1 ≡  node key₃ value₃ left₁ right₃ → replacedTree key value tree tree1 → key₂ ≡ key₃
-    lem00 _ _ () eq2 r-leaf
-    lem00 _ _ eq1 eq2 r-node = trans (just-injective (cong node-key (sym eq1))) (just-injective (cong node-key eq2))
-    lem00 _ _ eq1 eq2 (r-right x rt1) = trans (just-injective (cong node-key (sym eq1))) (just-injective (cong node-key eq2))
-    lem00 _ _ eq1 eq2 (r-left x rt1) = trans (just-injective (cong node-key (sym eq1))) (just-injective (cong node-key eq2))
-
+open import BTree 
 
 open _∧_
 
-
-depth-1< : {i j : ℕ} →   suc i ≤ suc (i Data.Nat.⊔ j )
-depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
-
-depth-2< : {i j : ℕ} →   suc i ≤ suc (j Data.Nat.⊔ i )
-depth-2< {i} {j} = s≤s (m≤n⊔m j i)
-
-depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
-depth-3< {zero} = s≤s ( z≤n )
-depth-3< {suc i} = s≤s (depth-3< {i} )
-
-
-treeLeftDown  : {n : Level} {A : Set n} {k : ℕ} {v1 : A}  → (tree tree₁ : bt A )
-      → treeInvariant (node k v1 tree tree₁)
-      →      treeInvariant tree
-treeLeftDown {n} {A} {k} {v1} tree tree₁ ti = lem00 (node k v1 tree tree₁) refl ti  where
-    lem00 : ( tr : bt A ) → tr ≡ node k v1 tree tree₁ → treeInvariant tr → treeInvariant tree
-    lem00 .leaf () t-leaf
-    lem00 .(node key value leaf leaf) eq (t-single key value) = subst (λ k → treeInvariant k ) (just-injective (cong node-left eq)) t-leaf
-    lem00 .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ x x₁ x₂ ti) = subst (λ k → treeInvariant k ) (just-injective (cong node-left eq)) t-leaf
-    lem00 .(node key₁ _ (node key _ _ _) leaf) eq (t-left key key₁ x x₁ x₂ ti) = subst (λ k → treeInvariant k ) (just-injective (cong node-left eq)) ti
-    lem00 .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) eq (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = subst (λ k → treeInvariant k ) (just-injective (cong node-left eq)) ti
-
-treeRightDown  : {n : Level} {A : Set n} {k : ℕ} {v1 : A}  → (tree tree₁ : bt A )
-      → treeInvariant (node k v1 tree tree₁)
-      →      treeInvariant tree₁
-treeRightDown {n} {A} {k} {v1} tree tree₁ ti = lem00 (node k v1 tree tree₁) refl ti  where
-    lem00 : ( tr : bt A ) → tr ≡ node k v1 tree tree₁ → treeInvariant tr → treeInvariant tree₁
-    lem00 .leaf () t-leaf
-    lem00 .(node key value leaf leaf) eq (t-single key value) = subst (λ k → treeInvariant k ) (just-injective (cong node-right eq)) t-leaf
-    lem00 .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ x x₁ x₂ ti) = subst (λ k → treeInvariant k ) (just-injective (cong node-right eq)) ti
-    lem00 .(node key₁ _ (node key _ _ _) leaf) eq (t-left key key₁ x x₁ x₂ ti) = subst (λ k → treeInvariant k ) (just-injective (cong node-right eq)) t-leaf
-    lem00 .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) eq (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = subst (λ k → treeInvariant k ) (just-injective (cong node-right eq)) ti₁
-
-
-ti-property1 :  {n : Level} {A : Set n} {key₁ : ℕ} {value₂ : A} {left right : bt A} → treeInvariant (node key₁ value₂  left right ) →   tr< key₁ left ∧  tr> key₁ right
-ti-property1 {n} {A} {key₁} {value₂} {left} {right} ti = lem00 key₁ (node key₁ value₂ left right) refl ti where
-    lem00 : (key₁ : ℕ) → ( tree : bt A ) → tree ≡ node key₁ value₂ left right → treeInvariant tree → tr< key₁ left ∧  tr> key₁ right
-    lem00 - .leaf () t-leaf
-    lem00 key₁ .(node key value leaf leaf) eq (t-single key value) = subst₂ (λ j k → tr< key₁ j ∧ tr> key₁ k ) lem01 lem02 ⟪ tt , tt ⟫ where
-         lem01 : leaf ≡ left
-         lem01 = just-injective (cong node-left eq)
-         lem02 : leaf ≡ right
-         lem02 = just-injective (cong node-right eq)
-    lem00 key₂ .(node key _ leaf (node key₁ _ _ _)) eq (t-right key key₁ {value} {value₁} {t₁} {t₂} x x₁ x₂ ti) 
-         = subst₂ (λ j k → tr< key₂ j ∧ tr> key₂ k ) lem01 lem02 ⟪ tt , ⟪ subst (λ k → k < key₁) lem04 x , 
-              ⟪ subst (λ k → tr> k t₁) lem04 x₁ , subst (λ k → tr> k t₂) lem04 x₂ ⟫  ⟫ ⟫ where
-         lem01 : leaf ≡ left
-         lem01 = just-injective (cong node-left eq)
-         lem02 : node key₁ value₁ t₁ t₂ ≡ right
-         lem02 = just-injective (cong node-right eq)
-         lem04 : key ≡ key₂
-         lem04 = just-injective (cong node-key eq)
-    lem00 key₂ .(node key₁ _ (node key _ _ _) leaf) eq (t-left key key₁ {value} {value₁} {t₁} {t₂} x x₁ x₂ ti) 
-         = subst₂ (λ j k → tr< key₂ j ∧ tr> key₂ k ) lem02 lem01 ⟪ ⟪ subst (λ k → key < k) lem04 x , 
-              ⟪ subst (λ k → tr< k t₁) lem04 x₁  , subst (λ k → tr< k t₂) lem04 x₂  ⟫  ⟫ , tt ⟫ where
-         lem01 : leaf ≡ right
-         lem01 = just-injective (cong node-right eq)
-         lem02 : node key value t₁ t₂ ≡ left
-         lem02 = just-injective (cong node-left eq)
-         lem04 : key₁ ≡ key₂
-         lem04 = just-injective (cong node-key eq)
-    lem00 key₂ .(node key₁ _ (node key _ _ _) (node key₃ _ _ _)) eq (t-node key key₁ key₃ {value} {value₁} {value₂} 
-      {t₁} {t₂} {t₃} {t₄} x x₁ x₂ x₃ x₄ x₅ ti ti₁) 
-        = subst₂ (λ j k → tr< key₂ j ∧ tr> key₂ k ) lem01 lem02 ⟪ ⟪ subst (λ k → key < k) lem04 x , 
-             ⟪ subst (λ k → tr< k t₁) lem04 x₂ , subst (λ k → tr< k t₂) lem04 x₃ ⟫ ⟫   
-           , ⟪ subst (λ k → k < key₃) lem04 x₁  , ⟪  subst (λ k → tr> k t₃) lem04 x₄   , subst (λ k → tr> k t₄) lem04 x₅  ⟫  ⟫ ⟫ where
-         lem01 : node key value t₁ t₂  ≡ left
-         lem01 = just-injective (cong node-left eq)
-         lem02 : node key₃ value₂ t₃ t₄  ≡ right
-         lem02 = just-injective (cong node-right eq)
-         lem04 : key₁ ≡ key₂
-         lem04 = just-injective (cong node-key eq)
-
-
-findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
-           →  treeInvariant tree ∧ stackInvariant key tree tree0 stack
-           → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
-                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
-findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl)
-findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
-findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
-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<
-
-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 = ?
-
-open import Relation.Binary.Definitions
-
-child-replaced :  {n : Level} {A : Set n} (key : ℕ)   (tree : bt A) → bt A
-child-replaced key leaf = leaf
-child-replaced key (node key₁ value left right) with <-cmp key key₁
-... | tri< a ¬b ¬c = left
-... | tri≈ ¬a b ¬c = node key₁ value left right
-... | tri> ¬a ¬b c = right
-
-child-replaced-left :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}
-   → key < key₁
-   → child-replaced key (node key₁ value left right) ≡ left
-child-replaced-left {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
-     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key < key₁ → child-replaced key tree ≡ left
-     ch00 = ?
-
-child-replaced-right :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}
-   → key₁ < key
-   → child-replaced key (node key₁ value left right) ≡ right
-child-replaced-right {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
-     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ < key → child-replaced key tree ≡ right
-     ch00 tree eq lt1 with <-cmp key key₁
-     ... | tri< a ¬b ¬c = ⊥-elim (¬c ?)
-     ... | tri≈ ¬a b ¬c = ⊥-elim (¬c ?)
-     ... | tri> ¬a ¬b c = ?
-
-child-replaced-eq :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}
-   → key₁ ≡ key
-   → child-replaced key (node key₁ value left right) ≡ node key₁ value left right
-child-replaced-eq {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
-     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ ≡ key → child-replaced key tree ≡ node key₁ value left right
-     ch00 tree eq lt1 with <-cmp key key₁
-     ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym ?))
-     ... | tri≈ ¬a b ¬c = ?
-     ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym ?))
-
-open _∧_
-
-ri-tr>  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key key₁ : ℕ) → (value : A)
-     → replacedTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl
-ri-tr> .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫
-ri-tr> .(node key _ _ _) .(node key value _ _) key key₁ value r-node a tgt = ⟪ a , ⟪ proj1 (proj2 tgt) , proj2 (proj2 tgt) ⟫ ⟫
-ri-tr> .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-right x ri) a tgt = ⟪ proj1 tgt , ⟪ proj1 (proj2 tgt) , ri-tr> _ _ _ _ _ ri a (proj2 (proj2 tgt)) ⟫ ⟫
-ri-tr> .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-left x ri) a tgt = ⟪ proj1 tgt , ⟪  ri-tr> _ _ _ _ _ ri a (proj1 (proj2 tgt)) , proj2 (proj2 tgt)  ⟫ ⟫
-
-ri-tr<  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key key₁ : ℕ) → (value : A)
-     → replacedTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl
-ri-tr< .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫
-ri-tr< .(node key _ _ _) .(node key value _ _) key key₁ value r-node a tgt = ⟪ a , ⟪ proj1 (proj2 tgt) , proj2 (proj2 tgt) ⟫ ⟫
-ri-tr< .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-right x ri) a tgt = ⟪ proj1 tgt , ⟪ proj1 (proj2 tgt) , ri-tr< _ _ _ _ _ ri a (proj2 (proj2 tgt)) ⟫ ⟫
-ri-tr< .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-left x ri) a tgt = ⟪ proj1 tgt , ⟪  ri-tr< _ _ _ _ _ ri a (proj1 (proj2 tgt)) , proj2 (proj2 tgt)  ⟫ ⟫
-
-<-tr>  : {n : Level} {A : Set n}  → {tree : bt A} → {key₁ key₂ : ℕ} → tr> key₁ tree → key₂ < key₁  → tr> key₂ tree
-<-tr> {n} {A} {leaf} {key₁} {key₂} tr lt = tt
-<-tr> {n} {A} {node key value t t₁} {key₁} {key₂} tr lt = ⟪ <-trans lt (proj1 tr) , ⟪ <-tr> (proj1 (proj2 tr)) lt , <-tr> (proj2 (proj2 tr)) lt ⟫ ⟫
-
->-tr<  : {n : Level} {A : Set n}  → {tree : bt A} → {key₁ key₂ : ℕ} → tr< key₁ tree → key₁ < key₂  → tr< key₂ tree
->-tr<  {n} {A} {leaf} {key₁} {key₂} tr lt = tt
->-tr<  {n} {A} {node key value t t₁} {key₁} {key₂} tr lt = ⟪ <-trans (proj1 tr) lt , ⟪ >-tr< (proj1 (proj2 tr)) lt , >-tr< (proj2 (proj2 tr)) lt ⟫ ⟫
-
-RTtoTI0  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
-     → replacedTree key value tree repl → treeInvariant repl
-RTtoTI0 = ?
-
---   RTtoTI0 .(node key _ leaf leaf) .(node key value leaf leaf) key value = ?
---   RTtoTI0 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right _ _ x a b ti) r-node = t-right _ _ x a b ti
---   RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left _ _ x a b ti) r-node = t-left _ _ x a b ti
---   RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node _ _ _ x x₁ a b c d ti ti₁) r-node = t-node _ _ _ x x₁ a b c d ti ti₁
---   -- r-right case
---   RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right _ _ x _ _ (t-single key value)
---   RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right _ _ x₁ a b ti) (r-right x ri) = t-single key₁ value₁
---   RTtoTI0 (node key₁ _ leaf right@(node key₂ _ left₁ right₁)) (node key₁ value₁ leaf right₃@(node key₃ _ left₂ right₂)) key value (t-right key₄ key₅ x₁ a b ti) (r-right x ri) =
---         t-right _ _ (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) (rr00 ri a ) (rr02 ri b) (RTtoTI0 right right₃ key value ti ri) where
---            rr00 : replacedTree key value (node key₂ _ left₁ right₁) (node key₃ _ left₂ right₂) → tr> key₁ left₁ → tr> key₁ left₂
---            rr00 = ?
---            rr02 : replacedTree key value (node key₂ _ left₁ right₁) (node key₃ _ left₂ right₂) → tr> key₁ right₁ → tr> key₁ right₂
---            rr02 = ?
---   RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left _ _ x₁ a b ti) (r-right x ())
---   RTtoTI0 (node key₁ _ (node key₃ _ _ _) leaf) (node key₁ _ (node key₃ value₃ _ _) (node key value leaf leaf)) key value (t-left _ _ x₁ a b ti) (r-right x r-leaf) =
---         t-node _ _ _ x₁ x a b tt tt ti (t-single key value)
---   RTtoTI0 (node key₁ _ (node _ _ left₀ right₀) (node key₂ _ left₁ right₁)) (node key₁ _ (node _ _ left₂ right₂) (node key₃ _ left₃ right₃)) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-right x ri) =
---         t-node _ _ _ x₁ (subst (λ k → key₁ < k ) (rt-property-key ri) x₂) a b (rr00 ri c) (rr02 ri d) ti (RTtoTI0 _ _ key value ti₁ ri) where
---            rr00 : replacedTree key value (node key₂ _ _ _) (node key₃ _ _ _) → tr> key₁ left₁ → tr> key₁ left₃
---            rr00 = ?
---            rr02 : replacedTree key value (node key₂ _ _ _) (node key₃ _ _ _) → tr> key₁ right₁ → tr> key₁ right₃
---            rr02 = ?
---   -- r-left case
---   RTtoTI0 .(node _ _ leaf leaf) .(node _ _ (node key value leaf leaf) leaf) key value (t-single _ _) (r-left x r-leaf) = t-left _ _ x tt tt (t-single _ _ )
---   RTtoTI0 .(node _ _ leaf (node _ _ _ _)) (node key₁ value₁ (node key value leaf leaf) (node _ _ _ _)) key value (t-right _ _ x₁ a b ti) (r-left x r-leaf) =
---         t-node _ _ _ x x₁ tt tt a b (t-single key value) ti
---   RTtoTI0 (node key₃ _ (node key₂ _ left₁ right₁) leaf) (node key₃ _ (node key₁ value₁ left₂ right₂) leaf) key value (t-left _ _ x₁ a b ti) (r-left x ri) =
---         t-left _ _ (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) (rr00 ri a) (rr02 ri b) (RTtoTI0 _ _ key value ti ri) where -- key₁ < key₃
---            rr00 : replacedTree key value (node key₂ _ left₁ right₁) (node key₁ _ left₂ right₂) → tr< key₃ left₁ → tr< key₃ left₂
---            rr00 = ?
---            rr02 : replacedTree key value (node key₂ _ left₁ right₁) (node key₁ _ left₂ right₂) → tr< key₃ right₁ → tr< key₃ right₂
---            rr02 = ?
---   RTtoTI0 (node key₁ _ (node key₂ _ left₂ right₂) (node key₃ _ left₃ right₃)) (node key₁ _ (node key₄ _ left₄ right₄) (node key₅ _ left₅ right₅)) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-left x ri) =
---         t-node _ _ _ (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂  (rr00 ri a) (rr02 ri b) c d (RTtoTI0 _ _ key value ti ri) ti₁ where
---            rr00 : replacedTree key value (node key₂ _ left₂ right₂) (node key₄ _ left₄ right₄) → tr< key₁ left₂ → tr< key₁ left₄
---            rr00 = ?
---            rr02 : replacedTree key value (node key₂ _ left₂ right₂) (node key₄ _ left₄ right₄) → tr< key₁ right₂ → tr< key₁ right₄
---            rr02 = ?
---
--- RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
---      → replacedTree key value tree repl → treeInvariant tree
--- RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf
--- RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁
--- RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right _ _ x a b ti) r-node = t-right _ _ x a b ti
--- RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left _ _ x a b ti) r-node = t-left _ _ x a b ti
--- RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node _ _ _ x x₁ a b c d ti ti₁) r-node = t-node _ _ _ x x₁ a b c d ti ti₁
--- -- r-right case
--- RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right _ _ x₁ a b ti) (r-right x r-leaf) = t-single key₁ value₁
--- RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right _ _ x₁ a b ti) (r-right x ri) =
---    t-right _ _ (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) ? ?  (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂
--- RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-right x r-leaf) =
---     t-left _ _ x₁ ? ? ti
--- RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node _ _ _ x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) a b ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁
--- -- r-left case
--- RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left _ _ x₁ a b ti) (r-left x ri) = t-single key₁ value₁
--- RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left _ _ x₁ a b ti) (r-left x ri) =
---    t-left _ _ (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁
--- RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right _ _ x₂ c d ti₁
--- RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-left x ri) =
---     t-node _ _ _ (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? c d (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
-
-popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt A))
-           → ( tree parent orig : bt A) →  (key : ℕ)
-           → stackInvariant key tree  orig ( tree ∷ parent ∷ rest )
-           → stackInvariant key parent orig (parent ∷ rest )
-popStackInvariant rest tree parent orig key = ?
-
-siToTreeinvariant : {n : Level} {A : Set n} → (rest : List ( bt A))
-           → ( tree orig : bt A) →  (key : ℕ)
-           → treeInvariant orig
-           → stackInvariant key tree  orig ( tree ∷ rest )
-           → treeInvariant tree
-siToTreeinvariant = ?
-
-record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
-   field
-     tree0 : bt A
-     ti : treeInvariant tree0
-     si : stackInvariant key tree tree0 stack
-     ri : replacedTree key value (child-replaced key tree ) repl
-     rti : treeInvariant repl
-     ci : C tree repl stack     -- data continuation
-
-replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
-    → (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 = ?
---   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)
---        (subst (λ j → replacedTree k v1 j  (node k v1 t t₁) ) repl00 r-node) where
---            repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁)
---            repl00 with <-cmp k k
---            ... | tri< a ¬b ¬c = ⊥-elim (¬b refl)
---            ... | tri≈ ¬a b ¬c = refl
---            ... | tri> ¬a ¬b c = ⊥-elim (¬b refl)
---
-
-replaceP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A)
-     → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤)
-     → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
-         → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
-     → (exit : (tree1 repl : bt A) → treeInvariant repl ∧ replacedTree key value tree1 repl → t) → t
-replaceP key value {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
-replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (replacePR.si Pre)-- tree0 ≡ leaf
-... | eq  =  exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ t-single _ _  ,  ? ⟫
-replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right )
-        ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where
-    repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right )
-    -- repl01 = ? --with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)
-    repl01 = ? where
-    -- | refl | refl = subst (λ k → replacedTree key value  (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where
-        repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
-        repl03 = replacePR.ri ?
-        repl02 : child-replaced key (node key₁ value₁ left right) ≡ left
-        repl02 with <-cmp key key₁
-        ... | tri< a ¬b ¬c = refl
-        ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a)
-        ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a)
-... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪  RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where
-    repl01 : replacedTree key value (replacePR.tree0 Pre) repl
-    --repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)
-    repl01 = ? where
-    --repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where
-        repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right
-        repl02 with <-cmp key key₁
-        ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b)
-        ... | tri≈ ¬a b ¬c = refl
-        ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b)
-... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl  ) ⟪  RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where
-    repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl )
-    -- repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)
-    repl01 = ? where
-    -- repl01 | refl | refl = subst (λ k → replacedTree key value  (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where
-        repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
-        repl03 = replacePR.ri ?
-        repl02 : child-replaced key (node key₁ value₁ left right) ≡ right
-        repl02 with <-cmp key key₁
-        ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c)
-        ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c)
-        ... | tri> ¬a ¬b c = refl
-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 = ? -- where with replacePR.si Pre
---   -- ... | s-right  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ;
---          rti = replacePR.rti Pre ; ci = lift tt } where
---       repl09 : tree1 ≡ node key₂ v1 tree₁ leaf
---       repl09 = si-property1 si
---       repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
---       repl10 with si-property1 si
---       ... | refl = si
---       repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf
---       repl07 with <-cmp key key₂
---       ... |  tri< a ¬b ¬c = ⊥-elim (¬c x)
---       ... |  tri≈ ¬a b ¬c = ⊥-elim (¬c x)
---       ... |  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 ; rti = replacePR.rti Pre ; 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)
---       repl10 with si-property1 si
---       ... | refl = si
---       repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf
---       repl07 with <-cmp key key₂
---       ... |  tri< a ¬b ¬c = refl
---       ... |  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
-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 ⊤)
-    Post = ? -- with replacePR.si Pre
---    ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10
---      ; rti = repl13
---      ; 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)
---        repl10 with si-property1 si
---        ... | refl = si
---        repl11 : stackInvariant key (node key₂ v1 tree₁ (node key₁ value₁ left right)) (replacePR.tree0 Pre) (node key₂ v1 tree₁ (node key₁ value₁ left right)∷ st1)
---        repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10
---        repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
---        repl03 with <-cmp key key₁
---        ... | tri< a1 ¬b ¬c = refl
---        ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
---        ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
---        repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
---        repl02 with repl09 | <-cmp key key₂
---        ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
---        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
---        ... | refl | tri> ¬a ¬b c = refl
---        repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
---        repl04  = begin
---            node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03  ⟩
---            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
---            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
---            child-replaced key tree1 ∎  where open ≡-Reasoning
---        repl05 : node key₁ value₁ left right ≡ child-replaced key tree1
---        repl05  = begin
---            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
---            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
---            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))
---        repl13 : treeInvariant (node key₁ value₁ repl right)
---        repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeRightDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12
---    ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; 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)
---        repl10 with si-property1 si
---        ... | refl = si
---        repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
---        repl03 with <-cmp key key₁
---        ... | tri< a1 ¬b ¬c = refl
---        ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
---        ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
---        repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
---        repl02 with repl09 | <-cmp key key₂
---        ... | refl | tri< a ¬b ¬c = refl
---        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
---        ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
---        repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
---        repl04  = begin
---            node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03  ⟩
---            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
---            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
---            child-replaced key tree1 ∎  where open ≡-Reasoning
---        repl05 : node key₁ value₁ left right ≡ child-replaced key tree1
---        repl05  = begin
---            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
---            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
---            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))
---        repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10
---        repl13 :  treeInvariant (node key₁ value₁ repl right)
---        repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeLeftDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12
-... | 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 ; rti = repl13 ; 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)
---        repl10 with si-property1 si
---        ... | refl = si
---        repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree
---        repl07 with <-cmp key key₂
---        ... |  tri< a ¬b ¬c = ⊥-elim (¬c x)
---        ... |  tri≈ ¬a b ¬c = ⊥-elim (¬c x)
---        ... |  tri> ¬a ¬b c = refl
---        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
---        repl13 : treeInvariant (node key₁ value left right)
---        repl13 = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (replacePR.si Pre))  r-node
---    ... | s-left  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; 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)
---        repl10 with si-property1 si
---        ... | refl = si
---        repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree
---        repl07 with <-cmp key key₂
---        ... |  tri< a ¬b ¬c = refl
---        ... |  tri≈ ¬a b ¬c = ⊥-elim (¬a x)
---        ... |  tri> ¬a ¬b c = ⊥-elim (¬a x)
---        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
---        repl13 : treeInvariant (node key₁ value left right)
---        repl13 = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (replacePR.si Pre))  r-node
-... | 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 ; rti = repl13 ; 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)
---        repl10 with si-property1 si
---        ... | refl = si
---        repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
---        repl03 with <-cmp key key₁
---        ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
---        ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
---        ... | tri> ¬a ¬b c = refl
---        repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
---        repl02 with repl09 | <-cmp key key₂
---        ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
---        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
---        ... | refl | tri> ¬a ¬b c = refl
---        repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
---        repl04  = begin
---            node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
---            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
---            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
---            child-replaced key tree1 ∎  where open ≡-Reasoning
---        repl05 : node key₁ value₁ left right ≡ child-replaced key tree1
---        repl05  = begin
---            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
---            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
---            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))
---        repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10
---        repl13 : treeInvariant (node key₁ value₁ left repl)
---        repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeRightDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12
---    ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; 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)
---        repl10 with si-property1 si
---        ... | refl = si
---        repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
---        repl03 with <-cmp key key₁
---        ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
---        ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
---        ... | tri> ¬a ¬b c = refl
---        repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
---        repl02 with repl09 | <-cmp key key₂
---        ... | refl | tri< a ¬b ¬c = refl
---        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
---        ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
---        repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
---        repl04  = begin
---            node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
---            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
---            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
---            child-replaced key tree1 ∎  where open ≡-Reasoning
---        repl05 : node key₁ value₁ left right ≡ child-replaced key tree1
---        repl05  = begin
---            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
---            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
---            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))
---        repl13 : treeInvariant (node key₁ value₁ left repl)
---        repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeLeftDown _ _
---           (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10)) )) repl12
-
-TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
-   → (r : Index) → (p : Invraiant r)
-   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t) → t
-TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
-... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim ? ) --
-... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where
-    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
-    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim ?) -- (lemma5 n≤j lt1))
-    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
-    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
-    ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
-    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )
-
-
-insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
-     → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t
-insertTreeP {n} {m} {A} {t} tree key value P0 exit =
-   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫  ⟪ P0 , s-nil ⟫
-       $ λ p P loop → findP key (proj1 p)  tree (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt )
-       $ λ t s P C → replaceNodeP key value t C (proj1 P)
-       $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
-            {λ p → replacePR key value  (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p)  (λ _ _ _ → Lift n ⊤ ) }
-               (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; rti = P1 ; ri = R ; ci = lift tt }
-       $  λ p P1 loop → replaceP key value  (proj2 (proj2 p)) (proj1 p) P1
-            (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1  ⟫ ⟫ P2 lt )
-       $ λ tree repl P → exit tree repl P
-
-insertTestP1 = insertTreeP leaf 1 1 t-leaf
-  $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0)
-  $ λ _ x1 P1 → insertTreeP x1 3 2 (proj1 P1)
-  $ λ _ x2 P2 → insertTreeP x2 2 2 (proj1 P2) (λ _ x P  → x )
-
-
-top-value : {n : Level} {A : Set n} → (tree : bt A) →  Maybe A
-top-value leaf = nothing
-top-value (node key value tree tree₁) = just value
-
--- is realy inserted?
-
--- other element is preserved?
-
--- deletion?
-
-
 data Color  : Set where
     Red : Color
     Black : Color