---

Step * of Lemma omega_start_wf

∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List].  (omega_start(eqs;ineqs) ∈ IntConstraints)
BY
{ (Auto
   THEN Unfold `omega_start` 0
   THEN (GenConcl ⌜gcd-reduce-eq-constraints([];eqs) = xxx ∈ ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?)⌝⋅
         THENA (Try (BLemma `gcd-reduce-eq-constraints_wf2`) THEN Auto)
         )
   THEN (GenConcl ⌜gcd-reduce-ineq-constraints([];ineqs) = yyy ∈ ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?)⌝⋅
         THENA (Try (BLemma `gcd-reduce-ineq-constraints_wf2`) THEN Auto)
         )) }

1
1. n : ℕ
2. eqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. xxx : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?
5. gcd-reduce-eq-constraints([];eqs) = xxx ∈ ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?)
6. yyy : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?
7. gcd-reduce-ineq-constraints([];ineqs) = yyy ∈ ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?)
⊢ case xxx of inl(eqs') => case yyy of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x  | inr(x) => inr x 
  ∈ IntConstraints

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[eqs,ineqs:\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List].    (omega\_start(eqs;ineqs)  \mmember{}  IntConstraints)


By

---

Latex:
(Auto
  THEN  Unfold  `omega\_start`  0
  THEN  (GenConcl  \mkleeneopen{}gcd-reduce-eq-constraints([];eqs)  =  xxx\mkleeneclose{}\mcdot{}
              THENA  (Try  (BLemma  `gcd-reduce-eq-constraints\_wf2`)  THEN  Auto)
              )
  THEN  (GenConcl  \mkleeneopen{}gcd-reduce-ineq-constraints([];ineqs)  =  yyy\mkleeneclose{}\mcdot{}
              THENA  (Try  (BLemma  `gcd-reduce-ineq-constraints\_wf2`)  THEN  Auto)
              ))

---

Home Index