P. 112 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11101-11200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	len0nnbi 11101	The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.)
|- ( W e. Word S -> ( W =/= (/) <-> (♯ ` W ) e. NN ) )
Theorem	wrdlenge2n0 11102	A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ 2 <_ (♯ ` W ) ) -> W =/= (/) )
Theorem	wrdsymb1 11103	The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
|- ( ( W e. Word V /\ 1 <_ (♯ ` W ) ) -> ( W ` 0 ) e. V )
Theorem	wrdlen1 11104*	A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018.) (Proof shortened by AV, 19-Oct-2018.)
|- ( ( W e. Word V /\ (♯ ` W ) = 1 ) -> E. v e. V ( W ` 0 ) = v )
Theorem	fstwrdne 11105	The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W ` 0 ) e. V )
Theorem	fstwrdne0 11106	The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( N e. NN /\ ( W e. Word V /\ (♯ ` W ) = N ) ) -> ( W ` 0 ) e. V )
Theorem	eqwrd 11107*	Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) (Revised by JJ, 30-Dec-2023.)
|- ( ( U e. Word S /\ W e. Word T ) -> ( U = W <-> ( (♯ ` U ) = (♯ ` W ) /\ A. i e. ( 0..^ (♯ ` U ) ) ( U ` i ) = ( W ` i ) ) ) )
Theorem	elovmpowrd 11108*	Implications for the value of an operation defined by the maps-to notation with a class abstraction of words as a result having an element. Note that ph may depend on z as well as on v and y. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- O = ( v e. _V , y e. _V |-> { z e. Word v | ph } )   =>    |- ( Z e. ( V O Y ) -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) )
Theorem	wrdred1 11109	A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)
|- ( F e. Word S -> ( F |` ( 0..^ ( (♯ ` F ) - 1 ) ) ) e. Word S )
Theorem	wrdred1hash 11110	The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
|- ( ( F e. Word S /\ 1 <_ (♯ ` F ) ) -> (♯ ` ( F |` ( 0..^ ( (♯ ` F ) - 1 ) ) ) ) = ( (♯ ` F ) - 1 ) )
4.7.2  Last symbol of a word
Syntax	clsw 11111	Extend class notation with the Last Symbol of a word.
class lastS
Definition	df-lsw 11112	Extract the last symbol of a word. May be not meaningful for other sets which are not words. The name lastS (as abbreviation of "lastSymbol") is a compromise between usually used names for corresponding functions in computer programs (as last() or lastChar()), the terminology used for words in set.mm ("symbol" instead of "character") and brevity ("lastS" is shorter than "lastChar" and "lastSymbol"). Labels of theorems about last symbols of a word will contain the abbreviation "lsw" (Last Symbol of a Word). (Contributed by Alexander van der Vekens, 18-Mar-2018.)
|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
Theorem	lswwrd 11113	Extract the last symbol of a word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Jim Kingdon, 18-Dec-2025.)
|- ( W e. Word V -> (lastS ` W ) = ( W ` ( (♯ ` W ) - 1 ) ) )
Theorem	lsw0 11114	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 19-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( ( W e. Word V /\ (♯ ` W ) = 0 ) -> (lastS ` W ) = (/) )
Theorem	lsw0g 11115	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)
|- (lastS ` (/) ) = (/)
Theorem	lsw1 11116	The last symbol of a word of length 1 is the first symbol of this word. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
|- ( ( W e. Word V /\ (♯ ` W ) = 1 ) -> (lastS ` W ) = ( W ` 0 ) )
Theorem	lswcl 11117	Closure of the last symbol: the last symbol of a nonempty word belongs to the alphabet for the word. (Contributed by AV, 2-Aug-2018.) (Proof shortened by AV, 29-Apr-2020.)
|- ( ( W e. Word V /\ W =/= (/) ) -> (lastS ` W ) e. V )
Theorem	lswex 11118	Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11115 or lswcl 11117 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 11119	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 11120	Syntax for the concatenation operator.
class ++
Definition	df-concat 11121*	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 11122*	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 11123	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 11124	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 11125	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 11126	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 11127	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 11128	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 11129	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 11130	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 11131	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 11132	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 11133	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 11134	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 11135	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 11136	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 11137	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 11138	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 11139	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 11140	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
|- ( (/) ++ (/) ) = (/)
Theorem	lswccatn0lsw 11141	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 11142	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 ) )
4.7.4  Singleton words
Syntax	cs1 11143	Syntax for the singleton word constructor.
class <" A ">
Definition	df-s1 11144	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 11151, 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 11145	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 11146	The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- ( A e. V -> ran <" A "> = { A } )
Theorem	s1eq 11147	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( A = B -> <" A "> = <" B "> )
Theorem	s1eqd 11148	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> <" A "> = <" B "> )
Theorem	s1cl 11149	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 11150	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. B )   =>    |- ( ph -> <" A "> e. Word B )
Theorem	s1prc 11151	Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)
|- ( -. A e. _V -> <" A "> = <" (/) "> )
Theorem	s1leng 11152	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 11153	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
|- ( A e. S -> dom <" A "> = { 0 } )
Theorem	s1fv 11154	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 11155	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
|- ( A e. V -> (lastS ` <" A "> ) = A )
Theorem	eqs1 11156	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 11157*	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 11158	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 11159	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 11160	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 11161	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 11162	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 11163	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	ccatw2s1cl 11164	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	ccats1val1g 11165	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 11166	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 11167	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 11168	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 11169	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 11170	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	ccatw2s1p2 11171	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 )
4.7.6  Subwords/substrings
Syntax	csubstr 11172	Syntax for the subword operator.
class substr
Definition	df-substr 11173*	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 11174	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 11175*	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 11176	A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( ( S e. V /\ X e. ZZ ) -> ( S substr <. X , X >. ) = (/) )
Theorem	swrdclg 11177	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 11178*	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 11179	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 11180	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 11181	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 11182	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 11183	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 11184	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 11185	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 11186	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 11187	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 11188	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 11189	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 11190	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 11191	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 11192	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 11193	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 11194*	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 11195	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 11196	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 11197	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 11198	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 11199	Syntax for the prefix operator.
class prefix
Definition	df-pfx 11200*	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 >. ) )