---

Step * 2 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. u : |K| × S
6. v : (|K| × S) List
7. ↓bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
⊢ ↓bfs-equiv(K;S;bfs-rm0(K;eq;{u}) + bfs-rm0(K;eq;v);{u} + v)
BY
{ (Assert ↓bfs-equiv(K;S;bfs-rm0(K;eq;{u});{u}) BY
         (DVar `u' THEN RepUR ``bfs-rm0 bag-filter single-bag`` 0 THEN AutoSplit)) }

1
.....aux..... 
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|
⊢ ↓bfs-equiv(K;S;[];[<u1, u2>])

2
1. K : RngSig
2. S : Type
3. eq : EqDecider(|K|)
4. EquivRel(bag(|K| × S);a,b.bfs-equiv(K;S;a;b))
5. u : |K| × S
6. v : (|K| × S) List
7. ↓bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
8. ↓bfs-equiv(K;S;bfs-rm0(K;eq;{u});{u})
⊢ ↓bfs-equiv(K;S;bfs-rm0(K;eq;{u}) + bfs-rm0(K;eq;v);{u} + v)

---

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.  u  :  |K|  \mtimes{}  S
6.  v  :  (|K|  \mtimes{}  S)  List
7.  \mdownarrow{}bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
\mvdash{}  \mdownarrow{}bfs-equiv(K;S;bfs-rm0(K;eq;\{u\})  +  bfs-rm0(K;eq;v);\{u\}  +  v)


By

---

Latex:
(Assert  \mdownarrow{}bfs-equiv(K;S;bfs-rm0(K;eq;\{u\});\{u\})  BY
              (DVar  `u'  THEN  RepUR  ``bfs-rm0  bag-filter  single-bag``  0  THEN  AutoSplit))

---

Home Index