Mercurial > hg > Gears > GearsAgda
changeset 788:1e8cb65cccef
: Enter commit message. Lines beginning with 'HG:' are removed.
| author | Moririn < Moririn@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 16 Oct 2023 19:42:05 +0900 |
| parents | d0080588ccf4 |
| children | b85b2a8e40c1 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 6 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Mon Oct 16 10:38:34 2023 +0900 +++ b/hoareBinaryTree1.agda Mon Oct 16 19:42:05 2023 +0900 @@ -942,19 +942,19 @@ ; ri = RBI.ri r } -} ... | case2 (case1 eq) = {!!} where -- insertCase12 insertCase12 : (to : bt (Color ∧ A)) → RBtreeInvariant orig → to ≡ orig - → (rr : bt (Color ∧ A)) → RBtreeInvariant {!!} → rr ≡ {!!} - → (stack1 : List (bt (Color ∧ A))) → (si : stackInvariant key {!!} to stack1 ) + → (rr : bt (Color ∧ A)) → RBtreeInvariant rr → rr ≡ (child-replaced key orig) + → (stack1 : List (bt (Color ∧ A))) → (si : stackInvariant key rr to stack1 ) → stack1 ≡ rr ∷ to ∷ [] → t insertCase12 to or t≡o rr rbt r≡r stack1 sti stack≡ = next rr stack1 record { od = RBI.od r ; d = RBI.rd r ; rd = RBI.rd r ; --r - tree = to ; rot = {!!} + tree = {!!} ; rot = RBI.rot r ; origti = RBI.origti r ; origrb = RBI.origrb r - ; treerb = subst (λ k → RBtreeInvariant k) (sym t≡o) (or) - ; replrb = {!!} --subst (λ k → RBtreeInvariant k) (sym t≡o) (RBI.origrb r) + ; treerb = {!!} --subst (λ k → RBtreeInvariant k) (sym t≡o) (or) + ; replrb = rbt --subst (λ k → RBtreeInvariant k) (sym t≡o) (RBI.origrb r) ; d=rd = {!!} - ; si = subst₂ (λ j k → stackInvariant key j k stack1) (r≡r) (t≡o) (sti) + ; si = {!!} --subst (λ k → stackInvariant key rr k stack1) (t≡o) (sti) ; rotated = {!!} ; ri = {!!} --subst (λ k → replacedRBTree key value (child-replaced key (RBI.rot r)) k) (sym t≡o) ({!ct!}) }