Mercurial > hg > Gears > GearsAgda
changeset 836:61f56e51ba3d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 18 Mar 2024 09:02:11 +0900 |
| parents | d7dab688bb8a |
| children | 887d84484e11 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 6 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sun Mar 17 20:29:43 2024 +0900 +++ b/hoareBinaryTree1.agda Mon Mar 18 09:02:11 2024 +0900 @@ -978,8 +978,12 @@ (t-single key₁ ⟪ ca , v1 ⟫) (rbr-right x trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₁ < key₂ ) ∧ tr> key₁ t ∧ tr> key₁ t₁ rr00 = RB-repl→ti> _ _ _ _ _ trb x tt -RB-repl→ti .(node _ ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) .(node _ ⟪ _ , _ ⟫ leaf _) key value (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-right x trb) = ? -RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) _) key value (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right x trb) = ? +RB-repl→ti (node _ ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ ca , v1 ⟫ leaf (node key₃ value₁ t t₁)) key value + (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-right x trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (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 key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) leaf) (node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) (node key₃ value₂ t₂ t₃)) key value + (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right x trb) = ? RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) _) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-right x trb) = ? RB-repl→ti .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key value ti (rbr-left x trb) = ? RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-right x trb) = ?