--- a/hoareBinaryTree.agda	Wed Dec 01 11:43:53 2021 +0900
+++ b/hoareBinaryTree.agda	Wed Dec 01 23:04:55 2021 +0900
@@ -97,7 +97,7 @@
     t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf) 
     t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → 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) → treeInvariant (node key value t₁ t₂)
+    t-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → 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₂)
        → treeInvariant (node key value t₁ t₂) 
@@ -128,12 +128,12 @@
         suc i + j ∎  where open ≤-Reasoning
 
 treeTest1  : bt ℕ
-treeTest1  =  node 1 0 leaf (node 3 1 (node 2 5 (node 4 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
+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 4 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
+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 _ 1) (t-node (add< 0) (add< 1) (t-left (add< 1) (t-single 4 7)) (t-single 5 5) )
+treeInvariantTest1  = t-right (m≤m+n _ 2) (t-node (add< 0) (add< 1) (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
@@ -145,7 +145,7 @@
 stack-last (x ∷ s) = stack-last s
 
 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
-stackInvariantTest1 = s-right (add< 2) (s-single  )
+stackInvariantTest1 = s-right (add< 3) (s-single  )
 
 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-single  ) ()
@@ -197,6 +197,12 @@
 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 r-leaf = refl
 
+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 r-node = refl
+rt-property-key (r-right x ri) = refl
+rt-property-key (r-left x ri) = refl
+
 depth-1< : {i j : ℕ} →   suc i ≤ suc (i Data.Nat.⊔ j )
 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
 
@@ -501,7 +507,23 @@
 
 RTtoTI0  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
      → replacedTree key value tree repl → treeInvariant repl
-RTtoTI0  = {!!}
+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 ti) r-node = t-right x ti 
+RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti 
+RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ ti ti₁) r-node = t-node x x₁ ti ti₁
+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₁ ti) (r-right x ri) = t-single key₁ value₁
+RTtoTI0 (node key₁ _ leaf right@(node key₂ _ _ _)) (node key₁ value₁ leaf right₁@(node key₃ _ _ _)) key value (t-right x₁ ti) (r-right x ri) = t-right rt2 rt1 where
+    rt2 : key₁ < key₃
+    rt2 = subst (λ k → key₁ < k ) (rt-property-key ri) x₁
+    rt1 : treeInvariant right₁   
+    rt1 = RTtoTI0 _ _ key value ti ri 
+RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ 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₁ ti) (r-right x r-leaf) =
+      t-node x₁ x ti (t-single key value) 
+RTtoTI0 .(node _ _ (node _ _ _ _) (node _ _ _ _)) .(node _ _ (node _ _ _ _) _) key value (t-node x₁ x₂ ti ti₁) (r-right x ri) = {!!}
+RTtoTI0 .(node _ _ _ _) .(node _ _ _ _) key value ti (r-left x ri) = {!!}
 
 RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
      → replacedTree key value tree repl → treeInvariant tree