Step * 1 of Lemma satisfies_int_formula_dnf


1. left int_term()
2. right int_term()
3. : ℤ ⟶ ℤ
⊢ 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" THENA Auto) }

1
1. left int_term()
2. right int_term()
3. : ℤ ⟶ ℤ
⊢ [<1, []>] ∈ iPolynomial()

2
.....subterm..... T:t
2:n
1. left int_term()
2. right int_term()
3. : ℤ ⟶ ℤ
⊢ [] ∈ {vs:ℤ List| sorted(vs)} 

3
1. left int_term()
2. right int_term()
3. : ℤ ⟶ ℤ
⊢ 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