---

Step * 1 1 of Lemma omega_step_wf


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
5. n = 0 ∈ ℤ
⊢ 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
BY
{ TACTIC:(Eliminate ⌜n⌝⋅ THEN D -2 THEN DVar `eqs' THEN Reduce 0 THEN DSetVars) }

1
1. n : ℕ
2. ineqs : {L:ℤ List| ||L|| = (0 + 1) ∈ ℤ}  List
3. n = 0 ∈ ℤ
⊢ if ineqs = Ax then 0 otherwise ||hd(ineqs)|| - 1 < 1

2
1. n : ℕ
2. u : ℤ List
3. ||u|| = (0 + 1) ∈ ℤ
4. v : {L:ℤ List| ||L|| = (0 + 1) ∈ ℤ}  List
5. ineqs : {L:ℤ List| ||L|| = (0 + 1) ∈ ℤ}  List
6. n = 0 ∈ ℤ
⊢ ||u|| - 1 < 1

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  eqs  :  \{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List
3.  ineqs  :  \{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List
4.  \mneg{}if  eqs  =  Ax  then  if  ineqs  =  Ax  then  0  otherwise  ||hd(ineqs)||  -  1  otherwise  ||hd(eqs)||  -  1  <  1
5.  n  =  0
\mvdash{}  let  eqs,ineqs  =  <eqs,  ineqs> 
    in  case  first-success(\mlambda{}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(\mlambda{}eq.eager-map(\mlambda{}x.(-x);eq);eqs)  @  eqs)  @  ineqs>
            fi    \mmember{}  IntConstraints


By

---

Latex:
TACTIC:(Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}  THEN  D  -2  THEN  DVar  `eqs'  THEN  Reduce  0  THEN  DSetVars)

---

Home Index