Step
*
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;ipolynomial-term(add_ipoly(int_term_to_ipoly(right);minus-poly(add_ipoly(...;[<1, []>]))))))
BY
{ (RWW "add_ipoly-sq" 0 THENA Auto) }
1
1. left : int_term()
2. right : int_term()
3. f : ℤ ⟶ ℤ
⊢ [<1, []>] ∈ iPolynomial()
2
.....subterm..... T:t
2:n
1. left : int_term()
2. right : int_term()
3. f : ℤ ⟶ ℤ
⊢ [] ∈ {vs:ℤ List| sorted(vs)} 
3
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, []>]))))))
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:
(RWW  "add\_ipoly-sq"  0  THENA  Auto)
Home
Index