---

Step * 2 1 1 1 1 1 of Lemma bfs-rm0-equiv


1. K : RngSig
2. S : Type
3. eq : EqDecider(|K|)
4. EquivRel(bag(|K| × S);a,b.bfs-equiv(K;S;a;b))
5. u1 : |K|
6. u2 : S
7. v : (|K| × S) List
8. ↓bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
9. u1 = 0 ∈ |K|
⊢ ∃s:bag(S). ([<u1, u2>] = ([] + 0 * s) ∈ basic-formal-sum(K;S))
BY
{ ((Fold `single-bag` 0 THEN Fold `empty-bag` 0) THEN D 0 With ⌜{u2}⌝  THEN Auto) }

1
1. K : RngSig
2. S : Type
3. eq : EqDecider(|K|)
4. EquivRel(bag(|K| × S);a,b.bfs-equiv(K;S;a;b))
5. u1 : |K|
6. u2 : S
7. v : (|K| × S) List
8. bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
9. u1 = 0 ∈ |K|
⊢ {<u1, u2>} = ({} + 0 * {u2}) ∈ basic-formal-sum(K;S)

---

Latex:

---

Latex:

1.  K  :  RngSig
2.  S  :  Type
3.  eq  :  EqDecider(|K|)
4.  EquivRel(bag(|K|  \mtimes{}  S);a,b.bfs-equiv(K;S;a;b))
5.  u1  :  |K|
6.  u2  :  S
7.  v  :  (|K|  \mtimes{}  S)  List
8.  \mdownarrow{}bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
9.  u1  =  0
\mvdash{}  \mexists{}s:bag(S).  ([<u1,  u2>]  =  ([]  +  0  *  s))


By

---

Latex:
((Fold  `single-bag`  0  THEN  Fold  `empty-bag`  0)  THEN  D  0  With  \mkleeneopen{}\{u2\}\mkleeneclose{}    THEN  Auto)

---

Home Index