Definition df-csh

Description: Perform a cyclical shift for an arbitrary class. Meaningful only for words w e. Word S 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) (Revised by AV, 4-Nov-2022)

	Ref	Expression
Assertion	df-csh	|- cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsh	|- cyclShift
1		vw	|- w
2		vf	|- f
3		vl	|- l
4		cn0	|- NN0
5	2	cv	|- f
6		cc0	|- 0
7		cfzo	|- ..^
8	3	cv	|- l
9	6 8 7	co	|- ( 0 ..^ l )
10	5 9	wfn	|- f Fn ( 0 ..^ l )
11	10 3 4	wrex	|- E. l e. NN0 f Fn ( 0 ..^ l )
12	11 2	cab	|- { f | E. l e. NN0 f Fn ( 0 ..^ l ) }
13		vn	|- n
14		cz	|- ZZ
15	1	cv	|- w
16		c0	|- (/)
17	15 16	wceq	|- w = (/)
18		csubstr	|- substr
19	13	cv	|- n
20		cmo	|- mod
21		chash	|- #
22	15 21	cfv	|- ( # ` w )
23	19 22 20	co	|- ( n mod ( # ` w ) )
24	23 22	cop	|- <. ( n mod ( # ` w ) ) , ( # ` w ) >.
25	15 24 18	co	|- ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. )
26		cconcat	|- ++
27		cpfx	|- prefix
28	15 23 27	co	|- ( w prefix ( n mod ( # ` w ) ) )
29	25 28 26	co	|- ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) )
30	17 16 29	cif	|- if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) )
31	1 13 12 14 30	cmpo	|- ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )
32	0 31	wceq	|- cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )