P. 114 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11301-11400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lswex 11301	Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11298 or lswcl 11300 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.)
|- ( W e. Word V -> (lastS ` W ) e. _V )
Theorem	lswlgt0cl 11302	The last symbol of a nonempty word is an element of the alphabet for the word. (Contributed by Alexander van der Vekens, 1-Oct-2018.) (Proof shortened by AV, 29-Apr-2020.)
|- ( ( N e. NN /\ ( W e. Word V /\ (♯ ` W ) = N ) ) -> (lastS ` W ) e. V )
4.7.3  Concatenations of words
Syntax	cconcat 11303	Syntax for the concatenation operator.
class ++
Definition	df-concat 11304*	Define the concatenation operator which combines two words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 15-Aug-2015.)
|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
Theorem	ccatfvalfi 11305*	Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Fin /\ T e. Fin ) -> ( S ++ T ) = ( x e. ( 0..^ ( (♯ ` S ) + (♯ ` T ) ) ) |-> if ( x e. ( 0..^ (♯ ` S ) ) , ( S ` x ) , ( T ` ( x - (♯ ` S ) ) ) ) ) )
Theorem	ccatcl 11306	The concatenation of two words is a word. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 29-Apr-2020.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) e. Word B )
Theorem	ccatclab 11307	The concatenation of words over two sets is a word over the union of those sets. (Contributed by Jim Kingdon, 19-Dec-2025.)
|- ( ( S e. Word A /\ T e. Word B ) -> ( S ++ T ) e. Word ( A u. B ) )
Theorem	ccatlen 11308	The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.)
|- ( ( S e. Word A /\ T e. Word B ) -> (♯ ` ( S ++ T ) ) = ( (♯ ` S ) + (♯ ` T ) ) )
Theorem	ccat0 11309	The concatenation of two words is empty iff the two words are empty. (Contributed by AV, 4-Mar-2022.) (Revised by JJ, 18-Jan-2024.)
|- ( ( S e. Word A /\ T e. Word B ) -> ( ( S ++ T ) = (/) <-> ( S = (/) /\ T = (/) ) ) )
Theorem	ccatval1 11310	Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 30-Apr-2020.) (Revised by JJ, 18-Jan-2024.)
|- ( ( S e. Word A /\ T e. Word B /\ I e. ( 0..^ (♯ ` S ) ) ) -> ( ( S ++ T ) ` I ) = ( S ` I ) )
Theorem	ccatval2 11311	Value of a symbol in the right half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( (♯ ` S )..^ ( (♯ ` S ) + (♯ ` T ) ) ) ) -> ( ( S ++ T ) ` I ) = ( T ` ( I - (♯ ` S ) ) ) )
Theorem	ccatval3 11312	Value of a symbol in the right half of a concatenated word, using an index relative to the subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof shortened by AV, 30-Apr-2020.)
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( 0..^ (♯ ` T ) ) ) -> ( ( S ++ T ) ` ( I + (♯ ` S ) ) ) = ( T ` I ) )
Theorem	elfzelfzccat 11313	An element of a finite set of sequential integers up to the length of a word is an element of an extended finite set of sequential integers up to the length of a concatenation of this word with another word. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... (♯ ` A ) ) -> N e. ( 0 ... (♯ ` ( A ++ B ) ) ) ) )
Theorem	ccatvalfn 11314	The concatenation of two words is a function over the half-open integer range having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
|- ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) Fn ( 0..^ ( (♯ ` A ) + (♯ ` B ) ) ) )
Theorem	ccatsymb 11315	The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018.) (Proof shortened by AV, 24-Nov-2018.)
|- ( ( A e. Word V /\ B e. Word V /\ I e. ZZ ) -> ( ( A ++ B ) ` I ) = if ( I < (♯ ` A ) , ( A ` I ) , ( B ` ( I - (♯ ` A ) ) ) ) )
Theorem	ccatfv0 11316	The first symbol of a concatenation of two words is the first symbol of the first word if the first word is not empty. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( A e. Word V /\ B e. Word V /\ 0 < (♯ ` A ) ) -> ( ( A ++ B ) ` 0 ) = ( A ` 0 ) )
Theorem	ccatval1lsw 11317	The last symbol of the left (nonempty) half of a concatenated word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( ( A ++ B ) ` ( (♯ ` A ) - 1 ) ) = (lastS ` A ) )
Theorem	ccatval21sw 11318	The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.)
|- ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( A ++ B ) ` (♯ ` A ) ) = ( B ` 0 ) )
Theorem	ccatlid 11319	Concatenation of a word by the empty word on the left. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
|- ( S e. Word B -> ( (/) ++ S ) = S )
Theorem	ccatrid 11320	Concatenation of a word by the empty word on the right. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
|- ( S e. Word B -> ( S ++ (/) ) = S )
Theorem	ccatass 11321	Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Word B /\ T e. Word B /\ U e. Word B ) -> ( ( S ++ T ) ++ U ) = ( S ++ ( T ++ U ) ) )
Theorem	ccatrn 11322	The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Word B /\ T e. Word B ) -> ran ( S ++ T ) = ( ran S u. ran T ) )
Theorem	ccatidid 11323	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
|- ( (/) ++ (/) ) = (/)
Theorem	lswccatn0lsw 11324	The last symbol of a word concatenated with a nonempty word is the last symbol of the nonempty word. (Contributed by AV, 22-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> (lastS ` ( A ++ B ) ) = (lastS ` B ) )
Theorem	lswccat0lsw 11325	The last symbol of a word concatenated with the empty word is the last symbol of the word. (Contributed by AV, 22-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( W e. Word V -> (lastS ` ( W ++ (/) ) ) = (lastS ` W ) )
Theorem	ccatalpha 11326	A concatenation of two arbitrary words is a word over an alphabet iff the symbols of both words belong to the alphabet. (Contributed by AV, 28-Feb-2021.)
|- ( ( A e. Word _V /\ B e. Word _V ) -> ( ( A ++ B ) e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )
Theorem	ccatrcl1 11327	Reverse closure of a concatenation: If the concatenation of two arbitrary words is a word over an alphabet then the symbols of the first word belong to the alphabet. (Contributed by AV, 3-Mar-2021.)
|- ( ( A e. Word X /\ B e. Word Y /\ ( W = ( A ++ B ) /\ W e. Word S ) ) -> A e. Word S )
4.7.4  Singleton words
Syntax	cs1 11328	Syntax for the singleton word constructor.
class <" A ">
Definition	df-s1 11329	Define the canonical injection from symbols to words. Although not required, A should usually be a set. Otherwise, the singleton word <" A "> would be the singleton word consisting of the empty set, see s1prc 11336, and not, as maybe expected, the empty word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- <" A "> = { <. 0 , ( _I ` A ) >. }
Theorem	s1val 11330	Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( A e. V -> <" A "> = { <. 0 , A >. } )
Theorem	s1rn 11331	The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- ( A e. V -> ran <" A "> = { A } )
Theorem	s1eq 11332	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( A = B -> <" A "> = <" B "> )
Theorem	s1eqd 11333	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> <" A "> = <" B "> )
Theorem	s1cl 11334	A singleton word is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)
|- ( A e. B -> <" A "> e. Word B )
Theorem	s1cld 11335	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. B )   =>    |- ( ph -> <" A "> e. Word B )
Theorem	s1prc 11336	Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)
|- ( -. A e. _V -> <" A "> = <" (/) "> )
Theorem	s1leng 11337	Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( A e. V -> (♯ ` <" A "> ) = 1 )
Theorem	s1dmg 11338	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
|- ( A e. S -> dom <" A "> = { 0 } )
Theorem	s1fv 11339	Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( A e. B -> ( <" A "> ` 0 ) = A )
Theorem	lsws1 11340	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
|- ( A e. V -> (lastS ` <" A "> ) = A )
Theorem	eqs1 11341	A word of length 1 is a singleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
|- ( ( W e. Word A /\ (♯ ` W ) = 1 ) -> W = <" ( W ` 0 ) "> )
Theorem	wrdl1exs1 11342*	A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.)
|- ( ( W e. Word S /\ (♯ ` W ) = 1 ) -> E. s e. S W = <" s "> )
Theorem	wrdl1s1 11343	A word of length 1 is a singleton word consisting of the first symbol of the word. (Contributed by AV, 22-Jul-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( S e. V -> ( W = <" S "> <-> ( W e. Word V /\ (♯ ` W ) = 1 /\ ( W ` 0 ) = S ) ) )
Theorem	s111 11344	The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( S e. A /\ T e. A ) -> ( <" S "> = <" T "> <-> S = T ) )
4.7.5  Concatenations with singleton words
Theorem	ccatws1cl 11345	The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )
Theorem	ccat2s1cl 11346	The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( X e. V /\ Y e. V ) -> ( <" X "> ++ <" Y "> ) e. Word V )
Theorem	ccatws1leng 11347	The length of the concatenation of a word with a singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 4-Mar-2022.)
|- ( ( W e. Word V /\ X e. Y ) -> (♯ ` ( W ++ <" X "> ) ) = ( (♯ ` W ) + 1 ) )
Theorem	ccatws1lenp1bg 11348	The length of a word is N iff the length of the concatenation of the word with a singleton word is N + 1. (Contributed by AV, 4-Mar-2022.)
|- ( ( W e. Word V /\ X e. Y /\ N e. NN0 ) -> ( (♯ ` ( W ++ <" X "> ) ) = ( N + 1 ) <-> (♯ ` W ) = N ) )
Theorem	wrdlenccats1lenm1g 11349	The length of a word is the length of the word concatenated with a singleton word minus 1. (Contributed by AV, 28-Jun-2018.) (Revised by AV, 5-Mar-2022.)
|- ( ( W e. Word V /\ S e. B ) -> ( (♯ ` ( W ++ <" S "> ) ) - 1 ) = (♯ ` W ) )
Theorem	ccatw2s1cl 11350	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	ccatw2s1leng 11351	The length of the concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 5-Mar-2022.)
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> (♯ ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( (♯ ` W ) + 2 ) )
Theorem	ccats1val1g 11352	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.) (Revised by JJ, 20-Jan-2024.)
|- ( ( W e. Word V /\ S e. Y /\ I e. ( 0..^ (♯ ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) )
Theorem	ccats1val2 11353	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	ccat1st1st 11354	The first symbol of a word concatenated with its first symbol is the first symbol of the word. This theorem holds even if W is the empty word. (Contributed by AV, 26-Mar-2022.)
|- ( W e. Word V -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )
Theorem	ccatws1ls 11355	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 11356	The last symbol of a word concatenated with a singleton word is the symbol of the singleton word. (Contributed by AV, 6-Aug-2018.)
|- ( ( W e. Word V /\ S e. V ) -> (lastS ` ( W ++ <" S "> ) ) = S )
Theorem	lswccats1fst 11357	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	ccatw2s1p1g 11358	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.) (Revised by AV, 1-May-2020.) (Revised by AV, 29-Jan-2024.)
|- ( ( ( W e. Word V /\ (♯ ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` N ) = X )
Theorem	ccatw2s1p2 11359	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	ccat2s1fvwd 11360	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.) (Revised by AV, 28-Jan-2024.)
|- ( ph -> W e. Word V )   &    |- ( ph -> I e. NN0 )   &    |- ( ph -> I < (♯ ` W ) )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )
Theorem	ccat2s1fstg 11361	The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 28-Jan-2024.)
|- ( ( ( W e. Word V /\ 0 < (♯ ` W ) ) /\ ( X e. A /\ Y e. B ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = ( W ` 0 ) )
4.7.6  Subwords/substrings
Syntax	csubstr 11362	Syntax for the subword operator.
class substr
Definition	df-substr 11363*	Define an operation which extracts portions (called subwords or substrings) of words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )
Theorem	fzowrddc 11364	Decidability of whether a range of integers is a subset of a word's domain. (Contributed by Jim Kingdon, 23-Dec-2025.)
|- ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) -> DECID ( F..^ L ) C_ dom S )
Theorem	swrdval 11365*	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	swrd00g 11366	A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( ( S e. V /\ X e. ZZ ) -> ( S substr <. X , X >. ) = (/) )
Theorem	swrdclg 11367	Closure of the subword extractor. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) e. Word A )
Theorem	swrdval2 11368*	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	swrdlen 11369	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 11370	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	swrdfv0 11371	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 11372	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 11373	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 11374	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 11375	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 11376	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 11377	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 11378	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 11379	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 11380	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 11381	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 11382	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 11383	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 11384*	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 11385	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 11386	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 11387	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 11388	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 11389	Syntax for the prefix operator.
class prefix
Definition	df-pfx 11390*	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 11391	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 11392	The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.)
|- ( S e. V -> ( S prefix 0 ) = (/) )
Theorem	pfx0g 11393	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
|- ( L e. NN0 -> ( (/) prefix L ) = (/) )
Theorem	fnpfx 11394	The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
|- prefix Fn ( _V X. NN0 )
Theorem	pfxclg 11395	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 11396	Closure of the prefix extractor. This extends pfxclg 11395 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 11397*	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 11398	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 11399	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 11400	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 ) )