Nuprl Definition : mreducible
Reducible(a) == ∃b,c:|g|. ((¬(g-unit(b))) ∧ (¬(g-unit(c))) ∧ (a = (b * c) ∈ |g|))
Definitions occuring in Statement :
munit: g-unit(u)
,
infix_ap: x f y
,
exists: ∃x:A. B[x]
,
not: ¬A
,
and: P ∧ Q
,
equal: s = t ∈ T
,
grp_op: *
,
grp_car: |g|
Definitions occuring in definition :
exists: ∃x:A. B[x]
,
and: P ∧ Q
,
not: ¬A
,
munit: g-unit(u)
,
equal: s = t ∈ T
,
grp_car: |g|
,
infix_ap: x f y
,
grp_op: *
Latex:
Reducible(a) == \mexists{}b,c:|g|. ((\mneg{}(g-unit(b))) \mwedge{} (\mneg{}(g-unit(c))) \mwedge{} (a = (b * c)))
Date html generated:
2016_05_16-AM-07_44_02
Last ObjectModification:
2015_09_23-AM-09_51_52
Theory : factor_1
Home
Index