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

.....aux..... 
1. RngSig
2. 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. (|K| × S) List
8. ↓bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
9. u1 0 ∈ |K|
⊢ ↓bfs-equiv(K;S;[];[<u1, u2>])
BY
(D THEN Symmetry THEN Auto) }

1
.....assertion..... 
1. RngSig
2. 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. (|K| × S) List
8. ↓bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
9. u1 0 ∈ |K|
⊢ bfs-equiv(K;S;[<u1, u2>];[])


Latex:


Latex:
.....aux..... 
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{}  \mdownarrow{}bfs-equiv(K;S;[];[<u1,  u2>])


By


Latex:
(D  0  THEN  Symmetry  THEN  Auto)




Home Index