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	wrdlndm 11101	The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021.) (Proof shortened by JJ, 18-Nov-2022.)
|- ( W e. Word V -> (♯ ` W ) e/ dom W )
Theorem	iswrdsymb 11102*	An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021.)
|- ( ( W e. Word _V /\ A. i e. ( 0..^ (♯ ` W ) ) ( W ` i ) e. V ) -> W e. Word V )
Theorem	wrdfin 11103	A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015.) (Proof shortened by AV, 18-Nov-2018.)
|- ( W e. Word S -> W e. Fin )
Theorem	lennncl 11104	The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ( ( W e. Word S /\ W =/= (/) ) -> (♯ ` W ) e. NN )
Theorem	wrdffz 11105	A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.)
|- ( W e. Word S -> W : ( 0 ... ( (♯ ` W ) - 1 ) ) --> S )
Theorem	wrdeq 11106	Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( S = T -> Word S = Word T )
Theorem	wrdeqi 11107	Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.)
|- S = T   =>    |- Word S = Word T
Theorem	iswrddm0 11108	A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.)
|- ( W : (/) --> S -> W e. Word S )
Theorem	wrd0 11109	The empty set is a word (the empty word, frequently denoted ε in this context). This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 13-May-2020.)
|- (/) e. Word S
Theorem	0wrd0 11110	The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)
|- ( W e. Word (/) <-> W = (/) )
Theorem	ffz0iswrdnn0 11111	A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.) (Proof shortened by JJ, 18-Nov-2022.)
|- ( ( W : ( 0 ... L ) --> S /\ L e. NN0 ) -> W e. Word S )
Theorem	wrdsymb 11112	A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.)
|- ( S e. Word A -> S e. Word ( S " ( 0..^ (♯ ` S ) ) ) )
Theorem	nfwrd 11113	Hypothesis builder for Word S. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- F/_ x S   =>    |- F/_ xWord S
Theorem	csbwrdg 11114*	Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- ( S e. V -> [_ S / x ]_Word x = Word S )
Theorem	wrdnval 11115*	Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Proof shortened by AV, 13-May-2020.)
|- ( ( V e. X /\ N e. NN0 ) -> { w e. Word V | (♯ ` w ) = N } = ( V ^m ( 0..^ N ) ) )
Theorem	wrdmap 11116	Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- ( ( V e. X /\ N e. NN0 ) -> ( ( W e. Word V /\ (♯ ` W ) = N ) <-> W e. ( V ^m ( 0..^ N ) ) ) )
Theorem	wrdsymb0 11117	A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( ( W e. Word V /\ I e. ZZ ) -> ( ( I < 0 \/ (♯ ` W ) <_ I ) -> ( W ` I ) = (/) ) )
Theorem	wrdlenge1n0 11118	A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)
|- ( W e. Word V -> ( W =/= (/) <-> 1 <_ (♯ ` W ) ) )
Theorem	len0nnbi 11119	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 11120	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 11121	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 11122*	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 11123	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 11124	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 11125*	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 11126*	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 11127	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 11128	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 11129	Extend class notation with the Last Symbol of a word.
class lastS
Definition	df-lsw 11130	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 11131	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 11132	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 11133	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)
|- (lastS ` (/) ) = (/)
Theorem	lsw1 11134	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 11135	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 11136	Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11133 or lswcl 11135 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 11137	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 11138	Syntax for the concatenation operator.
class ++
Definition	df-concat 11139*	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 11140*	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 11141	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 11142	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 11143	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 11144	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 11145	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 11146	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 11147	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 11148	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 11149	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 11150	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 11151	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 11152	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 11153	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 11154	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 11155	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 11156	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 11157	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 11158	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
|- ( (/) ++ (/) ) = (/)
Theorem	lswccatn0lsw 11159	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 11160	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 11161	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 11162	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 11163	Syntax for the singleton word constructor.
class <" A ">
Definition	df-s1 11164	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 11171, 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 11165	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 11166	The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- ( A e. V -> ran <" A "> = { A } )
Theorem	s1eq 11167	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( A = B -> <" A "> = <" B "> )
Theorem	s1eqd 11168	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> <" A "> = <" B "> )
Theorem	s1cl 11169	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 11170	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. B )   =>    |- ( ph -> <" A "> e. Word B )
Theorem	s1prc 11171	Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)
|- ( -. A e. _V -> <" A "> = <" (/) "> )
Theorem	s1leng 11172	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 11173	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
|- ( A e. S -> dom <" A "> = { 0 } )
Theorem	s1fv 11174	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 11175	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
|- ( A e. V -> (lastS ` <" A "> ) = A )
Theorem	eqs1 11176	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 11177*	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 11178	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 11179	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 11180	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 11181	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 11182	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 11183	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 11184	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 11185	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 11186	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 11187	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 11188	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 11189	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 11190	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 11191	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 11192	Syntax for the subword operator.
class substr
Definition	df-substr 11193*	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 11194	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 11195*	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 11196	A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( ( S e. V /\ X e. ZZ ) -> ( S substr <. X , X >. ) = (/) )
Theorem	swrdclg 11197	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 11198*	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 11199	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 11200	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 ) ) )