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	s1val 11301	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 11302	The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- ( A e. V -> ran <" A "> = { A } )
Theorem	s1eq 11303	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( A = B -> <" A "> = <" B "> )
Theorem	s1eqd 11304	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> <" A "> = <" B "> )
Theorem	s1cl 11305	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 11306	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. B )   =>    |- ( ph -> <" A "> e. Word B )
Theorem	s1prc 11307	Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)
|- ( -. A e. _V -> <" A "> = <" (/) "> )
Theorem	s1leng 11308	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 11309	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
|- ( A e. S -> dom <" A "> = { 0 } )
Theorem	s1fv 11310	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 11311	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
|- ( A e. V -> (lastS ` <" A "> ) = A )
Theorem	eqs1 11312	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 11313*	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 11314	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 11315	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 11316	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 11317	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 11318	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 11319	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 11320	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 11321	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 11322	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 11323	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 11324	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 11325	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 11326	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 11327	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 11328	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 11329	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 11330	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 11331	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 11332	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 11333	Syntax for the subword operator.
class substr
Definition	df-substr 11334*	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 11335	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 11336*	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 11337	A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( ( S e. V /\ X e. ZZ ) -> ( S substr <. X , X >. ) = (/) )
Theorem	swrdclg 11338	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 11339*	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 11340	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 11341	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 11342	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 11343	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 11344	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 11345	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 11346	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 11347	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 11348	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 11349	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 11350	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 11351	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 11352	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 11353	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 11354	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 11355*	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 11356	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 11357	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 11358	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 11359	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 11360	Syntax for the prefix operator.
class prefix
Definition	df-pfx 11361*	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 11362	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 11363	The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.)
|- ( S e. V -> ( S prefix 0 ) = (/) )
Theorem	pfx0g 11364	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
|- ( L e. NN0 -> ( (/) prefix L ) = (/) )
Theorem	fnpfx 11365	The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
|- prefix Fn ( _V X. NN0 )
Theorem	pfxclg 11366	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 11367	Closure of the prefix extractor. This extends pfxclg 11366 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 11368*	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 11369	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 11370	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 11371	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 11372	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 11373	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 11374	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 11375	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 11376	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 11377	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 5700). (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. NN0 /\ (♯ ` W ) < L ) -> ( W prefix L ) = (/) )
Theorem	pfxwrdsymbg 11378	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 11379	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 11380	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 11381	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 11382	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 11383	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 11384*	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 11385	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 11386	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 11387	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 11388*	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 11389	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 11390	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 11391	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 11392	Lemma for swrdswrd 11393. (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 11393	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 11394	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 11395	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 11396	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 11397	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 11398	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 11399	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 11400	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 ) )