Nuprl Lemma : mset_sum_assoc

s:DSet. Assoc(MSet{s};λa,b. (a b))


Proof




Definitions occuring in Statement :  mset_sum: b mset: MSet{s} assoc: Assoc(T;op) all: x:A. B[x] lambda: λx.A[x] dset: DSet
Definitions unfolded in proof :  assoc: Assoc(T;op) infix_ap: y all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T mset_sum: b mset: MSet{s} quotient: x,y:A//B[x; y] and: P ∧ Q dset: DSet implies:  Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a prop: top: Top iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  mset_wf dset_wf list_wf set_car_wf quotient-member-eq permr_wf permr_equiv_rel append_wf equal_wf equal-wf-base append_assoc permr_reflex permr_functionality_wrt_permr append_functionality_wrt_permr permr_weakening
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isect_memberEquality isectElimination axiomEquality because_Cache pointwiseFunctionalityForEquality pertypeElimination productElimination equalityTransitivity equalitySymmetry setElimination rename lambdaEquality independent_isectElimination independent_functionElimination productEquality voidElimination voidEquality

Latex:
\mforall{}s:DSet.  Assoc(MSet\{s\};\mlambda{}a,b.  (a  +  b))



Date html generated: 2017_10_01-AM-09_59_06
Last ObjectModification: 2017_03_03-PM-01_00_14

Theory : mset


Home Index