Step
*
of Lemma
poly-int-val_wf
∀[n:ℕ]. ∀[p:polyform(n)]. ∀[l:{l:ℤ List| n ≤ ||l||} ].  (p@l ∈ ℤ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p:polyform(n)].  \mforall{}[l:\{l:\mBbbZ{}  List|  n  \mleq{}  ||l||\}  ].    (p@l  \mmember{}  \mBbbZ{})
By
Latex:
ProveWfLemma
Home
Index