P. 113 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11201-11300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pfxval 11201	Value of a prefix operation. (Contributed by AV, 2-May-2020.)
|- ( ( S e. V /\ L e. NN0 ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )
Theorem	pfx00g 11202	The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.)
|- ( S e. V -> ( S prefix 0 ) = (/) )
Theorem	pfx0g 11203	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
|- ( L e. NN0 -> ( (/) prefix L ) = (/) )
Theorem	fnpfx 11204	The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
|- prefix Fn ( _V X. NN0 )
Theorem	pfxclg 11205	Closure of the prefix extractor. (Contributed by AV, 2-May-2020.)
|- ( ( S e. Word A /\ L e. NN0 ) -> ( S prefix L ) e. Word A )
Theorem	pfxclz 11206	Closure of the prefix extractor. This extends pfxclg 11205 from NN0 to ZZ (negative lengths are trivial, resulting in the empty word). (Contributed by Jim Kingdon, 8-Jan-2026.)
|- ( ( S e. Word A /\ L e. ZZ ) -> ( S prefix L ) e. Word A )
Theorem	pfxmpt 11207*	Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020.)
|- ( ( S e. Word A /\ L e. ( 0 ... (♯ ` S ) ) ) -> ( S prefix L ) = ( x e. ( 0..^ L ) |-> ( S ` x ) ) )
Theorem	pfxres 11208	Value of the prefix extractor as the restriction of a word. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.)
|- ( ( S e. Word A /\ L e. ( 0 ... (♯ ` S ) ) ) -> ( S prefix L ) = ( S |` ( 0..^ L ) ) )
Theorem	pfxf 11209	A prefix of a word is a function from a half-open range of nonnegative integers of the same length as the prefix to the set of symbols for the original word. (Contributed by AV, 2-May-2020.)
|- ( ( W e. Word V /\ L e. ( 0 ... (♯ ` W ) ) ) -> ( W prefix L ) : ( 0..^ L ) --> V )
Theorem	pfxfn 11210	Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.)
|- ( ( S e. Word V /\ L e. ( 0 ... (♯ ` S ) ) ) -> ( S prefix L ) Fn ( 0..^ L ) )
Theorem	pfxfv 11211	A symbol in a prefix of a word, indexed using the prefix' indices. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. ( 0 ... (♯ ` W ) ) /\ I e. ( 0..^ L ) ) -> ( ( W prefix L ) ` I ) = ( W ` I ) )
Theorem	pfxlen 11212	Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.)
|- ( ( S e. Word A /\ L e. ( 0 ... (♯ ` S ) ) ) -> (♯ ` ( S prefix L ) ) = L )
Theorem	pfxid 11213	A word is a prefix of itself. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by AV, 2-May-2020.)
|- ( S e. Word A -> ( S prefix (♯ ` S ) ) = S )
Theorem	pfxrn 11214	The range of a prefix of a word is a subset of the set of symbols for the word. (Contributed by AV, 2-May-2020.)
|- ( ( W e. Word V /\ L e. ( 0 ... (♯ ` W ) ) ) -> ran ( W prefix L ) C_ V )
Theorem	pfxn0 11215	A prefix consisting of at least one symbol is not empty. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 2-May-2020.)
|- ( ( W e. Word V /\ L e. NN /\ L <_ (♯ ` W ) ) -> ( W prefix L ) =/= (/) )
Theorem	pfxnd 11216	The value of a prefix operation for a length argument larger than the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfvg 5657). (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. NN0 /\ (♯ ` W ) < L ) -> ( W prefix L ) = (/) )
Theorem	pfxwrdsymbg 11217	A prefix of a word is a word over the symbols it consists of. (Contributed by AV, 3-Dec-2022.)
|- ( ( S e. Word A /\ L e. NN0 ) -> ( S prefix L ) e. Word ( S " ( 0..^ L ) ) )
Theorem	addlenpfx 11218	The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 21-Oct-2018.) (Revised by AV, 3-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... (♯ ` W ) ) ) -> ( (♯ ` ( W prefix M ) ) + (♯ ` ( W substr <. M , (♯ ` W ) >. ) ) ) = (♯ ` W ) )
Theorem	pfxfv0 11219	The first symbol of a prefix is the first symbol of the word. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. ( 1 ... (♯ ` W ) ) ) -> ( ( W prefix L ) ` 0 ) = ( W ` 0 ) )
Theorem	pfxtrcfv 11220	A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) /\ I e. ( 0..^ ( (♯ ` W ) - 1 ) ) ) -> ( ( W prefix ( (♯ ` W ) - 1 ) ) ` I ) = ( W ` I ) )
Theorem	pfxtrcfv0 11221	The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.)
|- ( ( W e. Word V /\ 2 <_ (♯ ` W ) ) -> ( ( W prefix ( (♯ ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )
Theorem	pfxfvlsw 11222	The last symbol in a nonempty prefix of a word. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. ( 1 ... (♯ ` W ) ) ) -> (lastS ` ( W prefix L ) ) = ( W ` ( L - 1 ) ) )
Theorem	pfxeq 11223*	The prefixes of two 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.) (Revised by AV, 4-May-2020.)
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( M <_ (♯ ` W ) /\ N <_ (♯ ` U ) ) ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( M = N /\ A. i e. ( 0..^ M ) ( W ` i ) = ( U ` i ) ) ) )
Theorem	pfxtrcfvl 11224	The last symbol in a word truncated by one symbol. (Contributed by AV, 16-Jun-2018.) (Revised by AV, 5-May-2020.)
|- ( ( W e. Word V /\ 2 <_ (♯ ` W ) ) -> (lastS ` ( W prefix ( (♯ ` W ) - 1 ) ) ) = ( W ` ( (♯ ` W ) - 2 ) ) )
Theorem	pfxsuffeqwrdeq 11225	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.) (Revised by AV, 5-May-2020.)
|- ( ( W e. Word V /\ S e. Word V /\ I e. ( 0..^ (♯ ` W ) ) ) -> ( W = S <-> ( (♯ ` W ) = (♯ ` S ) /\ ( ( W prefix I ) = ( S prefix I ) /\ ( W substr <. I , (♯ ` W ) >. ) = ( S substr <. I , (♯ ` W ) >. ) ) ) ) )
Theorem	pfxsuff1eqwrdeq 11226	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 AV, 6-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ 0 < (♯ ` W ) ) -> ( W = U <-> ( (♯ ` W ) = (♯ ` U ) /\ ( ( W prefix ( (♯ ` W ) - 1 ) ) = ( U prefix ( (♯ ` W ) - 1 ) ) /\ (lastS ` W ) = (lastS ` U ) ) ) ) )
Theorem	disjwrdpfx 11227*	Sets of words are disjoint if each set contains exactly the extensions of distinct words of a fixed length. Remark: A word W is called an "extension" of a word P if P is a prefix of W. (Contributed by AV, 29-Jul-2018.) (Revised by AV, 6-May-2020.)
|- Disj y e. W { x e. Word V | ( x prefix N ) = y }
Theorem	ccatpfx 11228	Concatenating a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020.)
|- ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... (♯ ` S ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) = ( S prefix Z ) )
Theorem	pfxccat1 11229	Recover the left half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by AV, 6-May-2020.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) prefix (♯ ` S ) ) = S )
Theorem	pfx1 11230	The prefix of length one of a nonempty word expressed as a singleton word. (Contributed by AV, 15-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W prefix 1 ) = <" ( W ` 0 ) "> )
4.7.8  Subwords of subwords
Theorem	swrdswrdlem 11231	Lemma for swrdswrd 11232. (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 11232	A subword of a subword is 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	pfxswrd 11233	A prefix of a subword is a subword. (Contributed by AV, 2-Apr-2018.) (Revised by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... (♯ ` W ) ) /\ M e. ( 0 ... N ) ) -> ( L e. ( 0 ... ( N - M ) ) -> ( ( W substr <. M , N >. ) prefix L ) = ( W substr <. M , ( M + L ) >. ) ) )
Theorem	swrdpfx 11234	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 11235	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 11236	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 11237	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 11238	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 11239	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 11240	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 11241	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 11242*	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 11243	An opth 4322-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 11244	An opth 4322-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 11245	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 11246	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 11247	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 11248	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 11249*	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 11250*	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 11251	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 11252	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 11253	Lemma 4 for pfxccatin12 11260. (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 11254	Lemma for pfxccatin12lem2 11258. (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 11255	Lemma 1 for pfxccatin12 11260. (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 11256	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 11257	Lemma for pfxccatin12lem2 11258 and pfxccatin12lem3 11259. (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 11258	Lemma 2 for pfxccatin12 11260. (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 11259	Lemma 3 for pfxccatin12 11260. (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 11260	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 11261	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 11262	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 11263	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 11264	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 11265	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 11266	Lemma for swrdccat3b 11267. (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 11267	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 11268	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 11269	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 11270	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 11271	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 11272	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 11273*	Lemma for reuccatpfxs1 11274. (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 11274*	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 11275*	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 11276	Syntax for the length 2 word constructor.
class <" A B ">
Syntax	cs3 11277	Syntax for the length 3 word constructor.
class <" A B C ">
Syntax	cs4 11278	Syntax for the length 4 word constructor.
class <" A B C D ">
Syntax	cs5 11279	Syntax for the length 5 word constructor.
class <" A B C D E ">
Syntax	cs6 11280	Syntax for the length 6 word constructor.
class <" A B C D E F ">
Syntax	cs7 11281	Syntax for the length 7 word constructor.
class <" A B C D E F G ">
Syntax	cs8 11282	Syntax for the length 8 word constructor.
class <" A B C D E F G H ">
Definition	df-s2 11283	Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B "> = ( <" A "> ++ <" B "> )
Definition	df-s3 11284	Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C "> = ( <" A B "> ++ <" C "> )
Definition	df-s4 11285	Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
Definition	df-s5 11286	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 11287	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 11288	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 11289	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 11290	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 11291	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 11292	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 11293	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 11294	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 11295	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 11296	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 11297	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 11298	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 11299	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 11300	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 "> )