P. 129 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	swrdswrd 12801	A subword of a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( ( W substr <. M , N >. ) substr <. K , L >. ) = ( W substr <. ( M + K ) , ( M + L ) >. ) ) )
Theorem	swrd0swrd 12802	A prefix of a subword. (Contributed by AV, 2-Apr-2018.) (Proof shortened by AV, 21-Oct-2018.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( L e. ( 0 ... ( N - M ) ) -> ( ( W substr <. M , N >. ) substr <. 0 , L >. ) = ( W substr <. M , ( M + L ) >. ) ) )
Theorem	swrdswrd0 12803	A subword of a prefix. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) -> ( ( W substr <. 0 , N >. ) substr <. K , L >. ) = ( W substr <. K , L >. ) ) )
Theorem	swrd0swrd0 12804	A prefix of a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( ( W substr <. 0 , N >. ) substr <. 0 , L >. ) = ( W substr <. 0 , L >. ) )
Theorem	swrd0swrdid 12805	A prefix of a prefix with the same length is the prefix. (Contributed by AV, 5-Apr-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( W substr <. 0 , N >. ) substr <. 0 , N >. ) = ( W substr <. 0 , N >. ) )
5.7.8  Subwords and concatenations
Theorem	wrdcctswrd 12806	The concatenation of two parts of a word yields the word itself. (Contributed by AV, 21-Oct-2018.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( W substr <. 0 , M >. ) ++ ( W substr <. M , ( # ` W ) >. ) ) = W )
Theorem	lencctswrd 12807	The length of two concatenated parts of a word is the length of the word. (Contributed by AV, 21-Oct-2018.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W substr <. 0 , M >. ) ++ ( W substr <. M , ( # ` W ) >. ) ) ) = ( # ` W ) )
Theorem	lenrevcctswrd 12808	The length of two reversely concatenated parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W substr <. M , ( # ` W ) >. ) ++ ( W substr <. 0 , M >. ) ) ) = ( # ` W ) )
Theorem	swrdccatwrd 12809	Reconstruct a nonempty word from its prefix and last symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( ( W substr <. 0 , ( ( # ` W ) - 1 ) >. ) ++ <" ( lastS ` W ) "> ) = W )
Theorem	ccats1swrdeq 12810	The last symbol of a word concatenated with the subword of the word having length less by 1 than the word results in the word itself. (Contributed by Alexander van der Vekens, 24-Oct-2018.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U substr <. 0 , ( # ` W ) >. ) -> U = ( W ++ <" ( lastS ` U ) "> ) ) )
Theorem	ccatopth 12811	An opth 4696-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) -> ( ( A ++ B ) = ( C ++ D ) <-> ( A = C /\ B = D ) ) )
Theorem	ccatopth2 12812	An opth 4696-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( A ++ B ) = ( C ++ D ) <-> ( A = C /\ B = D ) ) )
Theorem	ccatlcan 12813	Concatenation of words is left-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( ( A e. Word X /\ B e. Word X /\ C e. Word X ) -> ( ( C ++ A ) = ( C ++ B ) <-> A = B ) )
Theorem	ccatrcan 12814	Concatenation of words is right-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( ( A e. Word X /\ B e. Word X /\ C e. Word X ) -> ( ( A ++ C ) = ( B ++ C ) <-> A = B ) )
Theorem	wrdeqcats1OLD 12815	Decompose a nonempty word by separating off the last symbol. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 26-Apr-2020.) Obsolete version of swrdccatwrd 12809 as of 9-May-2020. (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( W e. Word A /\ W =/= (/) ) -> W = ( ( W substr <. 0 , ( ( # ` W ) - 1 ) >. ) ++ <" ( W ` ( ( # ` W ) - 1 ) ) "> ) )
Theorem	wrdeqs1cat 12816	Decompose a nonempty word by separating off the first symbol. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 9-May-2020.)
|- ( ( W e. Word A /\ W =/= (/) ) -> W = ( <" ( W ` 0 ) "> ++ ( W substr <. 1 , ( # ` W ) >. ) ) )
Theorem	cats1un 12817	Express a word with an extra symbol as the union of the word and the new value. (Contributed by Mario Carneiro, 28-Feb-2016.)
|- ( ( A e. Word X /\ B e. X ) -> ( A ++ <" B "> ) = ( A u. { <. ( # ` A ) , B >. } ) )
Theorem	wrdind 12818*	Perform induction over the structure of a word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( x = (/) -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y ++ <" z "> ) -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( ( y e. Word B /\ z e. B ) -> ( ch -> th ) )   =>    |- ( A e. Word B -> ta )
Theorem	wrd2ind 12819*	Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019.)
|- ( ( x = (/) /\ w = (/) ) -> ( ph <-> ps ) )   &    |- ( ( x = y /\ w = u ) -> ( ph <-> ch ) )   &    |- ( ( x = ( y ++ <" z "> ) /\ w = ( u ++ <" s "> ) ) -> ( ph <-> th ) )   &    |- ( x = A -> ( rh <-> ta ) )   &    |- ( w = B -> ( ph <-> rh ) )   &    |- ps   &    |- ( ( ( y e. Word X /\ z e. X ) /\ ( u e. Word Y /\ s e. Y ) /\ ( # ` y ) = ( # ` u ) ) -> ( ch -> th ) )   =>    |- ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ta )
Theorem	ccats1swrdeqrex 12820*	There exists a symbol such that its concatenation with the subword obtained by deleting the last symbol of a nonempty word results in the word itself. (Contributed by AV, 5-Oct-2018.) (Proof shortened by AV, 24-Oct-2018.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U substr <. 0 , ( # ` W ) >. ) -> E. s e. V U = ( W ++ <" s "> ) ) )
Theorem	reuccats1lem 12821*	Lemma for reuccats1 12822. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Proof shortened by AV, 15-Jan-2020.)
|- ( ( ( W e. Word V /\ U e. X /\ ( W ++ <" S "> ) e. X ) /\ ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) ) -> ( W = ( U substr <. 0 , ( # ` W ) >. ) -> U = ( W ++ <" S "> ) ) )
Theorem	reuccats1 12822*	A set of words having the length of a given word increased by 1 contains a unique word with the given word as prefix if there is a unique symbol which extends the given word to be a word of the set. (Contributed by Alexander van der Vekens, 6-Oct-2018.)
|- ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x substr <. 0 , ( # ` W ) >. ) ) )
5.7.9  Subwords of concatenations
Theorem	swrdccatfn 12823	The subword of a concatenation as function. (Contributed by Alexander van der Vekens, 27-May-2018.)
|- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0..^ ( N - M ) ) )
Theorem	swrdccatin1 12824	The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
|- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )
Theorem	swrdccatin12lem1 12825	Lemma 1 for swrdccatin12 12832. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.)
|- ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> K e. ( ( L - M )..^ ( ( L - M ) + ( N - L ) ) ) ) )
Theorem	swrdccatin12lem2a 12826	Lemma 1 for swrdccatin12lem2 12830. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( K + M ) e. ( L..^ X ) ) )
Theorem	swrdccatin12lem2b 12827	Lemma 2 for swrdccatin12lem2 12830. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( K - ( L - M ) ) e. ( 0..^ ( ( N - L ) - 0 ) ) ) )
Theorem	swrdccatin2 12828	The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) ) )
Theorem	swrdccatin12lem2c 12829	Lemma for swrdccatin12lem2 12830 and swrdccatin12lem3 12831. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
|- L = ( # ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
Theorem	swrdccatin12lem2 12830	Lemma 2 for swrdccatin12 12832. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
|- L = ( # ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( B substr <. 0 , ( N - L ) >. ) ` ( K - ( # ` ( A substr <. M , L >. ) ) ) ) ) )
Theorem	swrdccatin12lem3 12831	Lemma 3 for swrdccatin12 12832. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
|- L = ( # ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ K e. ( 0..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A substr <. M , L >. ) ` K ) ) )
Theorem	swrdccatin12 12832	The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B substr <. 0 , ( N - L ) >. ) ) ) )
Theorem	swrdccat3 12833	The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 28-May-2018.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B substr <. 0 , ( N - L ) >. ) ) ) ) ) )
Theorem	swrdccat 12834	The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) ) )
Theorem	swrdccat3a 12835	A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 29-May-2018.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + ( # ` B ) ) ) -> ( ( A ++ B ) substr <. 0 , N >. ) = if ( N <_ L , ( A substr <. 0 , N >. ) , ( A ++ ( B substr <. 0 , ( N - L ) >. ) ) ) ) )
Theorem	swrdccat3blem 12836	Lemma for swrdccat3b 12837. (Contributed by AV, 30-May-2018.)
|- L = ( # ` A )   =>    |- ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ ( L + ( # ` B ) ) <_ L ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) )
Theorem	swrdccat3b 12837	A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 30-May-2018.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> ( ( A ++ B ) substr <. M , ( L + ( # ` B ) ) >. ) = if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) ) )
Theorem	swrdccatid 12838	A prefix of a concatenation of length of the first concatenated word is the first word itself. (Contributed by Alexander van der Vekens, 20-Sep-2018.)
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( ( A ++ B ) substr <. 0 , N >. ) = A )
Theorem	ccats1swrdeqbi 12839	A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. (Contributed by AV, 24-Oct-2018.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U substr <. 0 , ( # ` W ) >. ) <-> U = ( W ++ <" ( lastS ` U ) "> ) ) )
Theorem	swrdccatin1d 12840	The subword of a concatenation of two words within the first of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.)
|- ( ph -> ( # ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( 0 ... N ) )   &    |- ( ph -> N e. ( 0 ... L ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) )
Theorem	swrdccatin2d 12841	The subword of a concatenation of two words within the second of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.)
|- ( ph -> ( # ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( L ... N ) )   &    |- ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
Theorem	swrdccatin12d 12842	The subword of a concatenation of two words within both of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.)
|- ( ph -> ( # ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( 0 ... L ) )   &    |- ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B substr <. 0 , ( N - L ) >. ) ) )
5.7.10  Splicing words (substring replacement)
Theorem	splval 12843	Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> ( S splice <. F , T , R >. ) = ( ( ( S substr <. 0 , F >. ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
Theorem	splcl 12844	Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- ( ( S e. Word A /\ R e. Word A ) -> ( S splice <. F , T , R >. ) e. Word A )
Theorem	splid 12845	Splicing a subword for the same subword makes no difference. (Contributed by Stefan O'Rear, 20-Aug-2015.)
|- ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( S splice <. X , Y , ( S substr <. X , Y >. ) >. ) = S )
Theorem	spllen 12846	The length of a splice. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( ph -> S e. Word A )   &    |- ( ph -> F e. ( 0 ... T ) )   &    |- ( ph -> T e. ( 0 ... ( # ` S ) ) )   &    |- ( ph -> R e. Word A )   =>    |- ( ph -> ( # ` ( S splice <. F , T , R >. ) ) = ( ( # ` S ) + ( ( # ` R ) - ( T - F ) ) ) )
Theorem	splfv1 12847	Symbols to the left of a splice are unaffected. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( ph -> S e. Word A )   &    |- ( ph -> F e. ( 0 ... T ) )   &    |- ( ph -> T e. ( 0 ... ( # ` S ) ) )   &    |- ( ph -> R e. Word A )   &    |- ( ph -> X e. ( 0..^ F ) )   =>    |- ( ph -> ( ( S splice <. F , T , R >. ) ` X ) = ( S ` X ) )
Theorem	splfv2a 12848	Symbols within the replacement region of a splice, expressed using the coordinates of the replacement region. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( ph -> S e. Word A )   &    |- ( ph -> F e. ( 0 ... T ) )   &    |- ( ph -> T e. ( 0 ... ( # ` S ) ) )   &    |- ( ph -> R e. Word A )   &    |- ( ph -> X e. ( 0..^ ( # ` R ) ) )   =>    |- ( ph -> ( ( S splice <. F , T , R >. ) ` ( F + X ) ) = ( R ` X ) )
Theorem	splval2 12849	Value of a splice, assuming the input word S has already been decomposed into its pieces. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ( ph -> A e. Word X )   &    |- ( ph -> B e. Word X )   &    |- ( ph -> C e. Word X )   &    |- ( ph -> R e. Word X )   &    |- ( ph -> S = ( ( A ++ B ) ++ C ) )   &    |- ( ph -> F = ( # ` A ) )   &    |- ( ph -> T = ( F + ( # ` B ) ) )   =>    |- ( ph -> ( S splice <. F , T , R >. ) = ( ( A ++ R ) ++ C ) )
5.7.11  Reversing words
Theorem	revval 12850*	Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- ( W e. V -> (reverse ` W ) = ( x e. ( 0..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )
Theorem	revcl 12851	The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- ( W e. Word A -> (reverse ` W ) e. Word A )
Theorem	revlen 12852	The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- ( W e. Word A -> ( # ` (reverse ` W ) ) = ( # ` W ) )
Theorem	revfv 12853	Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- ( ( W e. Word A /\ X e. ( 0..^ ( # ` W ) ) ) -> ( (reverse ` W ) ` X ) = ( W ` ( ( ( # ` W ) - 1 ) - X ) ) )
Theorem	rev0 12854	The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- (reverse ` (/) ) = (/)
Theorem	revs1 12855	Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- (reverse ` <" S "> ) = <" S ">
Theorem	revccat 12856	Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( ( S e. Word A /\ T e. Word A ) -> (reverse ` ( S ++ T ) ) = ( (reverse ` T ) ++ (reverse ` S ) ) )
Theorem	revrev 12857	Reversion is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ( W e. Word A -> (reverse ` (reverse ` W ) ) = W )
5.7.12  Repeated symbol words
Theorem	reps 12858*	Construct a function mapping a half-open range of nonnegative integers to a constant. (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( x e. ( 0..^ N ) |-> S ) )
Theorem	repsundef 12859	A function mapping a half-open range of nonnegative integers with an upper bound not being a nonnegative integer to a constant is the empty set (in the meaning of "undefined"). (Contributed by AV, 5-Nov-2018.)
|- ( N e/ NN0 -> ( S repeatS N ) = (/) )
Theorem	repsconst 12860	Construct a function mapping a half-open range of nonnegative integers to a constant, see also fconstmpt 4898. (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( ( 0..^ N ) X. { S } ) )
Theorem	repsf 12861	The constructed function mapping a half-open range of nonnegative integers to a constant is a function. (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) : ( 0..^ N ) --> V )
Theorem	repswsymb 12862	The symbols of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 /\ I e. ( 0..^ N ) ) -> ( ( S repeatS N ) ` I ) = S )
Theorem	repsw 12863	A function mapping a half-open range of nonnegative integers to a constant is a word consisting of one symbol repeated several times ("repeated symbol word"). (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) e. Word V )
Theorem	repswlen 12864	The length of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 ) -> ( # ` ( S repeatS N ) ) = N )
Theorem	repsw0 12865	The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018.)
|- ( S e. V -> ( S repeatS 0 ) = (/) )
Theorem	repsdf2 12866*	Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 ) -> ( W = ( S repeatS N ) <-> ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0..^ N ) ( W ` i ) = S ) ) )
Theorem	repswsymball 12867*	All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018.)
|- ( ( W e. Word V /\ S e. V ) -> ( W = ( S repeatS ( # ` W ) ) -> A. i e. ( 0..^ ( # ` W ) ) ( W ` i ) = S ) )
Theorem	repswsymballbi 12868*	A word is a "repeated symbol word" iff each of its symbols equals the first symbol of the word. (Contributed by AV, 10-Nov-2018.)
|- ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
Theorem	repswfsts 12869	The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN ) -> ( ( S repeatS N ) ` 0 ) = S )
Theorem	repswlsw 12870	The last symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN ) -> ( lastS ` ( S repeatS N ) ) = S )
Theorem	repsw1 12871	The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018.)
|- ( S e. V -> ( S repeatS 1 ) = <" S "> )
Theorem	repswswrd 12872	A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption N <_ L is required, because otherwise ( L < N ): ( ( S repeatS L ) substr <. M , N >. ) = (/), but for M < N ( S repeatS ( N - M ) ) ) =/= (/)! The proof is relatively long because the border cases ( M = N, -. ( M..^ N ) C_ ( 0..^ L ) must have been considered. (Contributed by AV, 6-Nov-2018.)
|- ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( ( S repeatS L ) substr <. M , N >. ) = ( S repeatS ( N - M ) ) )
Theorem	repswccat 12873	The concatenation of two "repeated symbol words" with the same symbol is again a "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( ( S repeatS N ) ++ ( S repeatS M ) ) = ( S repeatS ( N + M ) ) )
Theorem	repswrevw 12874	The reverse of a "repeated symbol word". (Contributed by AV, 6-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 ) -> (reverse ` ( S repeatS N ) ) = ( S repeatS N ) )
5.7.13  Cyclical shifts of words A word/string can be regarded as "necklace" by connecting the two ends of the word/string together (see Wikipedia "Necklace (combinatorics)", https://en.wikipedia.org/wiki/Necklace_(combinatorics)). Two strings are regarded as the same necklace if one string can be rotated/circularly shifted/cyclically shifted to obtain the second string. To cope with words in the sense of necklaces, the rotation/cyclic shift cyclShift is defined as the basic operation, see df-csh 12876. The main theorems in this section are about counting the number of different necklaces resulting from cyclically shifting a given word, see cshwrepswhash1 15027 for words consisting of identical symbols and cshwshash 15029 for words having lengths which are prime numbers.
Syntax	ccsh 12875	Extend class notation with Cyclical Shifts.
class cyclShift
Definition	df-csh 12876*	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.)
|- cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w substr <. 0 , ( n mod ( # ` w ) ) >. ) ) ) )
Theorem	cshfn 12877*	Perform a cyclical shift for a function over a half-open range of nonnegative integers. (Contributed by AV, 20-May-2018.) (Revised by AV, 17-Nov-2018.)
|- ( ( W e. { f | E. l e. NN0 f Fn ( 0..^ l ) } /\ N e. ZZ ) -> ( W cyclShift N ) = if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W substr <. 0 , ( N mod ( # ` W ) ) >. ) ) ) )
Theorem	cshword 12878	Perform a cyclical shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by AV, 17-Nov-2018.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W substr <. 0 , ( N mod ( # ` W ) ) >. ) ) )
Theorem	cshnz 12879	A cyclical shift is the empty set if the number of shifts is not an integer. (Contributed by Alexander van der Vekens, 21-May-2018.) (Revised by AV, 17-Nov-2018.)
|- ( -. N e. ZZ -> ( W cyclShift N ) = (/) )
Theorem	0csh0 12880	Cyclically shifting an empty set/word always results in the empty word/set. (Contributed by AV, 25-Oct-2018.) (Revised by AV, 17-Nov-2018.)
|- ( (/) cyclShift N ) = (/)
Theorem	cshw0 12881	A word cyclically shifted by 0 is the word itself. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 26-Oct-2018.)
|- ( W e. Word V -> ( W cyclShift 0 ) = W )
Theorem	cshwmodn 12882	Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) )
Theorem	cshwsublen 12883	Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N - ( # ` W ) ) ) )
Theorem	cshwn 12884	A word cyclically shifted by its length is the word itself. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 26-Oct-2018.)
|- ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W )
Theorem	cshwcl 12885	A cyclically shifted word is a word over the same set as for the original word. (Contributed by AV, 16-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 27-Oct-2018.)
|- ( W e. Word V -> ( W cyclShift N ) e. Word V )
Theorem	cshwlen 12886	The length of a cyclically shifted word is the same as the length of the original word. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 27-Oct-2018.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
Theorem	cshwf 12887	A cyclically shifted word is a function from a half-open range of integers of the same length as the word as domain to the set of symbols for the word. (Contributed by AV, 12-Nov-2018.)
|- ( ( W e. Word A /\ N e. ZZ ) -> ( W cyclShift N ) : ( 0..^ ( # ` W ) ) --> A )
Theorem	cshwfn 12888	A cyclically shifted word is a function with a half-open range of integers of the same length as the word as domain. (Contributed by AV, 12-Nov-2018.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) Fn ( 0..^ ( # ` W ) ) )
Theorem	cshwrn 12889	The range of a cyclically shifted word is a subset of the set of symbols for the word. (Contributed by AV, 12-Nov-2018.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ran ( W cyclShift N ) C_ V )
Theorem	cshwidxmod 12890	The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 13-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
|- ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )
Theorem	cshwidx0mod 12891	The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N (modulo the length of the word) of the original word. (Contributed by AV, 30-Oct-2018.)
|- ( ( W e. Word V /\ W =/= (/) /\ N e. ZZ ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` ( N mod ( # ` W ) ) ) )
Theorem	cshwidx0 12892	The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N of the original word. (Contributed by AV, 15-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
|- ( ( W e. Word V /\ N e. ( 0..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) )
Theorem	cshwidxm1 12893	The symbol at index ((n-N)-1) of a word of length n (not 0) cyclically shifted by N positions is the symbol at index (n-1) of the original word. (Contributed by AV, 23-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
|- ( ( W e. Word V /\ N e. ( 0..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( ( # ` W ) - N ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
Theorem	cshwidxm 12894	The symbol at index (n-N) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index 0 of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` 0 ) )
Theorem	cshwidxn 12895	The symbol at index (n-1) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index (N-1) of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( N - 1 ) ) )
Theorem	repswcshw 12896	A cyclically shifted "repeated symbol word". (Contributed by Alexander van der Vekens, 7-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) )
Theorem	2cshw 12897	Cyclically shifting a word two times. (Contributed by AV, 7-Apr-2018.) (Revised by AV, 4-Jun-2018.) (Revised by AV, 31-Oct-2018.)
|- ( ( W e. Word V /\ M e. ZZ /\ N e. ZZ ) -> ( ( W cyclShift M ) cyclShift N ) = ( W cyclShift ( M + N ) ) )
Theorem	2cshwid 12898	Cyclically shifting a word two times resulting in the word itself. (Contributed by AV, 7-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( ( W cyclShift N ) cyclShift ( ( # ` W ) - N ) ) = W )
Theorem	lswcshw 12899	The last symbol of a word cyclically shifted by N positions is the symbol at index (N-1) of the original word. (Contributed by AV, 21-Mar-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.)
|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W cyclShift N ) ) = ( W ` ( N - 1 ) ) )
Theorem	2cshwcom 12900	Cyclically shifting a word two times is commutative. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by Mario Carneiro/AV, 1-Nov-2018.)
|- ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( W cyclShift N ) cyclShift M ) = ( ( W cyclShift M ) cyclShift N ) )