--- a/hoareBinaryTree.agda	Mon Nov 08 20:54:09 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 08 21:07:41 2021 +0900
@@ -191,35 +191,36 @@
 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
 insertTreeSpec0 _ _ _ = tt
 
-record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
+record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where
    field
      tree0 : bt A
      ti : treeInvariant tree0
      si : stackInvariant tree tree0 stack
+     ci : C tree stack
    
 findPP : {n m : Level} {A : Set n} {t : Set m}
            → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
-           → (Pre :  findPR tree stack  )
-           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1  →  bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1  → t) → t
-findPP key leaf st Pre next exit = exit leaf st Pre  
-findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
-findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st P 
-findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c =
-          next tree (n ∷ st) (record {ti = findPR.ti Pre  ; si = findPP2 st (findPR.si Pre)} ) findPP1 where 
+           → (C : bt A → List (bt A) → Set n ) (Pre :  findPR tree stack {!!} )
+           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 {!!} →  bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 {!!} → t) → t
+findPP key leaf st C Pre next exit = exit leaf st Pre  
+findPP key (node key₁ v tree tree₁) st C Pre next exit with <-cmp key key₁
+findPP key n st C P next exit | tri≈ ¬a b ¬c = exit n st P 
+findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st C Pre next exit | tri< a ¬b ¬c =
+          next tree (n ∷ st) (record {ti = findPR.ti Pre  ; si = findPP2 st (findPR.si Pre) ; ci = ?} ) findPP1 where 
     tree0 =  findPR.tree0 Pre 
     findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st →  stackInvariant {!!} tree0 (node key₁ v tree tree₁ ∷ st)
-    findPP2 = ?
+    findPP2 = {!!}
     findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
     findPP1 =  {!!}
-findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st)
+findPP key n@(node key₁ v tree tree₁) st C Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st)
     findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
     findPP2 = {!!}
 
 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
      → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t
 insertTreePP {n} {m} {A} {t} tree key value P exit =
-   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  {!!}
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) {!!} } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  {!!}
        $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t ,  s  ⟫ {!!} lt )
        $ λ t s P → replaceNodeP key value t {!!}
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
@@ -240,7 +241,7 @@
 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree  → ⊤
 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
    TerminatingLoopS (bt A ∧ List (bt A) )
-     {λ p → findPR (proj1 p) (proj2 p) ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p))
+     {λ p → findPR (proj1 p) (proj2 p) {!!} ∧ findP-contains (proj1 p) (proj2 p)} (λ p → bt-depth (proj1 p))
               ⟪ tree1 , []  ⟫ ⟪ {!!} , record { key1 = key ; value1 = value ; tree1 = tree ; ci = RT ; R = record { tree0 = {!!} ; ti = P ; si = lift tt } } ⟫
        $ λ p P loop → findPP key (proj1 p) (proj2 p) (proj1 P) (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt ) 
        $ λ t1 s1 P2 → insertTreeSpec0 t1 value {!!}