# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1638232522 -32400
# Node ID 4efb74d28d6a742e0ee46eca8404ca9f6323d960
# Parent  01c16d4d6d8cc9a8ca049b5bcfbdbcfefe72cb81
...

diff -r 01c16d4d6d8c -r 4efb74d28d6a hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Tue Nov 30 05:52:13 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 30 09:35:22 2021 +0900
@@ -296,33 +296,25 @@
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ 
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
-    Post with replacePR.si Pre | inspect replacePR.si Pre
-    ... | s-left x t | record { eq = eq} = {!!}  -- can't happen
-    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si | record { eq = refl } = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl11 ; ci = lift tt } where
+    Post with replacePR.si Pre | inspect replacePR.si Pre | replacePR.ri Pre
+    ... | s-left x t | record { eq = refl } | ri = {!!}  -- can't happen
+    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si | record { eq = refl } | ri = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
         repl09 = si-property1 si
         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 refl = refl
-        repl04 : (si : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) )
-            → tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)  → child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si ≡  node key₁ value₁ left right 
-        repl04 s-single refl = {!!}
-        repl04 (s-right lt2 si2) refl = {!!}
-        repl04 (s-left lt2 si2) refl = refl
-        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
-                    ≡ child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) 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))
         repl12 : replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) repl10 ) (node key₁ value₁ repl right)
         repl12 with repl09 | repl10 
-        ... | refl | s-single = {!!}
-        ... | refl | s-right lt2 si2 = {!!}
-        ... | refl | s-left lt2 si2 = r-left a (subst (λ k → replacedTree key value k repl ) (repl03 refl) (replacePR.ri Pre))
+        ... | refl | s-single =  {!!} where -- key ≡ key₂ → ⊥ -- child-replaced ≡ leaf
+            repl03 : child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) s-single   ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
+            repl03 = refl
+        ... | refl | s-right lt2 si2 =  {!!} where -- key₂ < key, key₂ < key₁, key < key₁ -- child-replaced ≡ right
+            repl04 : child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) (s-right lt2 si2) ≡ tree₁
+            repl04 = refl
+        ... | refl | s-left lt2 si2 = r-left a (replacePR.ri Pre) where
+            repl05 : child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) (s-left lt2 si2)  ≡ node key₁ value₁ left right
+            repl05 = refl
 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl -- can't happen
 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl