---

Step * of Lemma omega_wf

∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List].  (omega(eqs;ineqs) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} )
BY
{ (ProveWfLemma THEN BLemma `omega_step_measure` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[eqs,ineqs:\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List].
    (omega(eqs;ineqs)  \mmember{}  \{p:IntConstraints|  dim(p)  =  0\}  )


By

---

Latex:
(ProveWfLemma  THEN  BLemma  `omega\_step\_measure`  THEN  Auto)

---

Home Index