---

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

1
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))))

---

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;ipolynomial-term(add-ipoly(int\_term\_to\_ipoly(right);minus-poly(...)))))


By

---

Latex:
(Fold  `const-poly`  0
  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)  +  1)))  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  (RepUR  ``int\_term\_value``  0  THEN  Fold  `int\_term\_value`  0)
                            THEN  (RWO  "add-ipoly-equiv"  0  THENA  Auto)
                            THEN  RepUR  ``int\_term\_value``  0
                            THEN  Fold  `int\_term\_value`  0
                            THEN  RWO  "int\_term\_polynomial  const-poly-value"  0
                            THEN  Auto)
              )
  )

---

Home Index