Proof of Nuprl Lemma : omega_step

Step * 1 1 1 of Lemma omega_step_measure

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. i : ℕ||eqs||
8. x : {x:ℤ List| x = eqs[i] ∈ (ℤ List)}
9. x2 : {i@0:ℕ⁺||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ}
10. first-success(λL.find-exact-eq-constraint(L);eqs)
= (inl <i, x, x2>)

∈ (i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}  × {i@0:ℕ⁺||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?)

⊢ (¬dim(case gcd-reduce-eq-constraints([];exact-reduce-constraints(x;x2;eqs))
   of inl(eqs') =>
   case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs))
    of inl(ineqs') =>
    inl <eqs', ineqs'>
    | inr(x) =>
    inr x
   | inr(x) =>
   inr x ) < dim(inl <eqs, ineqs>))
⇒ (¬((dim(case gcd-reduce-eq-constraints([];exact-reduce-constraints(x;x2;eqs))
    of inl(eqs') =>
    case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs))
     of inl(ineqs') =>
     inl <eqs', ineqs'>
     | inr(x) =>
     inr x
    | inr(x) =>
    inr x )
   = dim(inl <eqs, ineqs>)
   ∈ ℤ)
   ∧ num-eq-constraints(case gcd-reduce-eq-constraints([];exact-reduce-constraints(x;x2;eqs))
      of inl(eqs') =>
      case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs))
       of inl(ineqs') =>
       inl <eqs', ineqs'>
       | inr(x) =>
       inr x
      | inr(x) =>
      inr x ) < num-eq-constraints(inl <eqs, ineqs>)))
⇒ False
BY

{ TACTIC:((GenConcl ⌜exact-reduce-constraints(x;x2;eqs) = xx ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ}  List)⌝⋅

           THENA (Auto
                  THEN DVar `x'
                  THEN MemTypeCD
                  THEN Auto
                  THEN (Eliminate ⌜x⌝⋅ THEN GenConclTerm ⌜eqs[i]⌝⋅)
                  THEN Auto)
           )

          THEN (GenConcl ⌜gcd-reduce-eq-constraints([];xx) = xxx ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ}  List?)⌝⋅

                THENA (Try (BLemma `gcd-reduce-eq-constraints_wf2`) THEN 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. i : ℕ||eqs||
8. x : {x:ℤ List| x = eqs[i] ∈ (ℤ List)}
9. x2 : {i@0:ℕ⁺||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ}
10. first-success(λL.find-exact-eq-constraint(L);eqs)
= (inl <i, x, x2>)

∈ (i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}  × {i@0:ℕ⁺||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?)

11. xx : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ}  List
12. exact-reduce-constraints(x;x2;eqs) = xx ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ}  List)
13. x3 : {L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ}  List

14. gcd-reduce-eq-constraints([];xx) = (inl x3) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ}  List?)

⊢ (¬dim(case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs))
   of inl(ineqs') =>
   inl <x3, ineqs'>
   | inr(x) =>
   inr x ) < dim(inl <eqs, ineqs>))
⇒ (¬((dim(case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs))
    of inl(ineqs') =>
    inl <x3, ineqs'>
    | inr(x) =>
    inr x )
   = dim(inl <eqs, ineqs>)
   ∈ ℤ)
   ∧ num-eq-constraints(case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs))
      of inl(ineqs') =>
      inl <x3, ineqs'>
      | 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. i : ℕ||eqs||
8. x : {x:ℤ List| x = eqs[i] ∈ (ℤ List)}
9. x2 : {i@0:ℕ⁺||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ}
10. first-success(λL.find-exact-eq-constraint(L);eqs)
= (inl <i, x, x2>)

∈ (i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}  × {i@0:ℕ⁺||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?)

11. xx : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
12. exact-reduce-constraints(x;x2;eqs) = xx ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
13. y : Unit

14. gcd-reduce-eq-constraints([];xx) = (inr y ) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ}  List?)

⊢ (¬dim(inr y ) < dim(inl <eqs, ineqs>))
⇒

 (¬((dim(inr y ) = dim(inl <eqs, ineqs>) ∈ ℤ) ∧ num-eq-constraints(inr y ) < num-eq-constraints(inl <eqs, ineqs>)))

⇒ False

Latex:

Latex:
1. n : \mBbbN{} 2. eqs : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List 3. ineqs : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List 4. 0 < dim(inl <eqs, ineqs>) 5. \mneg{}(n = 0) 6. first-success(\mlambda{}L.find-exact-eq-constraint(L);eqs) \mmember{} i:\mBbbN{}||eqs|| \mtimes{} x:\{x:\mBbbZ{} List| x = eqs[i]\} \mtimes{} \{i@0:\mBbbN{}\msupplus{}||eqs[i]||| |eqs[i][i@0]| = 1\} ? 7. i : \mBbbN{}||eqs|| 8. x : \{x:\mBbbZ{} List| x = eqs[i]\} 9. x2 : \{i@0:\mBbbN{}\msupplus{}||eqs[i]||| |eqs[i][i@0]| = 1\} 10. first-success(\mlambda{}L.find-exact-eq-constraint(L);eqs) = (inl <i, x, x2>) \mvdash{} (\mneg{}dim(case gcd-reduce-eq-constraints([];exact-reduce-constraints(x;x2;eqs)) of inl(eqs') => case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs)) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x | inr(x) => inr x ) < dim(inl <eqs, ineqs>)) {}\mRightarrow{} (\mneg{}((dim(case gcd-reduce-eq-constraints([];exact-reduce-constraints(x;x2;eqs)) of inl(eqs') => case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs)) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x | inr(x) => inr x ) = dim(inl <eqs, ineqs>)) \mwedge{} num-eq-constraints(case gcd-reduce-eq-constraints([];exact-reduce-constraints(x;x2;eqs)) of inl(eqs') => case gcd-reduce-ineq-constraints([];exact-reduce-constraints(x;x2;ineqs)) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x | inr(x) => inr x ) < num-eq-constraints(inl <eqs, ineqs>))) {}\mRightarrow{} False By Latex: TACTIC:((GenConcl \mkleeneopen{}exact-reduce-constraints(x;x2;eqs) = xx\mkleeneclose{}\mcdot{} THENA (Auto THEN DVar `x' THEN MemTypeCD THEN Auto THEN (Eliminate \mkleeneopen{}x\mkleeneclose{}\mcdot{} THEN GenConclTerm \mkleeneopen{}eqs[i]\mkleeneclose{}\mcdot{}) THEN Auto) ) THEN (GenConcl \mkleeneopen{}gcd-reduce-eq-constraints([];xx) = xxx\mkleeneclose{}\mcdot{} THENA (Try (BLemma `gcd-reduce-eq-constraints\_wf2`) THEN Auto) ) THEN D -2 THEN Reduce 0) Home Index