# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1638596823 -32400
# Node ID e5140faf1602bfea94e0f8c5141cda7e77be82fb
# Parent  578f29a76857d8d59068f6f723c0eb188e0b5748
...

diff -r 578f29a76857 -r e5140faf1602 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Fri Dec 03 11:14:19 2021 +0900
+++ b/hoareBinaryTree.agda	Sat Dec 04 14:47:03 2021 +0900
@@ -610,11 +610,16 @@
 findPPC key (node key₁ v1 tree tree₁) st Pre next exit with <-cmp key key₁
 findPPC key n st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
 findPPC {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st)
-       record { tree0 = findPR.tree0 Pre ; ti0 = findPR.ti0 Pre  ; ti = treeLeftDown tree tree₁ (findPR.ti Pre)  ; si =  findP1 a st (findPR.si Pre)
+       record { tree0 = findPR.tree0 Pre ; ti0 = findPR.ti0 Pre  ; ti = treeLeftDown tree tree₁ (findPR.ti Pre)  ; si =  s-left a (findPR.si Pre)
           ; ci = {!!} } depth-1< where
-   findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁)
-         (findPR.tree0 Pre) st → stackInvariant key tree (findPR.tree0 Pre) (tree ∷ st)
-   findP1 a (x ∷ st) si = s-left a si
+   findP2 : findPC key tree (tree ∷ st)
+   findP2 with findPC.ci (findPR.ci Pre) | findPC.tree1 (findPR.ci Pre)
+   findP2 | r-node | leaf = {!!}
+   findP2 | r-node | node key value t t₁ = record { tree1 = t ; value = findPC.value (findPR.ci Pre)  ; ci =  {!!} }
+   findP2 | (r-right x ri) | t = ⊥-elim (nat-<> x a)
+   findP2 | (r-left x ri) | node key value t t₁ = record { tree1 = t ; value = findPC.value (findPR.ci Pre)  ; ci =  {!!} }
+   findP2 | r-left x ri | leaf = {!!}
+   -- findP2 (r-left x ri) = subst₂ (λ j k →  replacedTree key (findPC.value (findPR.ci Pre)) j k ) {!!} {!!} ri 
 findPPC key n@(node key₁ v1 tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st)
        record { tree0 = findPR.tree0 Pre ; ti0 = findPR.ti0 Pre ; ti = treeRightDown tree tree₁ (findPR.ti Pre) ; si =  s-right c (findPR.si Pre)
           ; ci = {!!} }  depth-2<