---

Step * 3 2 of Lemma satisfies_int_formula_dnf


1. left : int_term()
2. right : int_term()
3. f : ℤ ⟶ ℤ
4. (int_term_value(f;right) + (-int_term_value(f;left))) = 0 ∈ ℤ
5. True
⊢ int_term_value(f;left) = int_term_value(f;right) ∈ ℤ
BY
{ (Add ⌜int_term_value(f;left)⌝ (-2)⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Add  \mkleeneopen{}int\_term\_value(f;left)\mkleeneclose{}  (-2)\mcdot{}  THEN  Auto)

---

Home Index