Nuprl Definition : imonomial-less
imonomial-less(m1;m2) == (¬((snd(m1)) = (snd(m2)) ∈ (ℤ List))) ∧ (↑imonomial-le(m1;m2))
Definitions occuring in Statement :
imonomial-le: imonomial-le(m1;m2),
list: T List,
assert: ↑b,
pi2: snd(t),
not: ¬A,
and: P ∧ Q,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
not: ¬A,
equal: s = t ∈ T,
list: T List,
int: ℤ,
pi2: snd(t),
assert: ↑b,
imonomial-le: imonomial-le(m1;m2)
FDL editor aliases :
imonomial-less
Latex:
imonomial-less(m1;m2) == (\mneg{}((snd(m1)) = (snd(m2)))) \mwedge{} (\muparrow{}imonomial-le(m1;m2))
Date html generated:
2016_05_14-AM-07_00_15
Last ObjectModification:
2015_09_22-PM-05_51_41
Theory : omega
Home
Index