Mercurial > hg > Members > Moririn
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))