---

Step * 2 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;ipolynomial-term(add_ipoly(int_term_to_ipoly(right);minus-poly(int_term_to_ipoly(left))))))
BY
{ ((RWW "add_ipoly-sq" 0 THENA Auto)
   THEN (Subst' int_term_value(f;ipolynomial-term(add-ipoly(int_term_to_ipoly(right);minus-poly(...))))
         = (int_term_value(f;right) + (-int_term_value(f;left)))
         ∈ ℤ 0
         THENA ((RWO "add-ipoly-equiv" 0 THENA Auto)
                THEN RepUR ``int_term_value`` 0
                THEN Fold `int_term_value` 0
                THEN (RWO "minus-poly-equiv" 0 THENA Auto)
                THEN RWO "int_term_polynomial" 0
                THEN Auto)
         )
   THEN Auto) }

---

Latex:

---

Latex:

1.  left  :  int\_term()
2.  right  :  int\_term()
3.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  int\_term\_value(f;left)  \mleq{}  int\_term\_value(f;right)
\mLeftarrow{}{}\mRightarrow{}  True
        \mwedge{}  (0 
              \mleq{}  int\_term\_value(f;ipolynomial-term(add\_ipoly(int\_term\_to\_ipoly(right);minus-poly(...)))))


By

---

Latex:
((RWW  "add\_ipoly-sq"  0  THENA  Auto)
  THEN  (Subst'  int\_term\_value(f;ipolynomial-term(add-ipoly(int\_term\_to\_ipoly(right);...)))
              =  (int\_term\_value(f;right)  +  (-int\_term\_value(f;left)))  0
              THENA  ((RWO  "add-ipoly-equiv"  0  THENA  Auto)
                            THEN  RepUR  ``int\_term\_value``  0
                            THEN  Fold  `int\_term\_value`  0
                            THEN  (RWO  "minus-poly-equiv"  0  THENA  Auto)
                            THEN  RWO  "int\_term\_polynomial"  0
                            THEN  Auto)
              )
  THEN  Auto)

---

Home Index