---

Step * of Lemma omega_step_measure

∀p:IntConstraints
  (0 < dim(p)
  ⇒ (dim((λp.omega_step(p)) p) < dim(p)
     ∨ ((dim((λp.omega_step(p)) p) = dim(p) ∈ ℤ) ∧ num-eq-constraints((λp.omega_step(p)) p) < num-eq-constraints(p))))
BY
{ (Auto
   THEN (Decide dim(omega_step(p)) < dim(p) THENA Auto)
   THEN (Complete (Auto) ORELSE (OrRight THENA Auto))
   THEN ((SupposeNot THENA Auto) THEN Assert ⌜False⌝⋅)
   THEN Auto) }

1
.....assertion..... 
1. p : IntConstraints
2. 0 < dim(p)
3. ¬dim(omega_step(p)) < dim(p)
4. ¬((dim((λp.omega_step(p)) p) = dim(p) ∈ ℤ) ∧ num-eq-constraints((λp.omega_step(p)) p) < num-eq-constraints(p))
⊢ False

---

Latex:

---

Latex:
\mforall{}p:IntConstraints
    (0  <  dim(p)
    {}\mRightarrow{}  (dim((\mlambda{}p.omega\_step(p))  p)  <  dim(p)
          \mvee{}  ((dim((\mlambda{}p.omega\_step(p))  p)  =  dim(p))
              \mwedge{}  num-eq-constraints((\mlambda{}p.omega\_step(p))  p)  <  num-eq-constraints(p))))


By

---

Latex:
(Auto
  THEN  (Decide  dim(omega\_step(p))  <  dim(p)  THENA  Auto)
  THEN  (Complete  (Auto)  ORELSE  (OrRight  THENA  Auto))
  THEN  ((SupposeNot  THENA  Auto)  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{})
  THEN  Auto)

---

Home Index