---

Step * of Lemma rep_int_constraint_step_wf

∀[f:IntConstraints ⟶ IntConstraints]. ∀[p:IntConstraints].
  rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ}  
  supposing ∀p:IntConstraints
              (0 < dim(p)
              ⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p))))
BY
{ 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))))
⊢ rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} 

---

Latex:

---

Latex:
\mforall{}[f:IntConstraints  {}\mrightarrow{}  IntConstraints].  \mforall{}[p:IntConstraints].
    rep\_int\_constraint\_step(f;p)  \mmember{}  \{p:IntConstraints|  dim(p)  =  0\}   
    supposing  \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))))


By

---

Latex:
Auto

---

Home Index