---

Step * 3 1 of Lemma satisfies_int_formula_dnf


1. left : int_term()
2. right : int_term()
3. f : ℤ ⟶ ℤ
4. int_term_value(f;left) = int_term_value(f;right) ∈ ℤ
⊢ (int_term_value(f;right) + (-int_term_value(f;left))) = 0 ∈ ℤ
BY
{ (HypSubst' (-1) 0 THEN RW IntNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  left  :  int\_term()
2.  right  :  int\_term()
3.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
4.  int\_term\_value(f;left)  =  int\_term\_value(f;right)
\mvdash{}  (int\_term\_value(f;right)  +  (-int\_term\_value(f;left)))  =  0


By

---

Latex:
(HypSubst'  (-1)  0  THEN  RW  IntNormC  0  THEN  Auto)

---

Home Index