Step
*
2
1
1
1
of Lemma
bfs-rm0-equiv
.....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>])
BY
{ (D 0 THEN Symmetry THEN Auto) }
1
.....assertion.....
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>];[])
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