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	s1leng 11101	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 11102	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
|- ( A e. S -> dom <" A "> = { 0 } )
Theorem	s1fv 11103	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 11104	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
|- ( A e. V -> (lastS ` <" A "> ) = A )
Theorem	eqs1 11105	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 11106*	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 11107	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 11108	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 11109	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 11110	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 11111	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 11112	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 11113	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 11114	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 11115	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 11116	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 11117	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 11118	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 11119	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 11120	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 11121	Syntax for the subword operator.
class substr
Definition	df-substr 11122*	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 11123	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 11124*	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 11125	A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( ( S e. V /\ X e. ZZ ) -> ( S substr <. X , X >. ) = (/) )
Theorem	swrdclg 11126	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 11127*	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 11128	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 11129	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 11130	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 11131	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 11132	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 11133	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 11134	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 11135	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 11136	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 11137	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 11138	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 11139	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 11140	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 11141	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 11142	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 11143*	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 11144	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 11145	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 11146	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 11147	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 11148	Syntax for the prefix operator.
class prefix
Definition	df-pfx 11149*	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 11150	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 11151	The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.)
|- ( S e. V -> ( S prefix 0 ) = (/) )
Theorem	pfx0g 11152	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
|- ( L e. NN0 -> ( (/) prefix L ) = (/) )
Theorem	fnpfx 11153	The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
|- prefix Fn ( _V X. NN0 )
Theorem	pfxclg 11154	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 11155	Closure of the prefix extractor. This extends pfxclg 11154 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 11156*	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 11157	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 11158	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 11159	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 11160	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 11161	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 11162	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 11163	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 11164	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 11165	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 5620). (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. NN0 /\ (♯ ` W ) < L ) -> ( W prefix L ) = (/) )
Theorem	pfxwrdsymbg 11166	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 11167	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 11168	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 11169	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 11170	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 11171	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 11172*	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 11173	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 11174	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 11175	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 11176*	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 11177	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 11178	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 11179	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 11180	Lemma for swrdswrd 11181. (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 11181	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 11182	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 11183	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 11184	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 11185	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 11186	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 11187	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 11188	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 11189	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 11190	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 11191*	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 11192	An opth 4289-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 11193	An opth 4289-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 11194	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 11195	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 11196	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 11197	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 11198*	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 11199*	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.8  Elementary real and complex functions
4.8.1  The "shift" operation
Syntax	cshi 11200	Extend class notation with function shifter.
class shift