--- a/hoareBinaryTree.agda	Mon Nov 15 15:34:30 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 15 17:04:13 2021 +0900
@@ -97,6 +97,21 @@
        → treeInvariant (node key₂ value₂ t₃ t₄)
        → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 
 
+data stackInvariant {n : Level} {A : Set n}  : (tree tree0 : bt A) → (stack  : List (bt A)) → Set n where
+    s-single : (tree : bt A) → stackInvariant tree tree (tree ∷ [] ) 
+    s-right :  {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
+        →  stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree₁ tree0 (tree₁ ∷ st)
+    s-left :  {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
+        →  stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree tree0 (tree  ∷ st)
+
+data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (tree tree1 : 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 t1 t2 →  replacedTree key value (node k v1 t t1) (node k v1 t t2) 
+    r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
+          → k < key →  replacedTree key value t1 t2 →  replacedTree key value (node k v1 t1 t) (node k v1 t2 t) 
+
 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
 add<  {i} j = begin
         suc i ≤⟨ m≤m+n (suc i) j ⟩
@@ -110,27 +125,38 @@
 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) )
 
-data stackInvariant {n : Level} {A : Set n}  : (tree tree0 : bt A) → (stack  : List (bt A)) → Set n where
-    s-nil : stackInvariant  leaf leaf [] 
-    s-single : (tree : bt A) → stackInvariant tree tree (tree ∷ [] ) 
-    s-right :  {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
-        →  stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree₁ tree0 (tree₁ ∷ st)
-    s-left :  {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
-        →  stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree tree0 (tree  ∷ st)
+stack-top :  {n : Level} {A : Set n} (stack  : List (bt A)) → Maybe (bt A)
+stack-top [] = nothing
+stack-top (x ∷ s) = just x
 
-stackInvariantTest0 : stackInvariant {_} {ℕ} leaf leaf []
-stackInvariantTest0 = s-nil
+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 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
 stackInvariantTest1 = s-right (s-single treeTest1 )
 
-data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (tree tree1 : 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 t1 t2 →  replacedTree key value (node k v1 t t1) (node k v1 t t2) 
-    r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k < key →  replacedTree key value t1 t2 →  replacedTree key value (node k v1 t1 t) (node k v1 t2 t) 
+si-property1 :  {n : Level} {A : Set n}  (tree tree0 : bt A) → (stack  : List (bt A)) → stackInvariant tree tree0 stack
+   → stack-top stack ≡ just tree
+si-property1 t t0 (x ∷ .[]) (s-single .x) = refl
+si-property1 t t0 (t ∷ st) (s-right si) = refl
+si-property1 t t0 (t ∷ st) (s-left si) = refl
+
+si-property-last :  {n : Level} {A : Set n}  (tree tree0 : bt A) → (stack  : List (bt A)) → stackInvariant tree tree0 stack
+   → stack-last stack ≡ just tree0
+si-property-last t t0 (x ∷ []) (s-single .x) = refl
+si-property-last t t0 (.t ∷ x ∷ st) (s-right si) with  si-property1 _ _ (x ∷ st) si
+... | refl = si-property-last x t0 (x ∷ st) si
+si-property-last t t0 (.t ∷ x ∷ st) (s-left si) with  si-property1 _ _ (x ∷ st) si
+... | refl = si-property-last x t0 (x ∷ st) si
+
+rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
+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 _ _ _ _) .(node _ _ _ _) (r-right x rt) ()
+rt-property1 {n} {A} key value .(node _ _ _ _) .(node _ _ _ _) (r-left x rt) ()
+
 depth-1< : {i j : ℕ} →   suc i ≤ suc (i Data.Nat.⊔ j )
 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
 
@@ -153,8 +179,6 @@
 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₁
 
---        stackInvariant key (node key₁ v1 tree tree₁) tree0 st
---        → stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ st)
 
 open _∧_
 
@@ -186,14 +210,16 @@
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant repl tree stack ∧ replacedTree key value tree repl
-     → (next : ℕ → A → (tree1 repl : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant repl tree1 stack ∧ replacedTree key value tree1 repl → bt-depth tree1 < bt-depth tree   → t )
+     → (next : ℕ → A → (tree1 repl : bt A) → (stack1 : List (bt A))
+         → treeInvariant tree1 ∧ stackInvariant repl tree1 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
-replaceP key value tree repl [] Pre next exit = exit tree repl {!!} 
-replaceP key value tree repl (leaf ∷ st) Pre next exit = next key value tree {!!} st {!!} {!!}
+replaceP key value tree repl [] Pre next exit = exit tree repl ⟪ proj1 Pre , proj2 (proj2 Pre) ⟫
+replaceP key value tree repl (leaf ∷ st) Pre next exit with si-property1 _ _ _ (proj1 (proj2 Pre)) | rt-property1 _ _ _ _ (proj2 (proj2 Pre))
+... | refl | t1 = ⊥-elim ( t1 refl )
 replaceP key value 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₁ tree right ) {!!} st {!!}  {!!}
-... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) {!!} st {!!}  {!!}
-... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) {!!} st {!!}  {!!}
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) (node key₁ value₁ repl right ) st {!!}  ≤-refl
+... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right )(node key₁ value₁  left right )  st {!!}   ≤-refl
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) (node key₁ value₁ left repl )st {!!}  ≤-refl
 
 open import Relation.Binary.Definitions
 
@@ -235,7 +261,7 @@
        $ λ t _ s P C → replaceNodeP key value t C (proj1 P)
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
             {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p)  ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
-               (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ proj1 P , ⟪ {!!}  , R ⟫ ⟫
+               (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ proj1 P , ⟪ {!!}  , R ⟫ ⟫
        $  λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
             (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1  , repl1  ⟫ ⟫ {!!} lt )  exit 
 
@@ -280,7 +306,7 @@
        $ λ t s _ P → replaceNodeP key value t {!!} {!!}
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
             {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p)  ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
-               (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!}  , R ⟫ ⟫
+               (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!}  , R ⟫ ⟫
        $  λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
             (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1  , repl1  ⟫ ⟫ {!!} lt )  exit