Mercurial > hg > Members > Moririn

changeset 744:fbe7c5f09ef0

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, 24 Apr 2023 16:02:38 +0900
parents 80f027be2c68
children 9b7d706e7d0f
files hoareBinaryTree1.agda
diffstat 1 files changed, 5 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 24 14:52:06 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 24 16:02:38 2023 +0900
@@ -705,13 +705,15 @@
 replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 stack _ _ refl refl si where
     insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree : RBTree A k0 c0 d0) 
       → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) 
-      → (stack : List (bt A)) → (tr to : bt A) → RB→bt A grand ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) 
-      → (pg : ParentGrand (RB→bt A tree) (RB→bt A parent) tr ) → t
+      → (stack : List (bt A)) → (tr to pt gt : bt A) → RB→bt A tree ≡ tr → RB→bt A parent ≡ pt → RB→bt A grand ≡ gt →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) 
+      → (pg : ParentGrand tr pt gt ) → t
     insertCase2 tree parent grand stack tr to treq toeq si pg = ?
     insertCase1 : (stack : List (bt A)) → (tr to : bt A) → RB→bt A tree ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) → t
     insertCase1 stack tr to eqt eqo si with stackToPG tr to stack si
     ... | case1 eq = ?
     ... | case2 (case1 eq ) = ?
-    ... | case2 (case2 pg) = insertCase2 ? ? ? ? ? ? ? ? ? (subst₂ (λ j k → ParentGrand j k ? ) ? ? (PG.pg pg))
+    ... | case2 (case2 pg) = insertCase2 ? ? ? ? ? ? ? ? ? ? ? ? ? (PG.pg pg) where
+          si00 : stackInvariant key ? ? ?
+          si00 = ?