---

Step * 1 of Lemma omega_step_measure

.....assertion..... 
1. p : IntConstraints
2. 0 < dim(p)
3. ¬dim(omega_step(p)) < dim(p)
4. ¬((dim((λp.omega_step(p)) p) = dim(p) ∈ ℤ) ∧ num-eq-constraints((λp.omega_step(p)) p) < num-eq-constraints(p))
⊢ False
BY
{ TACTIC:((Assert ¬dim(p) < 1 BY
                 Auto)
          THEN All (Unfold `omega_step`)
          THEN (All Reduce THENA Auto)
          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 ((RepeatFor 2 (Thin (-3))
                 THEN Eliminate ⌜n⌝⋅
                 THEN D -2
                 THEN DVar `eqs'
                 THEN Reduce 0
                 THEN DSetVars
                 THEN Try ((HypSubst' 3 0 THEN Auto))
                 THEN DVar `ineqs'
                 THEN Reduce 0
                 THEN DSetVars
                 THEN Try (HypSubst' 3 0)
                 THEN Auto)
          ORELSE (Thin (-2)
                  THEN RepeatFor 2 (MoveToConcl (-2))
                  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)⌝;⌜eqs⌝]⋅
                        THENA Auto
                        )
                  THEN (GenConclTerm ⌜first-success(λL.find-exact-eq-constraint(L);eqs)⌝⋅ THENA Auto)
                  THEN 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. 0 < dim(inl <eqs, ineqs>)
5. ¬(n = 0 ∈ ℤ)
6. 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 ∈ ℤ} ?
7. x : i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}  × {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} 
8. first-success(λL.find-exact-eq-constraint(L);eqs)
= (inl x)
∈ (i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}  × {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?)
⊢ (¬dim(let i,wj = x 
        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 ) < dim(inl <eqs, ineqs>))
⇒ (¬((dim(let i,wj = x 
           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 )
   = dim(inl <eqs, ineqs>)
   ∈ ℤ)
   ∧ num-eq-constraints(let i,wj = x 
                        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 ) < num-eq-constraints(inl <eqs, ineqs>)))
⇒ False

2
1. n : ℕ
2. eqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. 0 < dim(inl <eqs, ineqs>)
5. ¬(n = 0 ∈ ℤ)
6. 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 ∈ ℤ} ?
7. y : Unit
8. first-success(λL.find-exact-eq-constraint(L);eqs)
= (inr y )
∈ (i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}  × {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?)
⊢ (¬dim(if null(eqs)
  then case gcd-reduce-ineq-constraints([];shadow_inequalities(ineqs)) of inl(ineqs') => inl <[], ineqs'> | inr(x) => in\000Cr x 
  else inl <[], (eager-map(λeq.eager-map(λx.(-x);eq);eqs) @ eqs) @ ineqs>
  fi ) < dim(inl <eqs, ineqs>))
⇒ (¬((dim(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 )
   = dim(inl <eqs, ineqs>)
   ∈ ℤ)
   ∧ num-eq-constraints(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 ) < num-eq-constraints(inl <eqs, ineqs>)))
⇒ False

---

Latex:

---

Latex:
.....assertion..... 
1.  p  :  IntConstraints
2.  0  <  dim(p)
3.  \mneg{}dim(omega\_step(p))  <  dim(p)
4.  \mneg{}((dim((\mlambda{}p.omega\_step(p))  p)  =  dim(p))
\mwedge{}  num-eq-constraints((\mlambda{}p.omega\_step(p))  p)  <  num-eq-constraints(p))
\mvdash{}  False


By

---

Latex:
TACTIC:((Assert  \mneg{}dim(p)  <  1  BY
                              Auto)
                THEN  All  (Unfold  `omega\_step`)
                THEN  (All  Reduce  THENA  Auto)
                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  ((RepeatFor  2  (Thin  (-3))
                              THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
                              THEN  D  -2
                              THEN  DVar  `eqs'
                              THEN  Reduce  0
                              THEN  DSetVars
                              THEN  Try  ((HypSubst'  3  0  THEN  Auto))
                              THEN  DVar  `ineqs'
                              THEN  Reduce  0
                              THEN  DSetVars
                              THEN  Try  (HypSubst'  3  0)
                              THEN  Auto)
                ORELSE  (Thin  (-2)
                                THEN  RepeatFor  2  (MoveToConcl  (-2))
                                THEN  (InstLemma  `first-success\_wf`  [\mkleeneopen{}\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}  \mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}L.x:\{x:\mBbbZ{}  List|\000C 
                                                                                                                                                                                    x  =  L\} 
                                                                                                                                                                      \mtimes{}  \{i:\mBbbN{}\msupplus{}||L||| 
                                                                                                                                                                            |L[i]|  =  1\}  \mkleeneclose{};\000C 
                                            \mkleeneopen{}\mlambda{}L.find-exact-eq-constraint(L)\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)
                ))

---

Home Index