---

Step * 1 3 1 of Lemma satisfies_int_formula_dnf


1. left : int_term()
2. right : int_term()
3. f : ℤ ⟶ ℤ
⊢ int_term_value(f;left) < int_term_value(f;right)
⇐⇒ True ∧ (0 ≤ (int_term_value(f;right) + (-(int_term_value(f;left) + 1))))
BY
{ Auto }

---

Latex:

---

Latex:

1.  left  :  int\_term()
2.  right  :  int\_term()
3.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  int\_term\_value(f;left)  <  int\_term\_value(f;right)
\mLeftarrow{}{}\mRightarrow{}  True  \mwedge{}  (0  \mleq{}  (int\_term\_value(f;right)  +  (-(int\_term\_value(f;left)  +  1))))


By

---

Latex:
Auto

---

Home Index