Nuprl Definition : bag-admissable
bag-admissable(T;as,bs.R[as; bs]) == (∀bs:bag(T). R[{}; bs]) ∧ (∀as,bs,cs:bag(T). (R[as; bs] ⇒ R[as + cs; bs + cs]))
Definitions occuring in Statement :
bag-append: as + bs,
empty-bag: {},
bag: bag(T),
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
empty-bag: {},
all: ∀x:A. B[x],
bag: bag(T),
implies: P ⇒ Q,
bag-append: as + bs
FDL editor aliases :
bag-admissable
Latex:
bag-admissable(T;as,bs.R[as; bs]) ==
(\mforall{}bs:bag(T). R[\{\}; bs]) \mwedge{} (\mforall{}as,bs,cs:bag(T). (R[as; bs] {}\mRightarrow{} R[as + cs; bs + cs]))
Date html generated:
2016_05_15-PM-03_10_27
Last ObjectModification:
2015_09_23-AM-07_42_12
Theory : bags
Home
Index