Nuprl Definition : gcd_p
GCD(a;b;y) == (y | a) ∧ (y | b) ∧ (∀z:ℤ. (((z | a) ∧ (z | b)) ⇒ (z | y)))
Definitions occuring in Statement :
divides: b | a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
int: ℤ
Definitions occuring in definition :
all: ∀x:A. B[x],
int: ℤ,
implies: P ⇒ Q,
and: P ∧ Q,
divides: b | a
FDL editor aliases :
gcd_p
Latex:
GCD(a;b;y) == (y | a) \mwedge{} (y | b) \mwedge{} (\mforall{}z:\mBbbZ{}. (((z | a) \mwedge{} (z | b)) {}\mRightarrow{} (z | y)))
Date html generated:
2016_05_14-PM-04_17_45
Last ObjectModification:
2015_09_22-PM-06_02_34
Theory : num_thy_1
Home
Index