--- a/hoareBinaryTree.agda	Sun Dec 05 23:18:38 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Dec 06 06:59:55 2021 +0900
@@ -533,6 +533,30 @@
     ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
     ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
+record ReplCond {n  : Level} {A : Set n} (C : ℕ → bt A → List (bt A) → Set n)   : Set (Level.suc n) where
+   field
+      c1 : (key : ℕ) → (repl : bt A) → (stack : List (bt A)) → C key repl stack
+
+replaceP0 : {n m : Level} {A : Set n} {t : Set m}
+     → (key : ℕ) → (value : A) →  ( repl : bt A)
+     → (stack : List (bt A)) 
+     →  {C : ℕ → (repl : bt A ) → List (bt A) → Set n} → C key repl stack → ReplCond C
+     → (next : ℕ → A → (repl : bt A) → (stack1 : List (bt A))
+         → C key repl stack → length stack1 < length stack → t)
+     → (exit : (repl : bt A) → C key repl [] → t) → t
+replaceP0 key value repl [] Pre _ next exit = exit repl {!!}
+replaceP0 key value repl (leaf ∷ []) Pre _ next exit = exit  (node key value leaf leaf) {!!}
+replaceP0 key value repl (node key₁ value₁ left right ∷ []) Pre e next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = exit  (node key₁ value₁ repl right ) {!!}
+... | tri≈ ¬a b ¬c = exit  repl {!!} 
+... | tri> ¬a ¬b c = exit  (node key₁ value₁ left repl  ) {!!} 
+replaceP0 {n} {_} {A} key value  repl (leaf ∷ st@(tree1 ∷ st1)) Pre e next exit = next key value repl st {!!}  ≤-refl
+replaceP0 {n} {_} {A} key value  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre e 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
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st {!!}  ≤-refl
+
+
 open _∧_
 
 RTtoTI0  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree