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	swrdfv0 11201	The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022.)
|- ( ( S e. Word A /\ F e. ( 0..^ L ) /\ L e. ( 0 ... (♯ ` S ) ) ) -> ( ( S substr <. F , L >. ) ` 0 ) = ( S ` F ) )
Theorem	swrdf 11202	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 11203	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	swrdrn 11204	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	swrdlend 11205	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 11206	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	swrd0g 11207	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.)
|- ( ( F e. ZZ /\ L e. ZZ ) -> ( (/) substr <. F , L >. ) = (/) )
Theorem	swrdrlen 11208	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	swrdlen2 11209	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 11210	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	swrdwrdsymbg 11211	A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022.)
|- ( ( S e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... (♯ ` S ) ) ) -> ( S substr <. M , N >. ) e. Word ( S " ( M..^ N ) ) )
Theorem	swrdsb0eq 11212	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 11213	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 11214*	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	swrds1 11215	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 11216	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	ccatswrd 11217	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	swrdccat2 11218	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 )
4.7.7  Prefixes of a word
Syntax	cpfx 11219	Syntax for the prefix operator.
class prefix
Definition	df-pfx 11220*	Define an operation which extracts prefixes of words, i.e. subwords (or substrings) starting at the beginning of a word (or string). In other words, ( S prefix L ) is the prefix of the word S of length L. Definition in Section 9.1 of [AhoHopUll] p. 318. See also Wikipedia "Substring" https://en.wikipedia.org/wiki/Substring#Prefix. (Contributed by AV, 2-May-2020.)
|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
Theorem	pfxval 11221	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 11222	The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.)
|- ( S e. V -> ( S prefix 0 ) = (/) )
Theorem	pfx0g 11223	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
|- ( L e. NN0 -> ( (/) prefix L ) = (/) )
Theorem	fnpfx 11224	The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
|- prefix Fn ( _V X. NN0 )
Theorem	pfxclg 11225	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 11226	Closure of the prefix extractor. This extends pfxclg 11225 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 11227*	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 11228	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 11229	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 11230	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 11231	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 11232	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 11233	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 11234	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 11235	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 11236	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 5660). (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. NN0 /\ (♯ ` W ) < L ) -> ( W prefix L ) = (/) )
Theorem	pfxwrdsymbg 11237	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 11238	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 11239	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 11240	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 11241	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 11242	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 11243*	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 11244	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 11245	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 11246	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 11247*	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 11248	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 11249	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 11250	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 11251	Lemma for swrdswrd 11252. (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 11252	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 11253	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 11254	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 11255	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 11256	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 11257	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 11258	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 11259	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 11260	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 11261	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 11262*	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 11263	An opth 4323-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 11264	An opth 4323-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 11265	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 11266	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 11267	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 11268	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 11269*	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 11270*	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 11271	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 11272	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 11273	Lemma 4 for pfxccatin12 11280. (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 11274	Lemma for pfxccatin12lem2 11278. (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 11275	Lemma 1 for pfxccatin12 11280. (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 11276	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 11277	Lemma for pfxccatin12lem2 11278 and pfxccatin12lem3 11279. (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 11278	Lemma 2 for pfxccatin12 11280. (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 11279	Lemma 3 for pfxccatin12 11280. (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 11280	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 11281	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 11282	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 11283	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 11284	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 11285	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 11286	Lemma for swrdccat3b 11287. (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 11287	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 11288	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 11289	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 11290	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 11291	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 11292	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 11293*	Lemma for reuccatpfxs1 11294. (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 11294*	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 11295*	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 11296	Syntax for the length 2 word constructor.
class <" A B ">
Syntax	cs3 11297	Syntax for the length 3 word constructor.
class <" A B C ">
Syntax	cs4 11298	Syntax for the length 4 word constructor.
class <" A B C D ">
Syntax	cs5 11299	Syntax for the length 5 word constructor.
class <" A B C D E ">
Syntax	cs6 11300	Syntax for the length 6 word constructor.
class <" A B C D E F ">