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


1. RngSig
2. Type
3. eq EqDecider(|K|)
4. EquivRel(bag(|K| × S);a,b.bfs-equiv(K;S;a;b))
5. |K| × S
6. (|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)
BY
(Fold `formal-sum-add` THEN -2 THEN -1 THEN THEN EAuto 1) }


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


By


Latex:
(Fold  `formal-sum-add`  0  THEN  D  -2  THEN  D  -1  THEN  D  0  THEN  EAuto  1)




Home Index