P. 135 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13401-13500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ccatw2s1cl 13401	The concatenation of a word with two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V )
Theorem	ccatw2s1len 13402	The length of the concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` W ) + 2 ) )
Theorem	ccats1val1 13403	Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
|- ( ( W e. Word V /\ S e. V /\ I e. ( 0..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) )
Theorem	ccats1val2 13404	Value of the symbol concatenated with a word. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Proof shortened by Alexander van der Vekens, 14-Oct-2018.)
|- ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( ( W ++ <" S "> ) ` I ) = S )
Theorem	ccat2s1p1 13405	Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = X )
Theorem	ccat2s1p2 13406	Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = Y )
Theorem	ccatw2s1ass 13407	Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
Theorem	ccatws1lenrevOLD 13408	Obsolete theorem as of 24-Jun-2022. Use wrdlenccats1lenm1 13399 instead. The length of a word concatenated with a singleton word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( W e. Word V /\ X e. V ) -> ( ( # ` ( W ++ <" X "> ) ) = N -> ( # ` W ) = ( N - 1 ) ) )
Theorem	ccatws1n0 13409	The concatenation of a word with a singleton word is not the empty set. (Contributed by Alexander van der Vekens, 29-Sep-2018.)
|- ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) =/= (/) )
Theorem	ccatws1ls 13410	The last symbol of the concatenation of a word with a singleton word is the symbol of the singleton word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ X e. V ) -> ( ( W ++ <" X "> ) ` ( # ` W ) ) = X )
Theorem	lswccats1 13411	The last symbol of a word concatenated with a singleton word is the symbol of the singleton word. (Contributed by AV, 6-Aug-2018.) (Proof shortened by AV, 22-Oct-2018.)
|- ( ( W e. Word V /\ S e. V ) -> ( lastS ` ( W ++ <" S "> ) ) = S )
Theorem	lswccats1fst 13412	The last symbol of a nonempty word concatenated with its first symbol is the first symbol. (Contributed by AV, 28-Jun-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) )
Theorem	ccatw2s1p1 13413	Extract the symbol of the first singleton word of a word concatenated with this singleton word and another singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` N ) = X )
Theorem	ccatw2s1p2 13414	Extract the second of two single symbols concatenated with a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N + 1 ) ) = Y )
Theorem	ccat2s1fvw 13415	Extract a symbol of a word from the concatenation of the word with two single symbols. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 13-Jan-2020.) (Proof shortened by AV, 1-May-2020.)
|- ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )
Theorem	ccat2s1fst 13416	The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( ( W e. Word V /\ 0 < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = ( W ` 0 ) )
5.7.6  Subwords
Theorem	swrdval 13417*	Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) = if ( ( F..^ L ) C_ dom S , ( x e. ( 0..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) )
Theorem	swrd00 13418	A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( S substr <. X , X >. ) = (/)
Theorem	swrdcl 13419	Closure of the subword extractor. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( S e. Word A -> ( S substr <. F , L >. ) e. Word A )
Theorem	swrdval2 13420*	Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 2-May-2020.)
|- ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) = ( x e. ( 0..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) )
Theorem	swrd0val 13421	Value of the subword extractor for left-anchored subwords. (Contributed by Stefan O'Rear, 24-Aug-2015.)
|- ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. 0 , L >. ) = ( S |` ( 0..^ L ) ) )
Theorem	swrd0len 13422	Length of a left-anchored subword. (Contributed by Stefan O'Rear, 24-Aug-2015.)
|- ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. 0 , L >. ) ) = L )
Theorem	swrdlen 13423	Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( L - F ) )
Theorem	swrdfv 13424	A symbol in an extracted subword, indexed using the subword's indices. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- ( ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) /\ X e. ( 0..^ ( L - F ) ) ) -> ( ( S substr <. F , L >. ) ` X ) = ( S ` ( X + F ) ) )
Theorem	swrdf 13425	A subword of a word is a function from a half-open range of nonnegative integers of the same length as the subword to the set of symbols for the original word. (Contributed by AV, 13-Nov-2018.)
|- ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) : ( 0..^ ( N - M ) ) --> V )
Theorem	swrdvalfn 13426	Value of the subword extractor as function with domain. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( ( S e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) Fn ( 0..^ ( L - F ) ) )
Theorem	swrd0f 13427	A left-anchored subword of a word is a function from a half-open range of nonnegative integers of the same length as the subword to the set of symbols for the original word. (Contributed by AV, 2-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. 0 , N >. ) : ( 0..^ N ) --> V )
Theorem	swrdid 13428	A word is a subword of itself. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof shortened by AV, 2-May-2020.)
|- ( S e. Word A -> ( S substr <. 0 , ( # ` S ) >. ) = S )
Theorem	swrdrn 13429	The range of a subword of a word is a subset of the set of symbols for the word. (Contributed by AV, 13-Nov-2018.)
|- ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ V )
Theorem	swrdn0 13430	A prefixing subword consisting of at least one symbol is not empty. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( ( W e. Word V /\ N e. NN /\ N <_ ( # ` W ) ) -> ( W substr <. 0 , N >. ) =/= (/) )
Theorem	swrdlend 13431	The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( L <_ F -> ( W substr <. F , L >. ) = (/) ) )
Theorem	swrdnd 13432	The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( F < 0 \/ L <_ F \/ ( # ` W ) < L ) -> ( W substr <. F , L >. ) = (/) ) )
Theorem	swrdnd2 13433	Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.)
|- ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( ( B <_ A \/ ( # ` W ) <_ A \/ B <_ 0 ) -> ( W substr <. A , B >. ) = (/) ) )
Theorem	swrd0 13434	A subword of an empty set is always the empty set. (Contributed by AV, 31-Mar-2018.) (Revised by AV, 20-Oct-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( (/) substr <. F , L >. ) = (/)
Theorem	swrdrlen 13435	Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.)
|- ( ( W e. Word V /\ I e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. I , ( # ` W ) >. ) ) = ( ( # ` W ) - I ) )
Theorem	swrd0len0 13436	Length of a prefix of a word reduced by a single symbol, analogous to swrd0len 13422. (Contributed by AV, 4-Aug-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( # ` ( W substr <. 0 , N >. ) ) = N )
Theorem	addlenrevswrd 13437	The sum of the lengths of two reversed 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	addlenswrd 13438	The sum of the lengths of two 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	swrd0fv 13439	A symbol in an left-anchored subword, indexed using the subword's indices. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0..^ L ) ) -> ( ( W substr <. 0 , L >. ) ` I ) = ( W ` I ) )
Theorem	swrd0fv0 13440	The first symbol in a left-anchored subword. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
|- ( ( W e. Word V /\ I e. ( 1 ... ( # ` W ) ) ) -> ( ( W substr <. 0 , I >. ) ` 0 ) = ( W ` 0 ) )
Theorem	swrdtrcfv 13441	A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
|- ( ( W e. Word V /\ W =/= (/) /\ I e. ( 0..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W substr <. 0 , ( ( # ` W ) - 1 ) >. ) ` I ) = ( W ` I ) )
Theorem	swrdtrcfv0 13442	The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( W substr <. 0 , ( ( # ` W ) - 1 ) >. ) ` 0 ) = ( W ` 0 ) )
Theorem	swrd0fvlsw 13443	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 13444*	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 13445	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 13446	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 13447	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 13448	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 13449*	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 13450	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 13451	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 13452	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 13453	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 13454	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 13455*	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 13456	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 13457	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 13458	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 13459	Lemma for swrdswrd 13460. (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 13460	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 13461	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 13462	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 13463	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 13464	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 13465	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 13466	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 13467	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 13468	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 13469	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 13470	An opth 4945-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 13471	An opth 4945-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 13472	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 13473	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	wrdeqs1cat 13474	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 13475	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 13476*	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 13477*	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 13478*	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 13479*	Lemma for reuccats1 13480. (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 13480*	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.) (Revised by AV, 21-Jan-2022.)
|- F/_ v X   =>    |- ( ( 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 ) >. ) ) )
Theorem	reuccats1v 13481*	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.) (Proof shortened by AV, 21-Jan-2022.)
|- ( ( 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 13482	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 13483	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 13484	Lemma 1 for swrdccatin12 13491. (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 13485	Lemma 1 for swrdccatin12lem2 13489. (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 13486	Lemma 2 for swrdccatin12lem2 13489. (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 13487	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 13488	Lemma for swrdccatin12lem2 13489 and swrdccatin12lem3 13490. (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 13489	Lemma 2 for swrdccatin12 13491. (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 13490	Lemma 3 for swrdccatin12 13491. (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 13491	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 13492	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 13493	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 13494	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 13495	Lemma for swrdccat3b 13496. (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 13496	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 13497	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 13498	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 13499	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 13500	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 ) >. ) )