Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 788:1e8cb65cccef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
: 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
comparison
equal deleted inserted replaced
787:d0080588ccf4 788:1e8cb65cccef
940 ; si = RBI.si r 940 ; si = RBI.si r
941 ; rotated = RBI.rotated r 941 ; rotated = RBI.rotated r
942 ; ri = RBI.ri r } -} 942 ; ri = RBI.ri r } -}
943 ... | case2 (case1 eq) = {!!} where -- insertCase12 943 ... | case2 (case1 eq) = {!!} where -- insertCase12
944 insertCase12 : (to : bt (Color ∧ A)) → RBtreeInvariant orig → to ≡ orig 944 insertCase12 : (to : bt (Color ∧ A)) → RBtreeInvariant orig → to ≡ orig
945 → (rr : bt (Color ∧ A)) → RBtreeInvariant {!!} → rr ≡ {!!} 945 → (rr : bt (Color ∧ A)) → RBtreeInvariant rr → rr ≡ (child-replaced key orig)
946 → (stack1 : List (bt (Color ∧ A))) → (si : stackInvariant key {!!} to stack1 ) 946 → (stack1 : List (bt (Color ∧ A))) → (si : stackInvariant key rr to stack1 )
947 → stack1 ≡ rr ∷ to ∷ [] → t 947 → stack1 ≡ rr ∷ to ∷ [] → t
948 insertCase12 to or t≡o rr rbt r≡r stack1 sti stack≡ = next rr stack1 948 insertCase12 to or t≡o rr rbt r≡r stack1 sti stack≡ = next rr stack1
949 record { 949 record {
950 od = RBI.od r ; d = RBI.rd r ; rd = RBI.rd r ; --r 950 od = RBI.od r ; d = RBI.rd r ; rd = RBI.rd r ; --r
951 tree = to ; rot = {!!} 951 tree = {!!} ; rot = RBI.rot r
952 ; origti = RBI.origti r 952 ; origti = RBI.origti r
953 ; origrb = RBI.origrb r 953 ; origrb = RBI.origrb r
954 ; treerb = subst (λ k → RBtreeInvariant k) (sym t≡o) (or) 954 ; treerb = {!!} --subst (λ k → RBtreeInvariant k) (sym t≡o) (or)
955 ; replrb = {!!} --subst (λ k → RBtreeInvariant k) (sym t≡o) (RBI.origrb r) 955 ; replrb = rbt --subst (λ k → RBtreeInvariant k) (sym t≡o) (RBI.origrb r)
956 ; d=rd = {!!} 956 ; d=rd = {!!}
957 ; si = subst₂ (λ j k → stackInvariant key j k stack1) (r≡r) (t≡o) (sti) 957 ; si = {!!} --subst (λ k → stackInvariant key rr k stack1) (t≡o) (sti)
958 ; rotated = {!!} 958 ; rotated = {!!}
959 ; ri = {!!} --subst (λ k → replacedRBTree key value (child-replaced key (RBI.rot r)) k) (sym t≡o) ({!ct!}) 959 ; ri = {!!} --subst (λ k → replacedRBTree key value (child-replaced key (RBI.rot r)) k) (sym t≡o) ({!ct!})
960 } 960 }
961 {!!} 961 {!!}
962 -- exit rot repl rbir ? ? 962 -- exit rot repl rbir ? ?