---

Step * 1 of Lemma isr-rep_int_constraint_step


1. f : IntConstraints ⟶ IntConstraints
2. p : IntConstraints
3. ∀p:IntConstraints
     (0 < dim(p) ⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p))))
4. ∀p:IntConstraints. (unsat(f p) ⇒ unsat(p))
5. ↑isr(rep_int_constraint_step(f;p))
6. n : ℤ
7. p1 : IntConstraints
8. dim(p1) < 0
9. ↑isr(rep_int_constraint_step(f;p1))
⊢ unsat(p1)
BY
{ (Assert ⌜False⌝⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  f  :  IntConstraints  {}\mrightarrow{}  IntConstraints
2.  p  :  IntConstraints
3.  \mforall{}p:IntConstraints
          (0  <  dim(p)
          {}\mRightarrow{}  (dim(f  p)  <  dim(p)
                \mvee{}  ((dim(f  p)  =  dim(p))  \mwedge{}  num-eq-constraints(f  p)  <  num-eq-constraints(p))))
4.  \mforall{}p:IntConstraints.  (unsat(f  p)  {}\mRightarrow{}  unsat(p))
5.  \muparrow{}isr(rep\_int\_constraint\_step(f;p))
6.  n  :  \mBbbZ{}
7.  p1  :  IntConstraints
8.  dim(p1)  <  0
9.  \muparrow{}isr(rep\_int\_constraint\_step(f;p1))
\mvdash{}  unsat(p1)


By

---

Latex:
(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto')

---

Home Index