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