# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1638195176 -32400
# Node ID 33bd83e5168fd38a4e12989bb7df4fc1fcf39141
# Parent  aeddbe37d9fceecc68346e154f9b7cdfbf058bb9
...

diff -r aeddbe37d9fc -r 33bd83e5168f hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Mon Nov 29 22:45:33 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 29 23:12:56 2021 +0900
@@ -304,13 +304,15 @@
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
         repl10 with si-property1 si
         ... | refl = si
+        repl03 : s-right {_} {_} {_} {_} {_} {tree₁} {key₂} {v1} lt si ≡ replacePR.si Pre
+            → child-replaced key value (node key₁ value₁ left right ∷ tree1 ∷ st1) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre) ≡ left
+        repl03 = {!!}
+        repl04 : (si : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) ) → child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si ≡  node key₁ value₁ left right 
+        repl04 = {!!}
         repl07 : (si : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) )
-           →  node key₁ value₁ (child-replaced key value (node key₁ value₁ left right ∷ tree1 ∷ st1)
-                 (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) right
+           →  node key₁ value₁ (child-replaced key value (node key₁ value₁ left right ∷ tree1 ∷ st1) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) right
                     ≡ child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si
-        repl07 s-single = {!!}
-        repl07 (s-right x si) = refl
-        repl07 (s-left x si) = {!!}
+        repl07 = {!!}
         repl11 : replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) repl10 ) (node key₁ value₁ repl right)
         repl11 =  subst (λ k →  replacedTree key value k (node key₁ value₁ repl right)) (repl07 repl10) ( r-left a (replacePR.ri Pre))
 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl -- can't happen