# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1636378240 -32400
# Node ID 074fb29ebf5766a861a8110332e37ae433a71a08
# Parent  bf27e2c7c6c5782ce25733af80cbf08f08e5b7e2
...

diff -r bf27e2c7c6c5 -r 074fb29ebf57 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Mon Nov 08 21:36:28 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 08 22:30:40 2021 +0900
@@ -202,10 +202,10 @@
            → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
            → (Pre :  findPR tree stack (λ t s → Lift n ⊤))
            → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) →  bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) → t) → t
-findPP key leaf st Pre next exit = exit leaf st Pre  
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key)  → findPR tree1 stack1 (λ t s → Lift n ⊤) → t) → t
+findPP key leaf st Pre next exit = exit leaf st (case1 refl) 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 key n st P next exit | tri≈ ¬a b ¬c = exit n st (case2 {!!}) 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) ; ci = lift tt} ) findPP1 where 
     tree0 =  findPR.tree0 Pre 
@@ -222,7 +222,7 @@
 insertTreePP {n} {m} {A} {t} tree key value  P exit =
    TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ 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 {!!}
+       $ λ t s _ P → replaceNodeP key value t {!!}
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
             {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p)  ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
                (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!}  , R ⟫ ⟫
@@ -242,7 +242,7 @@
            → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
            → (Pre :  findPR tree stack findP-contains)
            → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains →  bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains → t) → t
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key)  → findPR tree1 stack1 findP-contains → 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  → ⊤
@@ -251,5 +251,7 @@
      {λ p → findPR (proj1 p) (proj2 p) findP-contains } (λ 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 P2 → insertTreeSpec0 t1 value {!!}
+       $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value {!!} where
+           lemma3 : ?
+           lemma3 = ?