# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1710403931 -32400
# Node ID 0b0a54d7d6832f9da7b5fb0d9141ac3964c0e3c0
# Parent  1cce147edddbedc6cae84e22e58fe58f195057ff
...

diff -r 1cce147edddb -r 0b0a54d7d683 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Tue Mar 05 16:25:47 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Mar 14 17:12:11 2024 +0900
@@ -54,17 +54,17 @@
 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₁ 
+    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₁ 
+    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₂
+    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₃
@@ -73,7 +73,6 @@
        → 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)
 --
@@ -103,9 +102,9 @@
 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) 
+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) )
+    ⟪ 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
@@ -197,17 +196,17 @@
       → treeInvariant (node k v1 tree tree₁)
       →      treeInvariant tree
 treeLeftDown {n} {A} {_} {v1} leaf leaf (t-single k1 v1) = t-leaf
-treeLeftDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x _ _ ti) = t-leaf
-treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x _ _ ti) = ti
-treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ _ _ _ _ ti ti₁) = ti
+treeLeftDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right _ _ x _ _ ti) = t-leaf
+treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left _ _ x _ _ ti) = ti
+treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node _ _ _ x x₁ _ _ _ _ ti ti₁) = 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} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf
-treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x _ _ ti) = ti
-treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x _ _ ti) = t-leaf
-treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ _ _ _ _ ti ti₁) = ti₁
+treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right _ _ x _ _ ti) = ti
+treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left _ _ x _ _ ti) = t-leaf
+treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node _ _ _ x x₁ _ _ _ _ ti ti₁) = ti₁
 
 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
@@ -225,9 +224,9 @@
 
 replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
-replaceTree1 k v1 value (t-right x a b t) = t-right x a b t
-replaceTree1 k v1 value (t-left x a b t) = t-left x a b t
-replaceTree1 k v1 value (t-node x x₁ a b c d t t₁) = t-node x x₁ a b c d t t₁
+replaceTree1 k v1 value (t-right _ _ x a b t) = t-right _ _ x a b t
+replaceTree1 k v1 value (t-left _ _ x a b t) = t-left _ _ x a b t
+replaceTree1 k v1 value (t-node _ _ _ x x₁ a b c d t t₁) = t-node _ _ _ x x₁ a b c d t t₁
 
 open import Relation.Binary.Definitions
 
@@ -494,57 +493,78 @@
 
 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)  ⟫ ⟫
+
+
 RTtoTI0  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
      → replacedTree key value tree repl → treeInvariant repl
 RTtoTI0 .leaf .(node key value leaf leaf) key value ti r-leaf = t-single key value
 RTtoTI0 .(node key _ leaf leaf) .(node key value leaf leaf) key value (t-single .key _) r-node = t-single 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₁
+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 x₁ a b ti) (r-right x ri) =
-      t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) rr00 ? (RTtoTI0 _ _ key value ti ri) where
-         rr00 : tr> key₁ left₂
-         rr00 with RTtoTI0 _ _ key value ti ri
-         ... | t-single key₃ value = tt
-         ... | t-right x x₁ x₂ t = tt
-         ... | t-left x₃ x₄ x₅ t = ?
-         ... | t-node x x₁ x₂ x₃ x₄ x₅ t t₁ = ?
-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 ? ? ? ? ti (t-single key value)
-RTtoTI0 (node key₁ _ (node _ _ _ _) (node key₂ _ _ _)) (node key₁ _ (node _ _ _ _) (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) (rt-property-key ri) x₂) a b ? ?  ti (RTtoTI0 _ _ key value ti₁ ri)
+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 r-node tb = tb
+         rr00 (r-right x ri) tb = tb
+         rr00 (r-left x₂ ri) tb = ri-tr> _ _ _ _ _ ri x tb
+         rr02 : replacedTree key value (node key₂ _ left₁ right₁) (node key₃ _ left₂ right₂) → tr> key₁ right₁ → tr> key₁ right₂  
+         rr02 r-node tb = tb
+         rr02 (r-right x₂ ri) tb = ri-tr> _ _ _ _ _ ri x tb
+         rr02 (r-left x ri) tb = tb
+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) ?  ti (RTtoTI0 _ _ key value ti₁ ri) where
+         rr00 : replacedTree key value (node key₂ _ _ _) (node key₃ _ _ _) → tr> key₂ left₁ → tr> key₃ left₃
+         rr00 r-node tb = tb
+         rr00 (r-right x₃ ri) tb = tb
+         rr00 (r-left x₃ ri) tb = ri-tr> _ _ _ _ _ ri ? tb
 -- 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 ? ? (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₁ ? ? ? ? (t-single key value) ti
-RTtoTI0 (node key₃ _ (node key₂ _ _ _) leaf) (node key₃ _ (node key₁ value₁ left left₁) leaf) key value (t-left x₁ a b ti) (r-left x ri) =
-      t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃
-RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) 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₂  ? ? c d (RTtoTI0 _ _ key value ti ri) ti₁
+RTtoTI0 .(node _ _ leaf leaf) .(node _ _ (node key value leaf leaf) leaf) key value (t-single _ _) (r-left x r-leaf) = t-left _ _ x ? ? (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₁ ? ? ? ? (t-single key value) ti
+RTtoTI0 (node key₃ _ (node key₂ _ _ _) leaf) (node key₃ _ (node key₁ value₁ left left₁) leaf) key value (t-left _ _ x₁ a b ti) (r-left x ri) =
+      t-left _ _ (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃
+RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) 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₂  ? ? c d (RTtoTI0 _ _ key value ti ri) ti₁
 
 -- 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₁
+-- 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₁
+-- 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₁
+-- 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₁
 
 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