Nuprl Definition : satisfies-integer-equality
xs ⋅ as =0 == (||xs|| = ||as|| ∈ ℤ) ∧ 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ) ∧ (as ⋅ xs = 0 ∈ ℤ)
Definitions occuring in Statement :
integer-dot-product: as ⋅ bs,
hd: hd(l),
length: ||as||,
less_than: a < b,
and: P ∧ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
less_than: a < b,
length: ||as||,
and: P ∧ Q,
hd: hd(l),
equal: s = t ∈ T,
int: ℤ,
integer-dot-product: as ⋅ bs,
natural_number: $n
FDL editor aliases :
sat-z-eq
Latex:
xs \mcdot{} as =0 == (||xs|| = ||as||) \mwedge{} 0 < ||xs|| \mwedge{} (hd(xs) = 1) \mwedge{} (as \mcdot{} xs = 0)
Date html generated:
2016_05_14-AM-06_56_14
Last ObjectModification:
2015_09_22-PM-05_51_16
Theory : omega
Home
Index