--- a/hoareBinaryTree.agda	Mon Nov 22 08:24:21 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 22 08:58:59 2021 +0900
@@ -150,6 +150,11 @@
 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
 stackInvariantTest1 = s-right (add< 2) 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 key tree .tree .(tree ∷ []) s-single ()
+si-property0 key tree tree0 .(tree ∷ _) (s-right x si) ()
+si-property0 key tree tree0 .(tree ∷ _) (s-left x si) ()
+
 si-property1 :  {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-top stack ≡ just tree
 si-property1 key t t0 (t ∷ []) s-single  = refl
@@ -265,17 +270,19 @@
      → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A))
          → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 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 {tree0} {tree} {tree-st} repl [] Pre next exit = {!!} -- can't happen
-replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit =  exit tree0 (node key value leaf leaf) ?
+replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit = ⊥-elim ( si-property0 _ _ _ _ (proj1 (proj2 Pre)) refl ) -- can't happen
+replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit =
+       exit tree0 (node key value leaf leaf) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!}  r-leaf ⟫
 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ?
-... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value  left right ) ?
-... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ?
-replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit =  {!!} -- exit (node key value leaf leaf)
+... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫
+... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value  left right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫
+... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫
+replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit =
+     next key value {tree0} (node key value leaf leaf) st ⟪ proj1 Pre ,  ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫  ⟫  ≤-refl
 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ? ≤-refl
-... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value  left right ) st ? ≤-refl
-... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ? ≤-refl
+... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫  ⟫ ≤-refl
+... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value  left right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫ ⟫ ≤-refl
+... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫ ⟫ ≤-refl
 
 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
    → (r : Index) → (p : Invraiant r)