---

Step * 1 2 1 2 2 1 1 1 of Lemma satisfies-gcd-reduce-ineq-constraints


1. n : ℕ+
2. 1 = n ∈ ℤ
3. u : ℤ
4. 1 = 1 ∈ ℤ
5. v1 : {L:ℤ List| ||L|| = 1 ∈ ℤ}  List
6. ∀sat:{L:ℤ List| ||L|| = 1 ∈ ℤ}  List
     ((∀as∈sat.[1] ⋅ as ≥0)
     ⇒ (∀as∈v1.[1] ⋅ as ≥0)
     ⇒ ((↑isl(gcd-reduce-ineq-constraints(sat;v1))) ∧ (∀as∈outl(gcd-reduce-ineq-constraints(sat;v1)).[1] ⋅ as ≥0)))
7. sat : {L:ℤ List| ||L|| = 1 ∈ ℤ}  List
8. (∀as∈sat.[1] ⋅ as ≥0)
9. [1] ⋅ [u] ≥0
10. (∀as∈v1.[1] ⋅ as ≥0)
11. ¬u < 0
⊢ (↑isl(gcd-reduce-ineq-constraints([[u] / sat];v1)))
∧ (∀as∈outl(gcd-reduce-ineq-constraints([[u] / sat];v1)).[1] ⋅ as ≥0)
BY
{ ((InstHyp [⌜[[u] / sat]⌝] 6⋅ THEN Auto) THEN BLemma `l_all_cons` THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  1  =  n
3.  u  :  \mBbbZ{}
4.  1  =  1
5.  v1  :  \{L:\mBbbZ{}  List|  ||L||  =  1\}    List
6.  \mforall{}sat:\{L:\mBbbZ{}  List|  ||L||  =  1\}    List
          ((\mforall{}as\mmember{}sat.[1]  \mcdot{}  as  \mgeq{}0)
          {}\mRightarrow{}  (\mforall{}as\mmember{}v1.[1]  \mcdot{}  as  \mgeq{}0)
          {}\mRightarrow{}  ((\muparrow{}isl(gcd-reduce-ineq-constraints(sat;v1)))
                \mwedge{}  (\mforall{}as\mmember{}outl(gcd-reduce-ineq-constraints(sat;v1)).[1]  \mcdot{}  as  \mgeq{}0)))
7.  sat  :  \{L:\mBbbZ{}  List|  ||L||  =  1\}    List
8.  (\mforall{}as\mmember{}sat.[1]  \mcdot{}  as  \mgeq{}0)
9.  [1]  \mcdot{}  [u]  \mgeq{}0
10.  (\mforall{}as\mmember{}v1.[1]  \mcdot{}  as  \mgeq{}0)
11.  \mneg{}u  <  0
\mvdash{}  (\muparrow{}isl(gcd-reduce-ineq-constraints([[u]  /  sat];v1)))
\mwedge{}  (\mforall{}as\mmember{}outl(gcd-reduce-ineq-constraints([[u]  /  sat];v1)).[1]  \mcdot{}  as  \mgeq{}0)


By

---

Latex:
((InstHyp  [\mkleeneopen{}[[u]  /  sat]\mkleeneclose{}]  6\mcdot{}  THEN  Auto)  THEN  BLemma  `l\_all\_cons`  THEN  Auto)

---

Home Index