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	$$⊢\mathrm{cyclShift}=\left(w\in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\},n\in \mathbb{Z}⟼if\left(w=\varnothing ,\varnothing ,\left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)\mathrm{++}\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsh	$$class\mathrm{cyclShift}$$
1		vw	$$setvarw$$
2		vf	$$setvarf$$
3		vl	$$setvarl$$
4		cn0	$$class{\mathbb{N}}_0$$
5	2	cv	$$setvarf$$
6		cc0	$$class0$$
7		cfzo	$$class..^$$
8	3	cv	$$setvarl$$
9	6 8 7	co	$$class\left(0..^l\right)$$
10	5 9	wfn	$$wfffFn\left(0..^l\right)$$
11	10 3 4	wrex	$$wff\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)$$
12	11 2	cab	$$class\left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\}$$
13		vn	$$setvarn$$
14		cz	$$class\mathbb{Z}$$
15	1	cv	$$setvarw$$
16		c0	$$class\varnothing$$
17	15 16	wceq	$$wffw=\varnothing$$
18		csubstr	$$class\mathrm{substr}$$
19	13	cv	$$setvarn$$
20		cmo	$$class\mathrm{mod}$$
21		chash	$$class\left|.\right|$$
22	15 21	cfv	$$class\left|w\right|$$
23	19 22 20	co	$$class\left(n\mathrm{mod}\left|w\right|\right)$$
24	23 22	cop	$$class⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩$$
25	15 24 18	co	$$class\left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)$$
26		cconcat	$$class\mathrm{++}$$
27		cpfx	$$class\mathrm{prefix}$$
28	15 23 27	co	$$class\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)$$
29	25 28 26	co	$$class\left(\left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)\mathrm{++}\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)\right)$$
30	17 16 29	cif	$$classif\left(w=\varnothing ,\varnothing ,\left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)\mathrm{++}\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)\right)$$
31	1 13 12 14 30	cmpo	$$class\left(w\in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\},n\in \mathbb{Z}⟼if\left(w=\varnothing ,\varnothing ,\left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)\mathrm{++}\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)\right)\right)$$
32	0 31	wceq	$$wff\mathrm{cyclShift}=\left(w\in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\},n\in \mathbb{Z}⟼if\left(w=\varnothing ,\varnothing ,\left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)\mathrm{++}\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)\right)\right)$$