Mercurial > hg > Gears > GearsAgda

changeset 684:33bd83e5168f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Nov 2021 23:12:56 +0900
parents aeddbe37d9fc
children 01c16d4d6d8c
files hoareBinaryTree.agda
diffstat 1 files changed, 7 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- 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