---

Step * of Lemma isr-omega

∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List].  ¬satisfiable(eqs;ineqs) supposing ↑isr(omega(eqs;ineqs))
BY
{ (Auto
   THEN Unfold `omega` -1
   THEN (CallByValueReduce (-1) THENA Auto)
   THEN FLemma `isr-rep_int_constraint_step` [-1]
   THEN Auto
   THEN Try ((BLemma `omega_step_measure` THEN Auto))
   THEN Reduce (-1)
   THEN (BLemma `unsat-omega_start` ORELSE BLemma `unsat-omega_step`)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[eqs,ineqs:\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List].
    \mneg{}satisfiable(eqs;ineqs)  supposing  \muparrow{}isr(omega(eqs;ineqs))


By

---

Latex:
(Auto
  THEN  Unfold  `omega`  -1
  THEN  (CallByValueReduce  (-1)  THENA  Auto)
  THEN  FLemma  `isr-rep\_int\_constraint\_step`  [-1]
  THEN  Auto
  THEN  Try  ((BLemma  `omega\_step\_measure`  THEN  Auto))
  THEN  Reduce  (-1)
  THEN  (BLemma  `unsat-omega\_start`  ORELSE  BLemma  `unsat-omega\_step`)
  THEN  Auto)

---

Home Index