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

Definition df-csh 12816
 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 ++ substr
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-csh
StepHypRef Expression
1 ccsh 12815 . 2 cyclShift
2 vw . . 3
3 vn . . 3
4 vf . . . . . . 7
54cv 1404 . . . . . 6
6 cc0 9522 . . . . . . 7
7 vl . . . . . . . 8
87cv 1404 . . . . . . 7
9 cfzo 11854 . . . . . . 7 ..^
106, 8, 9co 6278 . . . . . 6 ..^
115, 10wfn 5564 . . . . 5 ..^
12 cn0 10836 . . . . 5
1311, 7, 12wrex 2755 . . . 4 ..^
1413, 4cab 2387 . . 3 ..^
15 cz 10905 . . 3
162cv 1404 . . . . 5
17 c0 3738 . . . . 5
1816, 17wceq 1405 . . . 4
193cv 1404 . . . . . . . 8
20 chash 12452 . . . . . . . . 9
2116, 20cfv 5569 . . . . . . . 8
22 cmo 12034 . . . . . . . 8
2319, 21, 22co 6278 . . . . . . 7
2423, 21cop 3978 . . . . . 6
25 csubstr 12587 . . . . . 6 substr
2616, 24, 25co 6278 . . . . 5 substr
276, 23cop 3978 . . . . . 6
2816, 27, 25co 6278 . . . . 5 substr
29 cconcat 12585 . . . . 5 ++
3026, 28, 29co 6278 . . . 4 substr ++ substr
3118, 17, 30cif 3885 . . 3 substr ++ substr
322, 3, 14, 15, 31cmpt2 6280 . 2 ..^ substr ++ substr
331, 32wceq 1405 1 cyclShift ..^ substr ++ substr
 Colors of variables: wff setvar class This definition is referenced by:  cshfn  12817  cshnz  12819  0csh0  12820
 Copyright terms: Public domain W3C validator