---

Step * of Lemma int_term_value_functionality

∀[f:ℤ ⟶ ℤ]. ∀[t1,t2:int_term()].  int_term_value(f;t1) = int_term_value(f;t2) ∈ ℤ supposing t1 ≡ t2
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[t1,t2:int\_term()].    int\_term\_value(f;t1)  =  int\_term\_value(f;t2)  supposing  t1  \mequiv{}  t2


By

---

Latex:
Auto

---

Home Index