---

Step * of Lemma omega_step_wf

∀[p:IntConstraints]. (omega_step(p) ∈ IntConstraints)
BY
{ TACTIC:((D 0 THENA Auto)
          THEN Unfold `omega_step` 0
          THEN AutoSplit
          THEN D 1
          THEN Try ((D_union 1 THEN D 2))
          THEN ((RenameVar `eqs' 2 THEN RenameVar `ineqs' 3 THEN RepUR ``int-problem-dimension`` -1)
          ORELSE (RepUR ``int-problem-dimension`` 0 THEN Auto)
          )) }

1
1. n : ℕ
2. eqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. ¬if eqs = Ax then if ineqs = Ax then 0 otherwise ||hd(ineqs)|| - 1 otherwise ||hd(eqs)|| - 1 < 1
⊢ let eqs,ineqs = <eqs, ineqs> 
  in case first-success(λL.find-exact-eq-constraint(L);eqs)
      of inl(tr) =>
      let i,wj = tr 
      in let w,j = wj 
         in case gcd-reduce-eq-constraints([];exact-reduce-constraints(w;j;eqs))
             of inl(eqs') =>
             case gcd-reduce-ineq-constraints([];exact-reduce-constraints(w;j;ineqs))
              of inl(ineqs') =>
              inl <eqs', ineqs'>
              | inr(x) =>
              inr x 
             | inr(x) =>
             inr x 
      | inr(_) =>
      if null(eqs)
      then case gcd-reduce-ineq-constraints([];shadow_inequalities(ineqs))
            of inl(ineqs') =>
            inl <[], ineqs'>
            | inr(x) =>
            inr x 
      else inl <[], (eager-map(λeq.eager-map(λx.(-x);eq);eqs) @ eqs) @ ineqs>
      fi  ∈ IntConstraints

---

Latex:

---

Latex:
\mforall{}[p:IntConstraints].  (omega\_step(p)  \mmember{}  IntConstraints)


By

---

Latex:
TACTIC:((D  0  THENA  Auto)
                THEN  Unfold  `omega\_step`  0
                THEN  AutoSplit
                THEN  D  1
                THEN  Try  ((D\_union  1  THEN  D  2))
                THEN  ((RenameVar  `eqs'  2  THEN  RenameVar  `ineqs'  3  THEN  RepUR  ``int-problem-dimension``  -1)
                ORELSE  (RepUR  ``int-problem-dimension``  0  THEN  Auto)
                ))

---

Home Index