Step
*
1
1
1
1
1
of Lemma
perm_assoc
1. T : Type
2. p : Perm(T)
3. q : Perm(T)
4. r : Perm(T)
5. p
O q
O r ∈ Perm(T)
6. InvFuns(T;T;p
O q
O r.f;p
O q
O r.b)
7. p
O q
O r ∈ Perm(T)
8. InvFuns(T;T;p
O q
O r.f;p
O q
O r.b)
⊢ mk_perm(p.f o (q.f o r.f);(r.b o q.b) o p.b) = mk_perm((p.f o q.f) o r.f;r.b o (q.b o p.b)) ∈ perm_sig(T)
BY
{ (RW CompIdNormC 0 THEN Auto) }
Latex:
Latex:
1. T : Type
2. p : Perm(T)
3. q : Perm(T)
4. r : Perm(T)
5. p
O q
O r \mmember{} Perm(T)
6. InvFuns(T;T;p
O q
O r.f;p
O q
O r.b)
7. p
O q
O r \mmember{} Perm(T)
8. InvFuns(T;T;p
O q
O r.f;p
O q
O r.b)
\mvdash{} mk\_perm(p.f o (q.f o r.f);(r.b o q.b) o p.b) = mk\_perm((p.f o q.f) o r.f;r.b o (q.b o p.b))
By
Latex:
(RW CompIdNormC 0 THEN Auto)
Home
Index