Mercurial > hg > Members > Moririn
changeset 732:18cd778f4bad
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 11 Apr 2023 21:12:56 +0900 |
| parents | 5b2985ecfcf7 |
| children | 737c5f95e5b3 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Tue Apr 11 20:06:26 2023 +0900 +++ b/hoareBinaryTree1.agda Tue Apr 11 21:12:56 2023 +0900 @@ -654,11 +654,11 @@ → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1)) → t ) → t replaceRBP {n} {m} {A} {t} key value {_} {key2} orig tree repl si ri next exit = insertCase1 key2 si where - insertCase4 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A k2 c2 d2) → t + insertCase4 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t insertCase4 = ? - insertCase3 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A k2 c2 d2) → t - insertCase3 = ? - insertCase2 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A k2 c2 d2) → t + insertCase3 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t + insertCase3 key1 si parent grandparent = ? + insertCase2 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t insertCase2 key1 si {_} {_} {_} {_} {Red} parent grand = insertCase3 key1 si parent grand insertCase2 key1 si {_} {_} {_} {_} {Black} parent grand = next ? ? ? ? ? ? ? insertCase1 : (key1 : ℕ) (si : rbstackInvariant orig key1) → t