--- a/hoareBinaryTree.agda	Mon Nov 08 23:17:35 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 08 23:44:24 2021 +0900
@@ -229,30 +229,26 @@
        $  λ 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 
 
--- findP key tree stack = findPP key tree stack {findPR} → record { ti = tree-invariant tree ; si stack-invariant tree stack } → 
-
-record findP-contains {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
+record findP-contains {n : Level} {A : Set n} (key1 : ℕ) (value1 : A) (tree : bt A ) (stack : List (bt A)) : Set n where
    field
-     key1 : ℕ
-     value1 : A
      tree1 : bt A
      ci : replacedTree key1 value1 tree tree1
    
 findPPC : {n m : Level} {A : Set n} {t : Set m}
-           → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
-           → (Pre :  findPR key tree stack findP-contains)
-           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 findP-contains →  bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key)  → findPR key tree1 stack1 findP-contains → t) → t
+           → (key : ℕ) → (value : A) → (tree : bt A ) → (stack : List (bt A))
+           → (Pre :  findPR key tree stack (findP-contains key value))
+           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 (findP-contains key value) →  bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key)  → findPR key tree1 stack1 (findP-contains key value) → t) → t
 findPPC = {!!}
 
 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 key (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p))
+     {λ p → findPR key (proj1 p) (proj2 p) (findP-contains key value ) } (λ p → bt-depth (proj1 p))
               ⟪ tree1 , []  ⟫ {!!}
-       $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )  
-       $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma7 {!!} {!!} found?  ) where
+       $ λ p P loop → findPPC key value (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )  
+       $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma7 {!!} (findPR.si P2 ) found?  ) where
            lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } →
               replacedTree key value1 tree t1 → stackInvariant key t1 tree s1  → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key)  →   top-value t1 ≡ just value
-           lemma7 = ?
+           lemma7 = {!!}