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	swrd0fvlsw 12801	The last symbol in a left-anchored subword. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W substr <. 0 , L >. ) ) = ( W ` ( L - 1 ) ) )
Theorem	swrdeq 12802*	Two subwords of words are equal iff they have the same length and the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018.)
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W substr <. 0 , M >. ) = ( U substr <. 0 , N >. ) <-> ( M = N /\ A. i e. ( 0..^ M ) ( W ` i ) = ( U ` i ) ) ) )
Theorem	swrdlen2 12803	Length of an extracted subword. (Contributed by AV, 5-May-2020.)
|- ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( L - F ) )
Theorem	swrdfv2 12804	A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020.)
|- ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F..^ L ) ) -> ( ( S substr <. F , L >. ) ` ( X - F ) ) = ( S ` X ) )
Theorem	swrdsb0eq 12805	Two subwords with the same bounds are equal if the range is not valid. (Contributed by AV, 4-May-2020.)
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> ( W substr <. M , N >. ) = ( U substr <. M , N >. ) )
Theorem	swrdsbslen 12806	Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020.)
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) )
Theorem	swrdspsleq 12807*	Two words have a common subword (starting at the same position with the same length) iff they have the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Proof shortened by AV, 7-May-2020.)
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> A. i e. ( M..^ N ) ( W ` i ) = ( U ` i ) ) )
Theorem	swrdtrcfvl 12808	The last symbol in a word truncated by one symbol. (Contributed by AV, 16-Jun-2018.) (Proof shortened by Mario Carneiro/AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W substr <. 0 , ( ( # ` W ) - 1 ) >. ) ) = ( W ` ( ( # ` W ) - 2 ) ) )
Theorem	swrds1 12809	Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( ( W e. Word A /\ I e. ( 0..^ ( # ` W ) ) ) -> ( W substr <. I , ( I + 1 ) >. ) = <" ( W ` I ) "> )
Theorem	swrdlsw 12810	Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` W ) "> )
Theorem	2swrdeqwrdeq 12811	Two words are equal if and only if they have the same prefix and the same suffix. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
|- ( ( W e. Word V /\ S e. Word V /\ I e. ( 0..^ ( # ` W ) ) ) -> ( W = S <-> ( ( # ` W ) = ( # ` S ) /\ ( ( W substr <. 0 , I >. ) = ( S substr <. 0 , I >. ) /\ ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) ) ) ) )
Theorem	2swrd1eqwrdeq 12812	Two (nonempty) words are equal if and only if they have the same prefix and the same single symbol suffix. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Revised by Mario Carneiro/AV, 23-Oct-2018.)
|- ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W substr <. 0 , ( ( # ` W ) - 1 ) >. ) = ( U substr <. 0 , ( ( # ` W ) - 1 ) >. ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
Theorem	disjxwrd 12813*	Sets of words are disjoint if each set contains extensions of distinct words of a fixed length. (Contributed by AV, 29-Jul-2018.) (Proof shortened by AV, 7-May-2020.)
|- Disj y e. W { x e. Word V | ( x substr <. 0 , N >. ) = y }
Theorem	ccatswrd 12814	Joining two adjacent subwords makes a longer subword. (Contributed by Stefan O'Rear, 20-Aug-2015.)
|- ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) = ( S substr <. X , Z >. ) )
Theorem	swrdccat1 12815	Recover the left half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) substr <. 0 , ( # ` S ) >. ) = S )
Theorem	swrdccat2 12816	Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) = T )
5.7.7  Subwords of subwords
Theorem	swrdswrdlem 12817	Lemma for swrdswrd 12818. (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 e. Word V /\ ( M + K ) e. ( 0 ... ( M + L ) ) /\ ( M + L ) e. ( 0 ... ( # ` W ) ) ) )
Theorem	swrdswrd 12818	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 12819	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 12820	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 12821	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 12822	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 12823	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 12824	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 12825	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 12826	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 12827	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 12828	An opth 4695-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 12829	An opth 4695-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 12830	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 12831	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 12832	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 12826 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 12833	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 12834	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 12835*	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 12836*	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 12837*	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 12838*	Lemma for reuccats1 12839. (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 12839*	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 12840	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 12841	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 12842	Lemma 1 for swrdccatin12 12849. (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 12843	Lemma 1 for swrdccatin12lem2 12847. (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 12844	Lemma 2 for swrdccatin12lem2 12847. (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 12845	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 12846	Lemma for swrdccatin12lem2 12847 and swrdccatin12lem3 12848. (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 12847	Lemma 2 for swrdccatin12 12849. (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 12848	Lemma 3 for swrdccatin12 12849. (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 12849	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 12850	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 12851	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 12852	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 12853	Lemma for swrdccat3b 12854. (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 12854	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 12855	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 12856	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 12857	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 12858	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 12859	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 12860	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 12861	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 12862	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 12863	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 12864	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 12865	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 12866	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 12867*	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 12868	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 12869	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 12870	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 12871	The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- (reverse ` (/) ) = (/)
Theorem	revs1 12872	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 12873	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 12874	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 12875*	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 12876	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 12877	Construct a function mapping a half-open range of nonnegative integers to a constant, see also fconstmpt 4897. (Contributed by AV, 4-Nov-2018.)
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( ( 0..^ N ) X. { S } ) )
Theorem	repsf 12878	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 12879	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 12880	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 12881	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 12882	The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018.)
|- ( S e. V -> ( S repeatS 0 ) = (/) )
Theorem	repsdf2 12883*	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 12884*	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 12885*	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 12886	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 12887	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 12888	The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018.)
|- ( S e. V -> ( S repeatS 1 ) = <" S "> )
Theorem	repswswrd 12889	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 12890	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 12891	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 12893. The main theorems in this section are about counting the number of different necklaces resulting from cyclically shifting a given word, see cshwrepswhash1 15072 for words consisting of identical symbols and cshwshash 15074 for words having lengths which are prime numbers.
Syntax	ccsh 12892	Extend class notation with Cyclical Shifts.
class cyclShift
Definition	df-csh 12893*	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 12894*	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 12895	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 12896	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 12897	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 12898	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 12899	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 12900	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 ) ) ) )