Nuprl Definition : polyform-lead-nonzero
polyform-lead-nonzero(n;p) == 0 < n ⇒ 0 < ||p|| ⇒ (¬↑poly-zero(n - 1;hd(p)))
Definitions occuring in Statement :
poly-zero: poly-zero(n;p),
hd: hd(l),
length: ||as||,
assert: ↑b,
less_than: a < b,
not: ¬A,
implies: P ⇒ Q,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
hd: hd(l),
natural_number: $n,
subtract: n - m,
poly-zero: poly-zero(n;p),
assert: ↑b,
not: ¬A,
length: ||as||,
less_than: a < b,
implies: P ⇒ Q
FDL editor aliases :
polyform-lead-nonzero
Latex:
polyform-lead-nonzero(n;p) == 0 < n {}\mRightarrow{} 0 < ||p|| {}\mRightarrow{} (\mneg{}\muparrow{}poly-zero(n - 1;hd(p)))
Date html generated:
2017_04_17-AM-09_02_17
Last ObjectModification:
2017_04_13-PM-00_33_58
Theory : list_1
Home
Index