---

Step * of Lemma unsat-omega_step

∀p:IntConstraints. (unsat(omega_step(p)) ⇒ unsat(p))
BY
{ (Auto
   THEN (Decide dim(p) < 1 THENA Auto)
   THEN (RepUR ``omega_step`` -2 THEN Try (Trivial))
   THEN UseWitness ⌜λxs,x. x⌝⋅
   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
   THEN Try ((D -1 THEN TrivialArith))
   THEN All Reduce
   THEN CaseNat 0 `n'
   THEN ((Eliminate ⌜n⌝⋅
          THEN DVar `eqs'
          THEN All Reduce
          THEN DSetVars
          THEN D -2
          THEN Auto
          THEN DVar `ineqs'
          THEN Reduce 0
          THEN DSetVars
          THEN Try (HypSubst' 3 0)
          THEN Auto)
   ORELSE (RepUR ``unsat-int-problem all not satisfies-int-constraint-problem`` 0
           THEN Auto
           THEN Assert ⌜False⌝⋅
           THEN Auto
           THEN MoveToConcl (-6)
           THEN (InstLemma `first-success_wf` [⌜{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} ⌝;
                 ⌜λ2L.x:{x:ℤ List| x = L ∈ (ℤ List)}  × {i:ℕ+||L||| |L[i]| = 1 ∈ ℤ} ⌝; ⌜λL.find-exact-eq-constraint(L)⌝;\000C⌜eqs⌝]⋅
                 THENA Auto
                 )
           THEN (GenConclTerm ⌜first-success(λL.find-exact-eq-constraint(L);eqs)⌝⋅ THENA Auto)
           THEN D -2
           THEN Reduce 0
           THEN RepeatFor 2 (D -2)
           THEN Reduce 0)
   )) }

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
5. ¬(n = 0 ∈ ℤ)
6. xs : ℤ List
7. x1 : (∀as∈eqs.xs ⋅ as =0)
8. x2 : (∀bs∈ineqs.xs ⋅ bs ≥0)
9. first-success(λL.find-exact-eq-constraint(L);eqs) ∈ i:ℕ||eqs||
   × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)} 
   × {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?
10. i : ℕ||eqs||
11. x : {x:ℤ List| x = eqs[i] ∈ (ℤ List)} 
12. x4 : {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} 
13. first-success(λL.find-exact-eq-constraint(L);eqs)
= (inl <i, x, x4>)
∈ (i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}  × {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?)
⊢ unsat(case gcd-reduce-eq-constraints([];exact-reduce-constraints(x;x4;eqs))
 of inl(eqs') =>
 case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x4;ineqs))
  of inl(ineqs') =>
  inl <eqs', ineqs'>
  | inr(x) =>
  inr x 
 | inr(x) =>
 inr x )
⇒ False

2
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 ∈ ℤ)
6. xs : ℤ List
7. x1 : (∀as∈eqs.xs ⋅ as =0)
8. x2 : (∀bs∈ineqs.xs ⋅ bs ≥0)
9. first-success(λL.find-exact-eq-constraint(L);eqs) ∈ i:ℕ||eqs||
   × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)} 
   × {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?
10. y : 0 = 0 ∈ ℤ
11. first-success(λL.find-exact-eq-constraint(L);eqs)
= (inr Ax )
∈ (i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}  × {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?)
⊢ unsat(if null(eqs)
then case gcd-reduce-ineq-constraints([];shadow_inequalities(ineqs)) of inl(ineqs') => inl <[], ineqs'> | inr(x) => inr \000Cx 
else inl <[], (eager-map(λeq.eager-map(λx.(-x);eq);eqs) @ eqs) @ ineqs>
fi )
⇒ False

---

Latex:

---

Latex:
\mforall{}p:IntConstraints.  (unsat(omega\_step(p))  {}\mRightarrow{}  unsat(p))


By

---

Latex:
(Auto
  THEN  (Decide  dim(p)  <  1  THENA  Auto)
  THEN  (RepUR  ``omega\_step``  -2  THEN  Try  (Trivial))
  THEN  UseWitness  \mkleeneopen{}\mlambda{}xs,x.  x\mkleeneclose{}\mcdot{}
  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
  THEN  Try  ((D  -1  THEN  TrivialArith))
  THEN  All  Reduce
  THEN  CaseNat  0  `n'
  THEN  ((Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
                THEN  DVar  `eqs'
                THEN  All  Reduce
                THEN  DSetVars
                THEN  D  -2
                THEN  Auto
                THEN  DVar  `ineqs'
                THEN  Reduce  0
                THEN  DSetVars
                THEN  Try  (HypSubst'  3  0)
                THEN  Auto)
  ORELSE  (RepUR  ``unsat-int-problem  all  not  satisfies-int-constraint-problem``  0
                  THEN  Auto
                  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                  THEN  Auto
                  THEN  MoveToConcl  (-6)
                  THEN  (InstLemma  `first-success\_wf`  [\mkleeneopen{}\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}  \mkleeneclose{};
                              \mkleeneopen{}\mlambda{}\msubtwo{}L.x:\{x:\mBbbZ{}  List|  x  =  L\}    \mtimes{}  \{i:\mBbbN{}\msupplus{}||L|||  |L[i]|  =  1\}  \mkleeneclose{};  \mkleeneopen{}\mlambda{}L.find-exact-eq-constraint(L\000C)\mkleeneclose{};\mkleeneopen{}eqs\mkleeneclose{}
                              ]\mcdot{}
                              THENA  Auto
                              )
                  THEN  (GenConclTerm  \mkleeneopen{}first-success(\mlambda{}L.find-exact-eq-constraint(L);eqs)\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  D  -2
                  THEN  Reduce  0
                  THEN  RepeatFor  2  (D  -2)
                  THEN  Reduce  0)
  ))

---

Home Index