--- a/hoareBinaryTree.agda	Mon Nov 08 16:36:26 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 08 20:54:09 2021 +0900
@@ -194,7 +194,7 @@
 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
    field
      tree0 : bt A
-     ti : treeInvariant tree
+     ti : treeInvariant tree0
      si : stackInvariant tree tree0 stack
    
 findPP : {n m : Level} {A : Set n} {t : Set m}
@@ -206,19 +206,10 @@
 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 = findPP0 tree tree₁ (findPR.ti Pre ) ; si = findPP2 st (findPR.si Pre)} ) findPP1 where 
+          next tree (n ∷ st) (record {ti = findPR.ti Pre  ; si = findPP2 st (findPR.si Pre)} ) findPP1 where 
     tree0 =  findPR.tree0 Pre 
-    findPP0 : (tree tree₁ : bt A) → treeInvariant ( node key₁ v tree tree₁ ) → treeInvariant tree
-    findPP0 leaf t x = {!!}
-    findPP0 (node key value tree tree₁) leaf x = proj1 {!!}
-    findPP0 (node key value tree tree₁) (node key₁ value₁ t t₁) x = proj1 {!!}
     findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st →  stackInvariant {!!} tree0 (node key₁ v tree tree₁ ∷ st)
-    findPP2 [] = {!!}
-    findPP2 (leaf ∷ st) x = {!!}
-    findPP2 (node key value leaf leaf ∷ st) x = {!!}
-    findPP2 (node key value leaf (node key₁ value₁ x₂ x₃) ∷ st) x = {!!}
-    findPP2 (node key value (node key₁ value₁ x₁ x₃) leaf ∷ st) x = {!!}
-    findPP2 (node key value (node key₁ value₁ x₁ x₃) (node key₂ value₂ x₂ x₄) ∷ st) x = {!!}
+    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)
@@ -251,12 +242,6 @@
    TerminatingLoopS (bt A ∧ List (bt A) )
      {λ 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) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ ⟪ P1 , {!!} ⟫ lt ) 
-       $ λ t s P → insertTreeSpec0 t value {!!}
+       $ λ 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 {!!}
 
-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) 
-            (P1 : treeInvariant tree₁ ∧ replacedTree key value tree₁ repl ) → insertTreeSpec0 tree₁ value (lemma1 {!!} ) ) where
-                lemma1 : (tree₁ : bt A) → top-value tree₁ ≡ just value
-                lemma1 = {!!}