---

Step * 1 of Lemma satisfies-shadow_inequalities


1. [n] : {2...}
2. xs : ℤ List
3. (∀as∈[].xs ⋅ as ≥0)
⊢ ∃xs:ℤ List. (∀as∈[].xs ⋅ as ≥0)
BY
{ TACTIC:(With ⌜[]⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [n]  :  \{2...\}
2.  xs  :  \mBbbZ{}  List
3.  (\mforall{}as\mmember{}[].xs  \mcdot{}  as  \mgeq{}0)
\mvdash{}  \mexists{}xs:\mBbbZ{}  List.  (\mforall{}as\mmember{}[].xs  \mcdot{}  as  \mgeq{}0)


By

---

Latex:
TACTIC:(With  \mkleeneopen{}[]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index