Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-csh Structured version   Unicode version

Definition df-csh 12710
 Description: Perform a cyclical shift for an arbitrary class. Meaningful only for words Word or at least functions over half-open ranges of nonnegative integers. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by Mario Carneiro/Alexander van der Vekens/ Gerard Lang, 17-Nov-2018.)
Assertion
Ref Expression
df-csh cyclShift ..^ substr concat substr
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-csh
StepHypRef Expression
1 ccsh 12709 . 2 cyclShift
2 vw . . 3
3 vn . . 3
4 vf . . . . . . 7
54cv 1373 . . . . . 6
6 cc0 9481 . . . . . . 7
7 vl . . . . . . . 8
87cv 1373 . . . . . . 7
9 cfzo 11781 . . . . . . 7 ..^
106, 8, 9co 6275 . . . . . 6 ..^
115, 10wfn 5574 . . . . 5 ..^
12 cn0 10784 . . . . 5
1311, 7, 12wrex 2808 . . . 4 ..^
1413, 4cab 2445 . . 3 ..^
15 cz 10853 . . 3
162cv 1373 . . . . 5
17 c0 3778 . . . . 5
1816, 17wceq 1374 . . . 4
193cv 1373 . . . . . . . 8
20 chash 12360 . . . . . . . . 9
2116, 20cfv 5579 . . . . . . . 8
22 cmo 11952 . . . . . . . 8
2319, 21, 22co 6275 . . . . . . 7
2423, 21cop 4026 . . . . . 6
25 csubstr 12491 . . . . . 6 substr
2616, 24, 25co 6275 . . . . 5 substr
276, 23cop 4026 . . . . . 6
2816, 27, 25co 6275 . . . . 5 substr
29 cconcat 12489 . . . . 5 concat
3026, 28, 29co 6275 . . . 4 substr concat substr
3118, 17, 30cif 3932 . . 3 substr concat substr
322, 3, 14, 15, 31cmpt2 6277 . 2 ..^ substr concat substr
331, 32wceq 1374 1 cyclShift ..^ substr concat substr
 Colors of variables: wff setvar class This definition is referenced by:  cshfn  12711  cshnz  12713  0csh0  12714
 Copyright terms: Public domain W3C validator