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

Definition df-csh 12760
Description: Perform a cyclical shift for an arbitrary class. Meaningful only for words 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
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-csh
StepHypRef Expression
1 ccsh 12759 . 2
2 vw . . 3
3 vn . . 3
4 vf . . . . . . 7
54cv 1394 . . . . . 6
6 cc0 9513 . . . . . . 7
7 vl . . . . . . . 8
87cv 1394 . . . . . . 7
9 cfzo 11824 . . . . . . 7
106, 8, 9co 6296 . . . . . 6
115, 10wfn 5588 . . . . 5
12 cn0 10820 . . . . 5
1311, 7, 12wrex 2808 . . . 4
1413, 4cab 2442 . . 3
15 cz 10889 . . 3
162cv 1394 . . . . 5
17 c0 3784 . . . . 5
1816, 17wceq 1395 . . . 4
193cv 1394 . . . . . . . 8
20 chash 12405 . . . . . . . . 9
2116, 20cfv 5593 . . . . . . . 8
22 cmo 11996 . . . . . . . 8
2319, 21, 22co 6296 . . . . . . 7
2423, 21cop 4035 . . . . . 6
25 csubstr 12538 . . . . . 6
2616, 24, 25co 6296 . . . . 5
276, 23cop 4035 . . . . . 6
2816, 27, 25co 6296 . . . . 5
29 cconcat 12536 . . . . 5
3026, 28, 29co 6296 . . . 4
3118, 17, 30cif 3941 . . 3
322, 3, 14, 15, 31cmpt2 6298 . 2
331, 32wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  cshfn  12761  cshnz  12763  0csh0  12764
  Copyright terms: Public domain W3C validator