---

Step * of Lemma satisfies-shadow_inequalities

∀[n:{2...}]
  ∀ineqs:{L:ℤ List| ||L|| = n ∈ ℤ}  List
    ((∃xs:ℤ List. (∀as∈ineqs.xs ⋅ as ≥0)) ⇒ (∃xs:ℤ List. (∀as∈shadow_inequalities(ineqs).xs ⋅ as ≥0)))
BY
{ TACTIC:(Auto THEN ExRepD THEN DVar `ineqs' THEN RepUR ``shadow_inequalities`` 0) }

1
1. [n] : {2...}
2. xs : ℤ List
3. (∀as∈[].xs ⋅ as ≥0)
⊢ ∃xs:ℤ List. (∀as∈[].xs ⋅ as ≥0)

2
1. [n] : {2...}
2. u : {L:ℤ List| ||L|| = n ∈ ℤ} 
3. v : {L:ℤ List| ||L|| = n ∈ ℤ}  List
4. xs : ℤ List
5. (∀as∈[u / v].xs ⋅ as ≥0)
⊢ ∃xs:ℤ List. (∀as∈eval i = index-of-min(max_tl_coeffs([u / v])) + 1 in shadow-inequalities(i;[u / v]).xs ⋅ as ≥0)

---

Latex:

---

Latex:
\mforall{}[n:\{2...\}]
    \mforall{}ineqs:\{L:\mBbbZ{}  List|  ||L||  =  n\}    List
        ((\mexists{}xs:\mBbbZ{}  List.  (\mforall{}as\mmember{}ineqs.xs  \mcdot{}  as  \mgeq{}0))
        {}\mRightarrow{}  (\mexists{}xs:\mBbbZ{}  List.  (\mforall{}as\mmember{}shadow\_inequalities(ineqs).xs  \mcdot{}  as  \mgeq{}0)))


By

---

Latex:
TACTIC:(Auto  THEN  ExRepD  THEN  DVar  `ineqs'  THEN  RepUR  ``shadow\_inequalities``  0)

---

Home Index