Nuprl Definition : is_ufm
IsUFM(g) == ∀b:|g|. ((¬(g-unit(b))) ⇒ (≡~)∃!as:Atom{g} List. (b = (Π as) ∈ |g|))
Definitions occuring in Statement :
permr_massoc_rel: ≡~,
exists_uni_upto: exists_uni_upto,
matom_ty: Atom{g},
munit: g-unit(u),
mon_reduce: mon_reduce,
list: T List,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
equal: s = t ∈ T,
grp_car: |g|
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
not: ¬A,
munit: g-unit(u),
exists_uni_upto: exists_uni_upto,
list: T List,
matom_ty: Atom{g},
permr_massoc_rel: ≡~,
equal: s = t ∈ T,
grp_car: |g|,
mon_reduce: mon_reduce
Latex:
IsUFM(g) == \mforall{}b:|g|. ((\mneg{}(g-unit(b))) {}\mRightarrow{} (\mequiv{}\msim{})\mexists{}!as:Atom\{g\} List. (b = (\mPi{} as)))
Date html generated:
2016_05_16-AM-07_45_19
Last ObjectModification:
2015_09_23-AM-09_51_58
Theory : factor_1
Home
Index