---

Step * 1 2 1 2 2 1 1 1 of Lemma satisfies-gcd-reduce-eq-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-eq-constraints(sat;v1))) ∧ (∀as∈outl(gcd-reduce-eq-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)
⊢ (↑isl(gcd-reduce-eq-constraints([[0] / sat];v1))) ∧ (∀as∈outl(gcd-reduce-eq-constraints([[0] / sat];v1)).[1] ⋅ as =0)
BY
{ ((InstHyp [⌜[[0] / sat]⌝] 6⋅ THEN Auto) THEN BLemma `l_all_cons` THEN Auto) }

1
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-eq-constraints(sat;v1))) ∧ (∀as∈outl(gcd-reduce-eq-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)
⊢ [1] ⋅ [0] =0

---

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  =0)
          {}\mRightarrow{}  (\mforall{}as\mmember{}v1.[1]  \mcdot{}  as  =0)
          {}\mRightarrow{}  ((\muparrow{}isl(gcd-reduce-eq-constraints(sat;v1)))
                \mwedge{}  (\mforall{}as\mmember{}outl(gcd-reduce-eq-constraints(sat;v1)).[1]  \mcdot{}  as  =0)))
7.  sat  :  \{L:\mBbbZ{}  List|  ||L||  =  (||[]||  +  1)\}    List
8.  (\mforall{}as\mmember{}sat.[1]  \mcdot{}  as  =0)
9.  [1]  \mcdot{}  [u]  =0
10.  (\mforall{}as\mmember{}v1.[1]  \mcdot{}  as  =0)
\mvdash{}  (\muparrow{}isl(gcd-reduce-eq-constraints([[0]  /  sat];v1)))
\mwedge{}  (\mforall{}as\mmember{}outl(gcd-reduce-eq-constraints([[0]  /  sat];v1)).[1]  \mcdot{}  as  =0)


By

---

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

---

Home Index