---

Step * 1 2 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:(Thin (-2) THEN Reduce 0) }

1
1. n : ℕ
2. eqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. ¬(n = 0 ∈ ℤ)
⊢ 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:

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.  \mneg{}(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:(Thin  (-2)  THEN  Reduce  0)

---

Home Index