Nuprl Definition : reducible
reducible(a) == ∃b,c:ℤ-o. ((¬(b ~ 1)) ∧ (¬(c ~ 1)) ∧ (a = (b * c) ∈ ℤ))
Definitions occuring in Statement :
assoced: a ~ b,
int_nzero: ℤ-o,
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
multiply: n * m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
int_nzero: ℤ-o,
and: P ∧ Q,
not: ¬A,
assoced: a ~ b,
natural_number: $n,
equal: s = t ∈ T,
int: ℤ,
multiply: n * m
FDL editor aliases :
reducible
Latex:
reducible(a) == \mexists{}b,c:\mBbbZ{}\msupminus{}\msupzero{}. ((\mneg{}(b \msim{} 1)) \mwedge{} (\mneg{}(c \msim{} 1)) \mwedge{} (a = (b * c)))
Date html generated:
2016_05_14-PM-04_19_41
Last ObjectModification:
2015_09_22-PM-06_02_37
Theory : num_thy_1
Home
Index