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

diff -r 074fb29ebf57 -r 6465673df5bc hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Mon Nov 08 22:30:40 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 08 22:45:19 2021 +0900
@@ -252,6 +252,11 @@
               ⟪ 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 {!!} where
-           lemma3 : ?
-           lemma3 = ?
+           lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } →
+              replacedTree key value1 tree t1 → stackInvariant t1 tree s1  → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key)  →  node-key t1 ≡ just key
+           lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case1 ())
+           lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case2 x) = x
+           lemma7 {.key₁} {value1} {.(node key₁ value1 s1 s2)} {node key₁ value s1 s2} r-node s or = {!!}
+           lemma7 {key} {value1} {.(node key₁ value s1 _)} {node key₁ value s1 s2} (r-right x r) s or = {!!}
+           lemma7 {key} {value1} {.(node key₁ value _ s2)} {node key₁ value s1 s2} (r-left x r) s or = {!!}