---

Step * of Lemma satisfiable-exact-reduce-constraints

∀eqs:ℤ List List. ∀i:ℕ||eqs||. ∀j:ℕ+||eqs[i]||.
  ∀ineqs:ℤ List List
    (satisfiable(eqs;ineqs)
    ⇒ satisfiable(exact-reduce-constraints(eqs[i];j;eqs);exact-reduce-constraints(eqs[i];j;ineqs))) 
  supposing exact-eq-constraint(eqs;i;j)
BY
{ TACTIC:(Auto
          THEN D -1
          THEN (FLemma `satisfies-integer-problem-length` [-1] THENA Auto)
          THEN D -1
          THEN (Assert ||eqs[i]|| ~ ||xs|| BY
                      Auto)
          THEN (Assert eqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ}  List BY
                      (HypSubst' (-1) 0 THEN BLemma `list-set-type2`  THEN Auto))
          THEN (Assert ineqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ}  List BY
                      (HypSubst' (-2) 0 THEN BLemma `list-set-type2`  THEN Auto))) }

1
1. eqs : ℤ List List
2. i : ℕ||eqs||
3. j : ℕ+||eqs[i]||
4. exact-eq-constraint(eqs;i;j)
5. ineqs : ℤ List List
6. xs : ℤ List
7. satisfies-integer-problem(eqs;ineqs;xs)
8. (∀e∈eqs.||e|| = ||xs|| ∈ ℤ)
9. (∀e∈ineqs.||e|| = ||xs|| ∈ ℤ)
10. ||eqs[i]|| ~ ||xs||
11. eqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ}  List
12. ineqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ}  List
⊢ satisfiable(exact-reduce-constraints(eqs[i];j;eqs);exact-reduce-constraints(eqs[i];j;ineqs))

---

Latex:

---

Latex:
\mforall{}eqs:\mBbbZ{}  List  List.  \mforall{}i:\mBbbN{}||eqs||.  \mforall{}j:\mBbbN{}\msupplus{}||eqs[i]||.
    \mforall{}ineqs:\mBbbZ{}  List  List
        (satisfiable(eqs;ineqs)
        {}\mRightarrow{}  satisfiable(exact-reduce-constraints(eqs[i];j;eqs);
                                      exact-reduce-constraints(eqs[i];j;ineqs))) 
    supposing  exact-eq-constraint(eqs;i;j)


By

---

Latex:
TACTIC:(Auto
                THEN  D  -1
                THEN  (FLemma  `satisfies-integer-problem-length`  [-1]  THENA  Auto)
                THEN  D  -1
                THEN  (Assert  ||eqs[i]||  \msim{}  ||xs||  BY
                                        Auto)
                THEN  (Assert  eqs  \mmember{}  \{l:\mBbbZ{}  List|  ||l||  =  ||eqs[i]||\}    List  BY
                                        (HypSubst'  (-1)  0  THEN  BLemma  `list-set-type2`    THEN  Auto))
                THEN  (Assert  ineqs  \mmember{}  \{l:\mBbbZ{}  List|  ||l||  =  ||eqs[i]||\}    List  BY
                                        (HypSubst'  (-2)  0  THEN  BLemma  `list-set-type2`    THEN  Auto)))

---

Home Index