---

Step * of Lemma isr-rep_int_constraint_step

∀[f:IntConstraints ⟶ IntConstraints]. ∀[p:IntConstraints].
  (unsat(p)) supposing 
     ((↑isr(rep_int_constraint_step(f;p))) and 
     ((∀p:IntConstraints
         (0 < dim(p)
         ⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p)))))
     ∧ (∀p:IntConstraints. (unsat(f p) ⇒ unsat(p)))))
BY
{ (Auto
   THEN (Assert ⌜∀n:ℕ. ∀p:IntConstraints.  (dim(p) < n ⇒ (↑isr(rep_int_constraint_step(f;p))) ⇒ unsat(p))⌝⋅
   THENM (InstHyp [⌜dim(p) + 1⌝] (-1)⋅ THEN Auto)
   )
   THEN InductionOnNat
   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. p1 : IntConstraints
8. dim(p1) < 0
9. ↑isr(rep_int_constraint_step(f;p1))
⊢ unsat(p1)

2
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))
⊢ unsat(p1)

---

Latex:

---

Latex:
\mforall{}[f:IntConstraints  {}\mrightarrow{}  IntConstraints].  \mforall{}[p:IntConstraints].
    (unsat(p))  supposing 
          ((\muparrow{}isr(rep\_int\_constraint\_step(f;p)))  and 
          ((\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)))))
          \mwedge{}  (\mforall{}p:IntConstraints.  (unsat(f  p)  {}\mRightarrow{}  unsat(p)))))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}p:IntConstraints.
                                  (dim(p)  <  n  {}\mRightarrow{}  (\muparrow{}isr(rep\_int\_constraint\_step(f;p)))  {}\mRightarrow{}  unsat(p))\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}dim(p)  +  1\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto)

---

Home Index