Mercurial > hg > Gears > GearsAgda
changeset 839:819562b1457d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 18 Mar 2024 21:08:17 +0900 |
| parents | 4b8e11846478 |
| children | 39e95f17ff18 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 18 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Mon Mar 18 18:54:53 2024 +0900 +++ b/hoareBinaryTree1.agda Mon Mar 18 21:08:17 2024 +0900 @@ -964,6 +964,23 @@ rr00 : kn < key₁ rr00 = proj1 rr01 +ti-replace-left : {n : Level} {A : Set n} → (t1 t2 t : bt (Color ∧ A) ) → (key k : ℕ ) → (value v1 : A) → (c : Color) → treeInvariant (node k ⟪ c , v1 ⟫ t1 t2) + → replacedRBTree key value t1 t → treeInvariant (node k ⟪ c , v1 ⟫ t t2) +ti-replace-left .leaf t2 .(node _ ⟪ Red , _ ⟫ leaf leaf) _ _ _ _ _ ti rbr-leaf = ? +ti-replace-left .(node _ ⟪ _ , _ ⟫ _ _) t2 .(node _ ⟪ _ , _ ⟫ _ _) _ _ _ _ _ ti rbr-node = ? +ti-replace-left .(node _ ⟪ _ , _ ⟫ _ _) t2 .(node _ ⟪ _ , _ ⟫ _ _) _ _ _ _ _ ti (rbr-right x rbt) = ? +ti-replace-left .(node _ ⟪ _ , _ ⟫ _ _) t2 .(node _ ⟪ _ , _ ⟫ _ _) _ _ _ _ _ ti (rbr-left x rbt) = ? +ti-replace-left .(node _ ⟪ Black , _ ⟫ _ _) t2 .(node _ ⟪ Black , _ ⟫ _ _) _ _ _ _ _ ti (rbr-black-right x rbt) = ? +ti-replace-left .(node _ ⟪ Black , _ ⟫ _ _) t2 .(node _ ⟪ Black , _ ⟫ _ _) _ _ _ _ _ ti (rbr-black-left x rbt) = ? +ti-replace-left .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) t2 .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) _ _ _ _ _ ti (rbr-flip-ll x rbt) = ? +ti-replace-left .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) t2 .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) _ _ _ _ _ ti (rbr-flip-lr x rbt) = ? +ti-replace-left .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) t2 .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) _ _ _ _ _ ti (rbr-flip-rl x rbt) = ? +ti-replace-left .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) t2 .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) _ _ _ _ _ ti (rbr-flip-rr x rbt) = ? +ti-replace-left .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) t2 .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) _ _ _ _ _ ti (rbr-rotate-ll x rbt) = ? +ti-replace-left .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) t2 .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) _ _ _ _ _ ti (rbr-rotate-rr x rbt) = ? +ti-replace-left .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) t2 .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) _ _ _ _ _ ti (rbr-rotate-lr t₂ t₃ kg kp kn rbt) = ? +ti-replace-left .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) t2 .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) _ _ _ _ _ ti (rbr-rotate-rl t₂ t₃ kg kp kn rbt) = ? + RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree → replacedRBTree key value tree repl → treeInvariant repl RB-repl→ti .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key value ti rbr-leaf = t-single key ⟪ Red , value ⟫ @@ -991,7 +1008,7 @@ (proj1 rr00) x₃ x₄ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ ti₁ trb) where rr00 : (key₃ < key₄) ∧ tr> key₃ t₃ ∧ tr> key₃ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb x ⟪ x₂ , ⟪ x₅ , x₆ ⟫ ⟫ -RB-repl→ti .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key value ti (rbr-left x trb) = ? +RB-repl→ti .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key value ti (rbr-left x trb) = ti-replace-left _ _ _ _ _ _ _ _ ti trb RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-right x trb) = ? RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-left x trb) = ? RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-ll x trb) = ?