---

Step * 1 of Lemma formal-sum-mul-add


1. S : Type
2. K : CRng
3. k : |K|
4. b : |K|
5. fs : basic-formal-sum(K;S)
⊢ bfs-reduce(K;S;k +K b * fs;k * fs + b * fs)
BY
{ (OrRight THEN Auto THEN InstConcl [⌜{}⌝;⌜k⌝;⌜b⌝;⌜fs⌝]⋅ THEN Auto) }

1
.....wf..... 
1. S : Type
2. K : CRng
3. k : |K|
4. b : |K|
5. fs : basic-formal-sum(K;S)
⊢ {} ∈ basic-formal-sum(K;S)

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  k  :  |K|
4.  b  :  |K|
5.  fs  :  basic-formal-sum(K;S)
\mvdash{}  bfs-reduce(K;S;k  +K  b  *  fs;k  *  fs  +  b  *  fs)


By

---

Latex:
(OrRight  THEN  Auto  THEN  InstConcl  [\mkleeneopen{}\{\}\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}fs\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index