---

Step * of Lemma satisfies_int_formula_dnf

∀fmla:int_formula(). ∀f:ℤ ⟶ ℤ.
  (int_formula_prop(f;fmla) ⇐⇒ (∃X∈int_formula_dnf(fmla). satisfies-poly-constraints(f;X)))
BY
{ ((BLemma `int_formula-induction` THENA Auto)
   THEN (UnivCD THENA Auto)
   THEN ((Unfolds ``int_formula_dnf`` 0
          THEN Reduce 0
          THEN Fold `int_formula_dnf` 0
          THEN RepUR
          ``int_formula_prop`` 0⋅
          THEN Fold `int_formula_prop` 0)
   ORELSE (Unfolds ``int_formula_dnf`` 0
           THEN Reduce 0
           THEN (RWO "l_exists_single" 0 THENA Auto)
           THEN RepUR ``satisfies-poly-constraints int_formula_prop`` 0
           THEN (RWO "l_all_nil_iff l_all_single" 0 THENA Auto)
           THEN RepUR ``int_term_to_ipoly`` 0
           THEN Fold `int_term_to_ipoly` 0)
   )) }

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;ipolynomial-term(add_ipoly(int_term_to_ipoly(right);minus-poly(add_ipoly(...;[<1, []>]))))))

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

3
1. left : int_term()
2. right : int_term()
3. f : ℤ ⟶ ℤ
⊢ int_term_value(f;left) = int_term_value(f;right) ∈ ℤ
⇐⇒ (int_term_value(f;ipolynomial-term(add_ipoly(int_term_to_ipoly(right);minus-poly(int_term_to_ipoly(left)))))
    = 0
    ∈ ℤ)
    ∧ True

4
1. left : int_formula()
2. right : int_formula()
3. ∀f:ℤ ⟶ ℤ. (int_formula_prop(f;left) ⇐⇒ (∃X∈int_formula_dnf(left). satisfies-poly-constraints(f;X)))
4. ∀f:ℤ ⟶ ℤ. (int_formula_prop(f;right) ⇐⇒ (∃X∈int_formula_dnf(right). satisfies-poly-constraints(f;X)))
5. f : ℤ ⟶ ℤ
⊢ int_formula_prop(f;left) ∧ int_formula_prop(f;right)
⇐⇒ (∃X∈and-poly-constraints(int_formula_dnf(left);int_formula_dnf(right)). satisfies-poly-constraints(f;X))

5
1. left : int_formula()
2. right : int_formula()
3. ∀f:ℤ ⟶ ℤ. (int_formula_prop(f;left) ⇐⇒ (∃X∈int_formula_dnf(left). satisfies-poly-constraints(f;X)))
4. ∀f:ℤ ⟶ ℤ. (int_formula_prop(f;right) ⇐⇒ (∃X∈int_formula_dnf(right). satisfies-poly-constraints(f;X)))
5. f : ℤ ⟶ ℤ
⊢ int_formula_prop(f;left) ∨ int_formula_prop(f;right)
⇐⇒ (∃X∈int_formula_dnf(left) @ int_formula_dnf(right). satisfies-poly-constraints(f;X))

6
1. left : int_formula()
2. right : int_formula()
3. ∀f:ℤ ⟶ ℤ. (int_formula_prop(f;left) ⇐⇒ (∃X∈int_formula_dnf(left). satisfies-poly-constraints(f;X)))
4. ∀f:ℤ ⟶ ℤ. (int_formula_prop(f;right) ⇐⇒ (∃X∈int_formula_dnf(right). satisfies-poly-constraints(f;X)))
5. f : ℤ ⟶ ℤ
⊢ int_formula_prop(f;left) ⇒ int_formula_prop(f;right)
⇐⇒ (∃X∈negate-poly-constraints(int_formula_dnf(left)) @ int_formula_dnf(right). satisfies-poly-constraints(f;X))

7
1. form : int_formula()
2. ∀f:ℤ ⟶ ℤ. (int_formula_prop(f;form) ⇐⇒ (∃X∈int_formula_dnf(form). satisfies-poly-constraints(f;X)))
3. f : ℤ ⟶ ℤ
⊢ ¬int_formula_prop(f;form) ⇐⇒ (∃X∈negate-poly-constraints(int_formula_dnf(form)). satisfies-poly-constraints(f;X))

---

Latex:

---

Latex:
\mforall{}fmla:int\_formula().  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.
    (int\_formula\_prop(f;fmla)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}int\_formula\_dnf(fmla).  satisfies-poly-constraints(f;X)))


By

---

Latex:
((BLemma  `int\_formula-induction`  THENA  Auto)
  THEN  (UnivCD  THENA  Auto)
  THEN  ((Unfolds  ``int\_formula\_dnf``  0
                THEN  Reduce  0
                THEN  Fold  `int\_formula\_dnf`  0
                THEN  RepUR
                ``int\_formula\_prop``  0\mcdot{}
                THEN  Fold  `int\_formula\_prop`  0)
  ORELSE  (Unfolds  ``int\_formula\_dnf``  0
                  THEN  Reduce  0
                  THEN  (RWO  "l\_exists\_single"  0  THENA  Auto)
                  THEN  RepUR  ``satisfies-poly-constraints  int\_formula\_prop``  0
                  THEN  (RWO  "l\_all\_nil\_iff  l\_all\_single"  0  THENA  Auto)
                  THEN  RepUR  ``int\_term\_to\_ipoly``  0
                  THEN  Fold  `int\_term\_to\_ipoly`  0)
  ))

---

Home Index