changeset 743:80f027be2c68

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Apr 2023 14:52:06 +0900
parents 0e0a30f942ca
children fbe7c5f09ef0
files hoareBinaryTree1.agda
diffstat 1 files changed, 4 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 24 13:44:44 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 24 14:52:06 2023 +0900
@@ -709,6 +709,9 @@
       → (pg : ParentGrand (RB→bt A tree) (RB→bt A parent) tr ) → 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 = ?
+    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))