Mercurial > hg > Members > Moririn
changeset 733:737c5f95e5b3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 13 Apr 2023 16:13:42 +0900 |
| parents | 18cd778f4bad |
| children | 9d5e749531b1 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 7 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Tue Apr 11 21:12:56 2023 +0900 +++ b/hoareBinaryTree1.agda Thu Apr 13 16:13:42 2023 +0900 @@ -570,6 +570,11 @@ s-left : {key₁ key₂ : ℕ} → {c1 : Color} {d1 : ℕ} → key₂ < key₁ → (top : RBTree A key₁ c1 d1) → rbstackInvariant orig key₁ → rbstackInvariant orig key +data rbstackInvariant2 {n : Level} {A : Set n} {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) : + {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (parent : RBTree A k1 c1 d1) (grand : RBTree A k2 c2 d2) Set n where + s-head : rbstackInvariant2 orig ? orig + s-right : rbstackInvariant2 orig ? ? → rbstackInvariant2 orig ? ? + rbsi-len : {n : Level} {A : Set n} {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) {key₁ : ℕ } → rbstackInvariant orig key₁ → ℕ rbsi-len orig s-nil = 0 @@ -622,6 +627,7 @@ rotateRight : ? rotateRight = ? + rotateLeft : ? rotateLeft = ? @@ -664,7 +670,7 @@ insertCase1 : (key1 : ℕ) (si : rbstackInvariant orig key1) → t insertCase1 key1 s-nil = exit ? ? ? insertCase1 key1 (s-right {key₁} {key₂} x top s-nil) = exit ? ? ? - insertCase1 key1 (s-right {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ + insertCase1 key1 (s-right {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si ? top₁ insertCase1 key1 (s-right {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ insertCase1 key1 (s-left {key₁} {key₂} x top s-nil) = exit ? ? ? insertCase1 key1 (s-left {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁