--- a/hoareBinaryTree.agda	Fri Nov 19 20:07:09 2021 +0900
+++ b/hoareBinaryTree.agda	Sat Nov 20 06:36:02 2021 +0900
@@ -190,6 +190,11 @@
 depth-2< : {i j : ℕ} →   suc i ≤ suc (j Data.Nat.⊔ i )
 depth-2< {i} {j} = s≤s (m≤n⊔m _ 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 
@@ -229,6 +234,15 @@
 replaceTree1 k v1 value (t-left x t) = t-left x t
 replaceTree1 k v1 value (t-node x x₁ t t₁) = t-node x x₁ t t₁
 
+open import Relation.Binary.Definitions
+
+nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
+nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
+lemma3 refl ()
+lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
+lemma5 (s≤s z≤n) ()
+
 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 tree tree1 → t) → t
@@ -247,30 +261,30 @@
         exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (repl4 (proj1 (proj2 Pre))) (proj2 (proj2 Pre)) ⟫ where
     repl4 : stackInvariant key tree tree0 (leaf ∷ []) →  tree ≡ tree0
     repl4 (s-single .leaf) = refl
-replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = {!!} -- can't happen
-replaceP key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl ) st {!!} {!!}
-... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} {!!} 
-... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} {!!} 
+replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen
+    repl3 : stackInvariant key tree tree0 (leaf ∷ leaf ∷ st) → ⊥
+    repl3 (s-right x ())
+    repl3 (s-left x ())
+replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl ) (node key₁ value₁ left tree ∷ st)
+                  ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-right a (proj2 (proj2 Pre))  ⟫ ⟫ {!!} where
+    repl5 :  stackInvariant key tree tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 (node key₁ value₁ left tree ∷ st )
+    repl5 (s-right x si) with  si-property1 _ _ _ _ si
+    ... | refl = ⊥-elim ( nat-≤> a {!!} )
+    repl5 (s-left x si) with  si-property1 _ _ _ _ si
+    ... | refl = {!!} -- suc key ≤ key₁  , suc key ≤ key₁
+... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3<
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3<
 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
 ... | tri> ¬a ¬b c = next key value  (node key₁ value₁ repl right ) st {!!}  ≤-refl
 ... | tri≈ ¬a b ¬c = next key value  (node key value left right ) st {!!}  ≤-refl where -- this case won't happen
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl)  st ⟪ proj1 Pre , ⟪ {!!} ,  r-right a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl   where
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl)  st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) ,  r-right a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl   where
     repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 st
     repl2 (s-single .(node key₁ value₁ left right)) = {!!}
     repl2 (s-right _ si) = {!!}
     repl2 (s-left _ si) = {!!}
 
 
-open import Relation.Binary.Definitions
-
-nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
-nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
-lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
-lemma3 refl ()
-lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
-lemma5 (s≤s z≤n) ()
-
 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