--- a/hoareBinaryTree.agda	Fri Nov 05 09:21:38 2021 +0900
+++ b/hoareBinaryTree.agda	Fri Nov 05 09:35:20 2021 +0900
@@ -118,15 +118,15 @@
 replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!} {!!}
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ rstackInvariant tree rstack
-     → (next : ℕ → A → (tree1 repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ rstackInvariant repl rstack → bt-depth tree1 < bt-depth tree   → t )
+     → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ rstackInvariant repl rstack
+     → (next : ℕ → A → (tree1 : bt A) → (stack rstack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ rstackInvariant repl rstack → bt-depth tree1 < bt-depth tree   → t )
      → (exit : (tree1 repl : bt A) → (rstack : List (bt A))  → treeInvariant tree1 ∧ rstackInvariant repl rstack → t) → t
 replaceP key value tree repl [] rs Pre next exit = exit tree repl {!!} {!!}  
-replaceP key value tree repl (leaf ∷ st) rs Pre next exit = next key value tree repl st {!!} {!!} {!!}
+replaceP key value tree repl (leaf ∷ st) rs Pre next exit = next key value tree st {!!} {!!} {!!}
 replaceP key value tree repl (node key₁ value₁ left right ∷ st) rs Pre next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) repl st {!!} {!!} {!!} 
-... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) repl st {!!} {!!} {!!}
-... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) repl st {!!} {!!} {!!}
+... | 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 {!!} {!!} {!!}
 
 open import Relation.Binary.Definitions
 
@@ -161,16 +161,17 @@
        $ λ t1 P1 r R → TerminatingLoopS (bt A ∧ List (bt A) ∧ List (bt A))
             {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p))  ∧ rstackInvariant t1 (proj2 (proj2 p))}
                (λ p → bt-depth (proj1 p)) ⟪ t , ⟪ s , r ⟫ ⟫　⟪ proj1 P , ⟪ proj2 P , R ⟫ ⟫
-       $  λ p P1 loop → replaceP key value (proj1 p) {!!} (proj1 (proj2 p)) (proj2 (proj2 p)) {!!} (λ k v t repl s s1 P2 lt → loop ⟪ t , ⟪  {!!} , s1 ⟫ ⟫ {!!} {!!} ) exit 
-
+       $  λ p P1 loop → replaceP key value (proj1 p) t1 (proj1 (proj2 p)) (proj2 (proj2 p)) P1 (λ k v t s s1 P2 lt → loop ⟪ t , ⟪  s , s1 ⟫ ⟫ P2 lt ) exit 
 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
 
-insertTreeSpec0 : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
+insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
 insertTreeSpec0 _ _ _ = tt
 
 insertTreeSpec1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
 insertTreeSpec1 {n} {A}  tree key value P =
          insertTreeP tree key value P (λ  (tree₁ repl : bt A) (rstack : List (bt A)) 
-            (P1 : treeInvariant tree₁ ∧ rstackInvariant repl rstack ) → insertTreeSpec0 tree₁ value {!!} )
+            (P1 : treeInvariant tree₁ ∧ rstackInvariant repl rstack ) → insertTreeSpec0 tree₁ value (lemma1 {!!} ) ) where
+                lemma1 : (tree₁ : bt A) → top-value tree₁ ≡ just value
+                lemma1 = {!!}