Step
*
of Lemma
real_term_value_wf
∀[f:ℤ ⟶ ℝ]. ∀[t:int_term()].  (real_term_value(f;t) ∈ ℝ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[t:int\_term()].    (real\_term\_value(f;t)  \mmember{}  \mBbbR{})
By
Latex:
ProveWfLemma
Home
Index