---

Step * 2 1 2 2 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. 0 < n
8. ∀p:IntConstraints. (dim(p) < n - 1 ⇒ (↑isr(rep_int_constraint_step(f;p))) ⇒ unsat(p))
9. p1 : IntConstraints
10. dim(p1) < n
11. ↑isr(rep_int_constraint_step(f;p1))
12. m : ℤ
13. 0 < m
14. ∀p:IntConstraints. (dim(p) < n ⇒ num-eq-constraints(p) < m - 1 ⇒ (↑isr(rep_int_constraint_step(f;p))) ⇒ unsat(p))
15. p2 : IntConstraints
16. ¬0 < dim(p2)
17. dim(p2) < n
18. num-eq-constraints(p2) < m
⊢ (↑isr(p2)) ⇒ unsat(p2)
BY
{ (DVar `p2' THEN Reduce 0 THEN Auto) }

1
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. 0 < n
8. ∀p:IntConstraints. (dim(p) < n - 1 ⇒ (↑isr(rep_int_constraint_step(f;p))) ⇒ unsat(p))
9. p1 : IntConstraints
10. dim(p1) < n
11. ↑isr(rep_int_constraint_step(f;p1))
12. m : ℤ
13. 0 < m
14. ∀p:IntConstraints. (dim(p) < n ⇒ num-eq-constraints(p) < m - 1 ⇒ (↑isr(rep_int_constraint_step(f;p))) ⇒ unsat(p))
15. y : Unit
16. ¬0 < dim(inr y )
17. dim(inr y ) < n
18. num-eq-constraints(inr y ) < m
19. True
⊢ unsat(inr y )

---

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.  0  <  n
8.  \mforall{}p:IntConstraints.  (dim(p)  <  n  -  1  {}\mRightarrow{}  (\muparrow{}isr(rep\_int\_constraint\_step(f;p)))  {}\mRightarrow{}  unsat(p))
9.  p1  :  IntConstraints
10.  dim(p1)  <  n
11.  \muparrow{}isr(rep\_int\_constraint\_step(f;p1))
12.  m  :  \mBbbZ{}
13.  0  <  m
14.  \mforall{}p:IntConstraints
            (dim(p)  <  n
            {}\mRightarrow{}  num-eq-constraints(p)  <  m  -  1
            {}\mRightarrow{}  (\muparrow{}isr(rep\_int\_constraint\_step(f;p)))
            {}\mRightarrow{}  unsat(p))
15.  p2  :  IntConstraints
16.  \mneg{}0  <  dim(p2)
17.  dim(p2)  <  n
18.  num-eq-constraints(p2)  <  m
\mvdash{}  (\muparrow{}isr(p2))  {}\mRightarrow{}  unsat(p2)


By

---

Latex:
(DVar  `p2'  THEN  Reduce  0  THEN  Auto)

---

Home Index