# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1636613839 -32400
# Node ID 119f340c0b10464d75d04ab71fc2b93e0f06dce3
# Parent  b58991f8e2e47ad3bc2527f990b63722a0e5da0a
...

diff -r b58991f8e2e4 -r 119f340c0b10 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Thu Nov 11 15:48:36 2021 +0900
+++ b/hoareBinaryTree.agda	Thu Nov 11 15:57:19 2021 +0900
@@ -138,6 +138,17 @@
 depth-2< : {i j : ℕ} →   suc i ≤ suc (j Data.Nat.⊔ i )
 depth-2< {i} {j} = s≤s (m≤n⊔m _ i)
 
+lemma11  : {n : Level} {A : Set n} {v1 : A}  → (key key₁ : ℕ) → (tree tree₁ : bt A )
+      → key < key₁
+      → treeInvariant (node key₁ v1 tree tree₁)
+      →      treeInvariant tree 
+lemma11  = {!!}
+
+--        stackInvariant key (node key₁ v1 tree tree₁) tree0 st
+--        → stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ st)
+
+open _∧_
+
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
            →  treeInvariant tree ∧ stackInvariant key tree tree0 stack  
            → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
@@ -145,12 +156,8 @@
 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre
 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
 findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st Pre
-findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} depth-1<
+findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) ⟪ lemma11 {!!} {!!} {!!} {!!} {!!} (proj1 Pre)  , {!!}  ⟫ depth-1<
 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} depth-2<
--- Pre   : treeInvariant (node key₁ v1 tree tree₁)
---    →      treeInvariant tree ∧
---        stackInvariant key (node key₁ v1 tree tree₁) tree0 st
--        → stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ st)
 
 
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree )