P. 116 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11501-11600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	swrdpfx 11501	A subword of a prefix is a subword. (Contributed by Alexander van der Vekens, 6-Apr-2018.) (Revised by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... (♯ ` W ) ) ) -> ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) -> ( ( W prefix N ) substr <. K , L >. ) = ( W substr <. K , L >. ) ) )
Theorem	pfxpfx 11502	A prefix of a prefix is a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... (♯ ` W ) ) /\ L e. ( 0 ... N ) ) -> ( ( W prefix N ) prefix L ) = ( W prefix L ) )
Theorem	pfxpfxid 11503	A prefix of a prefix with the same length is the original prefix. In other words, the operation "prefix of length N " is idempotent. (Contributed by AV, 5-Apr-2018.) (Revised by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... (♯ ` W ) ) ) -> ( ( W prefix N ) prefix N ) = ( W prefix N ) )
4.7.9  Subwords and concatenations
Theorem	pfxcctswrd 11504	The concatenation of the prefix of a word and the rest of the word yields the word itself. (Contributed by AV, 21-Oct-2018.) (Revised by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... (♯ ` W ) ) ) -> ( ( W prefix M ) ++ ( W substr <. M , (♯ ` W ) >. ) ) = W )
Theorem	lenpfxcctswrd 11505	The length of the concatenation of the prefix of a word and the rest of the word is the length of the word. (Contributed by AV, 21-Oct-2018.) (Revised by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... (♯ ` W ) ) ) -> (♯ ` ( ( W prefix M ) ++ ( W substr <. M , (♯ ` W ) >. ) ) ) = (♯ ` W ) )
Theorem	lenrevpfxcctswrd 11506	The length of the concatenation of the rest of a word and the prefix of the word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (Revised by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... (♯ ` W ) ) ) -> (♯ ` ( ( W substr <. M , (♯ ` W ) >. ) ++ ( W prefix M ) ) ) = (♯ ` W ) )
Theorem	pfxlswccat 11507	Reconstruct a nonempty word from its prefix and last symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 9-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( ( W prefix ( (♯ ` W ) - 1 ) ) ++ <" (lastS ` W ) "> ) = W )
Theorem	ccats1pfxeq 11508	The last symbol of a word concatenated with the word with the last symbol removed results in the word itself. (Contributed by Alexander van der Vekens, 24-Oct-2018.) (Revised by AV, 9-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ (♯ ` U ) = ( (♯ ` W ) + 1 ) ) -> ( W = ( U prefix (♯ ` W ) ) -> U = ( W ++ <" (lastS ` U ) "> ) ) )
Theorem	ccats1pfxeqrex 11509*	There exists a symbol such that its concatenation after the prefix obtained by deleting the last symbol of a nonempty word results in the word itself. (Contributed by AV, 5-Oct-2018.) (Revised by AV, 9-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ (♯ ` U ) = ( (♯ ` W ) + 1 ) ) -> ( W = ( U prefix (♯ ` W ) ) -> E. s e. V U = ( W ++ <" s "> ) ) )
Theorem	ccatopth 11510	An opth 4379-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 12-Oct-2022.)
|- ( ( ( 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 11511	An opth 4379-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 11512	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 11513	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 11514	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, 12-Oct-2022.)
|- ( ( W e. Word A /\ W =/= (/) ) -> W = ( <" ( W ` 0 ) "> ++ ( W substr <. 1 , (♯ ` W ) >. ) ) )
Theorem	cats1un 11515	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 11516*	Perform induction over the structure of a word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 12-Oct-2022.)
|- ( 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 11517*	Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019.) (Proof shortened by AV, 12-Oct-2022.)
|- ( ( 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 )
4.7.10  Subwords of concatenations
Theorem	swrdccatfn 11518	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 11519	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	pfxccatin12lem4 11520	Lemma 4 for pfxccatin12 11527. (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	pfxccatin12lem2a 11521	Lemma for pfxccatin12lem2 11525. (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	pfxccatin12lem1 11522	Lemma 1 for pfxccatin12 11527. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.)
|- ( ( 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 ) ) ) )
Theorem	swrdccatin2 11523	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	pfxccatin12lem2c 11524	Lemma for pfxccatin12lem2 11525 and pfxccatin12lem3 11526. (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	pfxccatin12lem2 11525	Lemma 2 for pfxccatin12 11527. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.)
|- 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 prefix ( N - L ) ) ` ( K - (♯ ` ( A substr <. M , L >. ) ) ) ) ) )
Theorem	pfxccatin12lem3 11526	Lemma 3 for pfxccatin12 11527. (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	pfxccatin12 11527	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 AV, 9-May-2020.)
|- 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 prefix ( N - L ) ) ) ) )
Theorem	pfxccat3 11528	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 AV, 10-May-2020.)
|- 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 prefix ( N - L ) ) ) ) ) ) )
Theorem	swrdccat 11529	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	pfxccatpfx1 11530	A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020.)
|- L = (♯ ` A )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )
Theorem	pfxccatpfx2 11531	A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020.)
|- L = (♯ ` A )   &    |- M = (♯ ` B )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )
Theorem	pfxccat3a 11532	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 AV, 10-May-2020.)
|- L = (♯ ` A )   &    |- M = (♯ ` B )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + M ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) ) )
Theorem	swrdccat3blem 11533	Lemma for swrdccat3b 11534. (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 11534	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.) (Proof shortened by AV, 14-Oct-2022.)
|- 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	pfxccatid 11535	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.) (Revised by AV, 10-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ N = (♯ ` A ) ) -> ( ( A ++ B ) prefix N ) = A )
Theorem	ccats1pfxeqbi 11536	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.) (Revised by AV, 10-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ (♯ ` U ) = ( (♯ ` W ) + 1 ) ) -> ( W = ( U prefix (♯ ` W ) ) <-> U = ( W ++ <" (lastS ` U ) "> ) ) )
Theorem	swrdccatin1d 11537	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 11538	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	pfxccatin12d 11539	The subword of a concatenation of two words within both of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by AV, 10-May-2020.)
|- ( 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 prefix ( N - L ) ) ) )
Theorem	reuccatpfxs1lem 11540*	Lemma for reuccatpfxs1 11541. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 9-May-2020.)
|- ( ( ( W e. Word V /\ U 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 prefix (♯ ` W ) ) -> U = ( W ++ <" S "> ) ) )
Theorem	reuccatpfxs1 11541*	There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Revised by AV, 13-Oct-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 prefix (♯ ` W ) ) ) )
Theorem	reuccatpfxs1v 11542*	There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Revised by AV, 10-May-2022.) (Proof shortened by AV, 13-Oct-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 prefix (♯ ` W ) ) ) )
4.7.11  Longer string literals
Syntax	cs2 11543	Syntax for the length 2 word constructor.
class <" A B ">
Syntax	cs3 11544	Syntax for the length 3 word constructor.
class <" A B C ">
Syntax	cs4 11545	Syntax for the length 4 word constructor.
class <" A B C D ">
Syntax	cs5 11546	Syntax for the length 5 word constructor.
class <" A B C D E ">
Syntax	cs6 11547	Syntax for the length 6 word constructor.
class <" A B C D E F ">
Syntax	cs7 11548	Syntax for the length 7 word constructor.
class <" A B C D E F G ">
Syntax	cs8 11549	Syntax for the length 8 word constructor.
class <" A B C D E F G H ">
Definition	df-s2 11550	Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B "> = ( <" A "> ++ <" B "> )
Definition	df-s3 11551	Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C "> = ( <" A B "> ++ <" C "> )
Definition	df-s4 11552	Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
Definition	df-s5 11553	Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
Definition	df-s6 11554	Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
Definition	df-s7 11555	Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
Definition	df-s8 11556	Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
Theorem	cats1cld 11557	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word A )   &    |- ( ph -> X e. A )   =>    |- ( ph -> T e. Word A )
Theorem	cats1fvn 11558	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- S e. Word _V   &    |- (♯ ` S ) = M   =>    |- ( X e. V -> ( T ` M ) = X )
Theorem	cats1fvnd 11559	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. V )   &    |- ( ph -> (♯ ` S ) = M )   =>    |- ( ph -> ( T ` M ) = X )
Theorem	cats1fvd 11560	A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> (♯ ` S ) = M )   &    |- ( ph -> Y e. V )   &    |- ( ph -> X e. W )   &    |- ( ph -> ( S ` N ) = Y )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> N < M )   =>    |- ( ph -> ( T ` N ) = Y )
Theorem	cats1lend 11561	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. W )   &    |- (♯ ` S ) = M   &    |- ( M + 1 ) = N   =>    |- ( ph -> (♯ ` T ) = N )
Theorem	cats1catd 11562	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> A e. Word _V )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. W )   &    |- ( ph -> C = ( B ++ <" X "> ) )   &    |- ( ph -> B = ( A ++ S ) )   =>    |- ( ph -> C = ( A ++ T ) )
Theorem	cats2catd 11563	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- ( ph -> B e. Word _V )   &    |- ( ph -> D e. Word _V )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. W )   &    |- ( ph -> A = ( B ++ <" X "> ) )   &    |- ( ph -> C = ( <" Y "> ++ D ) )   =>    |- ( ph -> ( A ++ C ) = ( ( B ++ <" X Y "> ) ++ D ) )
Theorem	s2eqd 11564	Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   =>    |- ( ph -> <" A B "> = <" N O "> )
Theorem	s3eqd 11565	Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   =>    |- ( ph -> <" A B C "> = <" N O P "> )
Theorem	s4eqd 11566	Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   =>    |- ( ph -> <" A B C D "> = <" N O P Q "> )
Theorem	s5eqd 11567	Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   =>    |- ( ph -> <" A B C D E "> = <" N O P Q R "> )
Theorem	s6eqd 11568	Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   =>    |- ( ph -> <" A B C D E F "> = <" N O P Q R S "> )
Theorem	s7eqd 11569	Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   &    |- ( ph -> G = T )   =>    |- ( ph -> <" A B C D E F G "> = <" N O P Q R S T "> )
Theorem	s8eqd 11570	Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   &    |- ( ph -> G = T )   &    |- ( ph -> H = U )   =>    |- ( ph -> <" A B C D E F G H "> = <" N O P Q R S T U "> )
Theorem	s3eq2 11571	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
|- ( B = D -> <" A B C "> = <" A D C "> )
Theorem	s2cld 11572	A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> <" A B "> e. Word X )
Theorem	s3cld 11573	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   =>    |- ( ph -> <" A B C "> e. Word X )
Theorem	s4cld 11574	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   =>    |- ( ph -> <" A B C D "> e. Word X )
Theorem	s5cld 11575	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   =>    |- ( ph -> <" A B C D E "> e. Word X )
Theorem	s6cld 11576	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   =>    |- ( ph -> <" A B C D E F "> e. Word X )
Theorem	s7cld 11577	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   =>    |- ( ph -> <" A B C D E F G "> e. Word X )
Theorem	s8cld 11578	A length 8 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   &    |- ( ph -> H e. X )   =>    |- ( ph -> <" A B C D E F G H "> e. Word X )
Theorem	s2cl 11579	A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. X /\ B e. X ) -> <" A B "> e. Word X )
Theorem	s3cl 11580	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. X /\ B e. X /\ C e. X ) -> <" A B C "> e. Word X )
Theorem	s2fv0g 11581	Extract the first symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> ( <" A B "> ` 0 ) = A )
Theorem	s2fv1g 11582	Extract the second symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> ( <" A B "> ` 1 ) = B )
Theorem	s2leng 11583	The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> (♯ ` <" A B "> ) = 2 )
Theorem	s2dmg 11584	The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.)
|- ( ( A e. V /\ B e. W ) -> dom <" A B "> = { 0 , 1 } )
Theorem	s3fv0g 11585	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 0 ) = A )
Theorem	s3fv1g 11586	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 1 ) = B )
Theorem	s3fv2g 11587	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 2 ) = C )
Theorem	s1s2d 11588	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   =>    |- ( ph -> <" A B C "> = ( <" A "> ++ <" B C "> ) )
Theorem	s1s3d 11589	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> <" A B C D "> = ( <" A "> ++ <" B C D "> ) )
Theorem	s1s4d 11590	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   =>    |- ( ph -> <" A B C D E "> = ( <" A "> ++ <" B C D E "> ) )
Theorem	s1s5d 11591	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   =>    |- ( ph -> <" A B C D E F "> = ( <" A "> ++ <" B C D E F "> ) )
Theorem	s1s6d 11592	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A "> ++ <" B C D E F G "> ) )
Theorem	s1s7d 11593	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   &    |- ( ph -> H e. R )   =>    |- ( ph -> <" A B C D E F G H "> = ( <" A "> ++ <" B C D E F G H "> ) )
Theorem	s2s2d 11594	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> <" A B C D "> = ( <" A B "> ++ <" C D "> ) )
Theorem	s4s2d 11595	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   =>    |- ( ph -> <" A B C D E F "> = ( <" A B C D "> ++ <" E F "> ) )
Theorem	s4s3d 11596	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> ) )
Theorem	s3s4d 11597	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C "> ++ <" D E F G "> ) )
Theorem	s2s5d 11598	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B "> ++ <" C D E F G "> ) )
Theorem	s5s2d 11599	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C D E "> ++ <" F G "> ) )
Theorem	s4s4d 11600	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   &    |- ( ph -> H e. R )   =>    |- ( ph -> <" A B C D E F G H "> = ( <" A B C D "> ++ <" E F G H "> ) )