Description: Define a convenience permutation cycle builder. Given a list of elements to be cycled, in the form of a word, this function produces the corresponding permutation cycle. See definition in Lang p. 30. (Contributed by Thierry Arnoux, 19-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | df-tocyc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ctocyc | |
|
1 | vd | |
|
2 | cvv | |
|
3 | vw | |
|
4 | vu | |
|
5 | 1 | cv | |
6 | 5 | cword | |
7 | 4 | cv | |
8 | 7 | cdm | |
9 | 8 5 7 | wf1 | |
10 | 9 4 6 | crab | |
11 | cid | |
|
12 | 3 | cv | |
13 | 12 | crn | |
14 | 5 13 | cdif | |
15 | 11 14 | cres | |
16 | ccsh | |
|
17 | c1 | |
|
18 | 12 17 16 | co | |
19 | 12 | ccnv | |
20 | 18 19 | ccom | |
21 | 15 20 | cun | |
22 | 3 10 21 | cmpt | |
23 | 1 2 22 | cmpt | |
24 | 0 23 | wceq | |