Home | Metamath
Proof Explorer Theorem List (p. 145 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ccatval21sw 14401 | The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β ) β ((π΄ ++ π΅)β(β―βπ΄)) = (π΅β0)) | ||
Theorem | ccatlid 14402 | 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.) |
β’ (π β Word π΅ β (β ++ π) = π) | ||
Theorem | ccatrid 14403 | 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.) |
β’ (π β Word π΅ β (π ++ β ) = π) | ||
Theorem | ccatass 14404 | Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β Word π΅ β§ π β Word π΅ β§ π β Word π΅) β ((π ++ π) ++ π) = (π ++ (π ++ π))) | ||
Theorem | ccatrn 14405 | The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β Word π΅ β§ π β Word π΅) β ran (π ++ π) = (ran π βͺ ran π)) | ||
Theorem | ccatidid 14406 | Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.) |
β’ (β ++ β ) = β | ||
Theorem | lswccatn0lsw 14407 | 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.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β ) β (lastSβ(π΄ ++ π΅)) = (lastSβπ΅)) | ||
Theorem | lswccat0lsw 14408 | 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.) |
β’ (π β Word π β (lastSβ(π ++ β )) = (lastSβπ)) | ||
Theorem | ccatalpha 14409 | 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.) |
β’ ((π΄ β Word V β§ π΅ β Word V) β ((π΄ ++ π΅) β Word π β (π΄ β Word π β§ π΅ β Word π))) | ||
Theorem | ccatrcl1 14410 | 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.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ (π = (π΄ ++ π΅) β§ π β Word π)) β π΄ β Word π) | ||
Syntax | cs1 14411 | Syntax for the singleton word constructor. |
class β¨βπ΄ββ© | ||
Definition | df-s1 14412 | Define the canonical injection from symbols to words. Although not required, π΄ should usually be a set. Otherwise, the singleton word β¨βπ΄ββ© would be the singleton word consisting of the empty set, see s1prc 14420, and not, as maybe expected, the empty word, see also s1nz 14423. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© = {β¨0, ( I βπ΄)β©} | ||
Theorem | ids1 14413 | Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© = β¨β( I βπ΄)ββ© | ||
Theorem | s1val 14414 | Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ β π β β¨βπ΄ββ© = {β¨0, π΄β©}) | ||
Theorem | s1rn 14415 | The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ (π΄ β π β ran β¨βπ΄ββ© = {π΄}) | ||
Theorem | s1eq 14416 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ = π΅ β β¨βπ΄ββ© = β¨βπ΅ββ©) | ||
Theorem | s1eqd 14417 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π β π΄ = π΅) β β’ (π β β¨βπ΄ββ© = β¨βπ΅ββ©) | ||
Theorem | s1cl 14418 | 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.) |
β’ (π΄ β π΅ β β¨βπ΄ββ© β Word π΅) | ||
Theorem | s1cld 14419 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π β π΄ β π΅) β β’ (π β β¨βπ΄ββ© β Word π΅) | ||
Theorem | s1prc 14420 | Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.) |
β’ (Β¬ π΄ β V β β¨βπ΄ββ© = β¨ββ ββ©) | ||
Theorem | s1cli 14421 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© β Word V | ||
Theorem | s1len 14422 | Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (β―ββ¨βπ΄ββ©) = 1 | ||
Theorem | s1nz 14423 | A singleton word is not the empty string. (Contributed by Mario Carneiro, 27-Feb-2016.) (Proof shortened by Kyle Wyonch, 18-Jul-2021.) |
β’ β¨βπ΄ββ© β β | ||
Theorem | s1dm 14424 | The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.) |
β’ dom β¨βπ΄ββ© = {0} | ||
Theorem | s1dmALT 14425 | Alternate version of s1dm 14424, having a shorter proof, but requiring that π΄ is a set. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β π β dom β¨βπ΄ββ© = {0}) | ||
Theorem | s1fv 14426 | Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ β π΅ β (β¨βπ΄ββ©β0) = π΄) | ||
Theorem | lsws1 14427 | The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.) |
β’ (π΄ β π β (lastSββ¨βπ΄ββ©) = π΄) | ||
Theorem | eqs1 14428 | A word of length 1 is a singleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 1-May-2020.) |
β’ ((π β Word π΄ β§ (β―βπ) = 1) β π = β¨β(πβ0)ββ©) | ||
Theorem | wrdl1exs1 14429* | A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.) |
β’ ((π β Word π β§ (β―βπ) = 1) β βπ β π π = β¨βπ ββ©) | ||
Theorem | wrdl1s1 14430 | 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.) |
β’ (π β π β (π = β¨βπββ© β (π β Word π β§ (β―βπ) = 1 β§ (πβ0) = π))) | ||
Theorem | s111 14431 | The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ ((π β π΄ β§ π β π΄) β (β¨βπββ© = β¨βπββ© β π = π)) | ||
Theorem | ccatws1cl 14432 | The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
β’ ((π β Word π β§ π β π) β (π ++ β¨βπββ©) β Word π) | ||
Theorem | ccatws1clv 14433 | The concatenation of a word with a singleton word (which can be over a different alphabet) is a word. (Contributed by AV, 5-Mar-2022.) |
β’ (π β Word π β (π ++ β¨βπββ©) β Word V) | ||
Theorem | ccat2s1cl 14434 | The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
β’ ((π β π β§ π β π) β (β¨βπββ© ++ β¨βπββ©) β Word π) | ||
Theorem | ccats1alpha 14435 | A concatenation of a word with a singleton word is a word over an alphabet π iff the symbols of both words belong to the alphabet π. (Contributed by AV, 27-Mar-2022.) |
β’ ((π΄ β Word π β§ π β π) β ((π΄ ++ β¨βπββ©) β Word π β (π΄ β Word π β§ π β π))) | ||
Theorem | ccatws1len 14436 | 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.) |
β’ (π β Word π β (β―β(π ++ β¨βπββ©)) = ((β―βπ) + 1)) | ||
Theorem | ccatws1lenp1b 14437 | The length of a word is π iff the length of the concatenation of the word with a singleton word is π + 1. (Contributed by AV, 4-Mar-2022.) |
β’ ((π β Word π β§ π β β0) β ((β―β(π ++ β¨βπββ©)) = (π + 1) β (β―βπ) = π)) | ||
Theorem | wrdlenccats1lenm1 14438 | 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.) |
β’ (π β Word π β ((β―β(π ++ β¨βπββ©)) β 1) = (β―βπ)) | ||
Theorem | ccat2s1len 14439 | The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 14-Jan-2024.) |
β’ (β―β(β¨βπββ© ++ β¨βπββ©)) = 2 | ||
Theorem | ccatw2s1cl 14440 | The concatenation of a word with two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
β’ ((π β Word π β§ π β π β§ π β π) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π) | ||
Theorem | ccatw2s1len 14441 | 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.) |
β’ (π β Word π β (β―β((π ++ β¨βπββ©) ++ β¨βπββ©)) = ((β―βπ) + 2)) | ||
Theorem | ccats1val1 14442 | 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.) |
β’ ((π β Word π β§ πΌ β (0..^(β―βπ))) β ((π ++ β¨βπββ©)βπΌ) = (πβπΌ)) | ||
Theorem | ccats1val2 14443 | 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.) |
β’ ((π β Word π β§ π β π β§ πΌ = (β―βπ)) β ((π ++ β¨βπββ©)βπΌ) = π) | ||
Theorem | ccat1st1st 14444 | The first symbol of a word concatenated with its first symbol is the first symbol of the word. This theorem holds even if π is the empty word. (Contributed by AV, 26-Mar-2022.) |
β’ (π β Word π β ((π ++ β¨β(πβ0)ββ©)β0) = (πβ0)) | ||
Theorem | ccat2s1p1 14445 | Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 20-Jan-2024.) |
β’ (π β π β ((β¨βπββ© ++ β¨βπββ©)β0) = π) | ||
Theorem | ccat2s1p2 14446 | Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 20-Jan-2024.) |
β’ (π β π β ((β¨βπββ© ++ β¨βπββ©)β1) = π) | ||
Theorem | ccatw2s1ass 14447 | Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
β’ (π β Word π β ((π ++ β¨βπββ©) ++ β¨βπββ©) = (π ++ (β¨βπββ© ++ β¨βπββ©))) | ||
Theorem | ccatw2s1assOLD 14448 | Obsolete version of ccatw2s1ass 14447 as of 29-Jan-2024. Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Word π β§ π β π β§ π β π) β ((π ++ β¨βπββ©) ++ β¨βπββ©) = (π ++ (β¨βπββ© ++ β¨βπββ©))) | ||
Theorem | ccatws1n0 14449 | The concatenation of a word with a singleton word is not the empty set. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 5-Mar-2022.) |
β’ (π β Word π β (π ++ β¨βπββ©) β β ) | ||
Theorem | ccatws1ls 14450 | 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.) |
β’ ((π β Word π β§ π β π) β ((π ++ β¨βπββ©)β(β―βπ)) = π) | ||
Theorem | lswccats1 14451 | The last symbol of a word concatenated with a singleton word is the symbol of the singleton word. (Contributed by AV, 6-Aug-2018.) (Proof shortened by AV, 22-Oct-2018.) |
β’ ((π β Word π β§ π β π) β (lastSβ(π ++ β¨βπββ©)) = π) | ||
Theorem | lswccats1fst 14452 | 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.) |
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (lastSβ(π ++ β¨β(πβ0)ββ©)) = ((π ++ β¨β(πβ0)ββ©)β0)) | ||
Theorem | ccatw2s1p1 14453 | 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.) |
β’ ((π β Word π β§ (β―βπ) = π β§ π β π) β (((π ++ β¨βπββ©) ++ β¨βπββ©)βπ) = π) | ||
Theorem | ccatw2s1p1OLD 14454 | Obsolete version of ccatw2s1p1 14453 as of 29-Jan-2024. 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (((π β Word π β§ (β―βπ) = π) β§ (π β π β§ π β π)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)βπ) = π) | ||
Theorem | ccatw2s1p2 14455 | 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.) |
β’ (((π β Word π β§ (β―βπ) = π) β§ (π β π β§ π β π)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1)) = π) | ||
Theorem | ccat2s1fvw 14456 | 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.) |
β’ ((π β Word π β§ πΌ β β0 β§ πΌ < (β―βπ)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)βπΌ) = (πβπΌ)) | ||
Theorem | ccat2s1fvwOLD 14457 | Obsolete version of ccat2s1fvw 14456 as of 28-Jan-2024. 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.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (((π β Word π β§ πΌ β β0 β§ πΌ < (β―βπ)) β§ (π β π β§ π β π)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)βπΌ) = (πβπΌ)) | ||
Theorem | ccat2s1fst 14458 | 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.) |
β’ ((π β Word π β§ 0 < (β―βπ)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)β0) = (πβ0)) | ||
Theorem | ccat2s1fstOLD 14459 | Obsolete version of ccat2s1fst 14458 as of 28-Jan-2024. The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (((π β Word π β§ 0 < (β―βπ)) β§ (π β π β§ π β π)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)β0) = (πβ0)) | ||
Syntax | csubstr 14460 | Syntax for the subword operator. |
class substr | ||
Definition | df-substr 14461* | 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 = (π β V, π β (β€ Γ β€) β¦ if(((1st βπ)..^(2nd βπ)) β dom π , (π₯ β (0..^((2nd βπ) β (1st βπ))) β¦ (π β(π₯ + (1st βπ)))), β )) | ||
Theorem | swrdnznd 14462 | The value of a subword operation for noninteger arguments is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6873). (Contributed by AV, 2-Dec-2022.) (New usage is discouraged.) |
β’ (Β¬ (πΉ β β€ β§ πΏ β β€) β (π substr β¨πΉ, πΏβ©) = β ) | ||
Theorem | swrdval 14463* | Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β π β§ πΉ β β€ β§ πΏ β β€) β (π substr β¨πΉ, πΏβ©) = if((πΉ..^πΏ) β dom π, (π₯ β (0..^(πΏ β πΉ)) β¦ (πβ(π₯ + πΉ))), β )) | ||
Theorem | swrd00 14464 | A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ (π substr β¨π, πβ©) = β | ||
Theorem | swrdcl 14465 | Closure of the subword extractor. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (π β Word π΄ β (π substr β¨πΉ, πΏβ©) β Word π΄) | ||
Theorem | swrdval2 14466* | Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 2-May-2020.) |
β’ ((π β Word π΄ β§ πΉ β (0...πΏ) β§ πΏ β (0...(β―βπ))) β (π substr β¨πΉ, πΏβ©) = (π₯ β (0..^(πΏ β πΉ)) β¦ (πβ(π₯ + πΉ)))) | ||
Theorem | swrdlen 14467 | Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ ((π β Word π΄ β§ πΉ β (0...πΏ) β§ πΏ β (0...(β―βπ))) β (β―β(π substr β¨πΉ, πΏβ©)) = (πΏ β πΉ)) | ||
Theorem | swrdfv 14468 | A symbol in an extracted subword, indexed using the subword's indices. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ (((π β Word π΄ β§ πΉ β (0...πΏ) β§ πΏ β (0...(β―βπ))) β§ π β (0..^(πΏ β πΉ))) β ((π substr β¨πΉ, πΏβ©)βπ) = (πβ(π + πΉ))) | ||
Theorem | swrdfv0 14469 | The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022.) |
β’ ((π β Word π΄ β§ πΉ β (0..^πΏ) β§ πΏ β (0...(β―βπ))) β ((π substr β¨πΉ, πΏβ©)β0) = (πβπΉ)) | ||
Theorem | swrdf 14470 | 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.) |
β’ ((π β Word π β§ π β (0...π) β§ π β (0...(β―βπ))) β (π substr β¨π, πβ©):(0..^(π β π))βΆπ) | ||
Theorem | swrdvalfn 14471 | 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.) |
β’ ((π β Word π β§ πΉ β (0...πΏ) β§ πΏ β (0...(β―βπ))) β (π substr β¨πΉ, πΏβ©) Fn (0..^(πΏ β πΉ))) | ||
Theorem | swrdrn 14472 | 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.) |
β’ ((π β Word π β§ π β (0...π) β§ π β (0...(β―βπ))) β ran (π substr β¨π, πβ©) β π) | ||
Theorem | swrdlend 14473 | 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.) |
β’ ((π β Word π β§ πΉ β β€ β§ πΏ β β€) β (πΏ β€ πΉ β (π substr β¨πΉ, πΏβ©) = β )) | ||
Theorem | swrdnd 14474 | 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.) |
β’ ((π β Word π β§ πΉ β β€ β§ πΏ β β€) β ((πΉ < 0 β¨ πΏ β€ πΉ β¨ (β―βπ) < πΏ) β (π substr β¨πΉ, πΏβ©) = β )) | ||
Theorem | swrdnd2 14475 | Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.) |
β’ ((π β Word π β§ π΄ β β€ β§ π΅ β β€) β ((π΅ β€ π΄ β¨ (β―βπ) β€ π΄ β¨ π΅ β€ 0) β (π substr β¨π΄, π΅β©) = β )) | ||
Theorem | swrdnnn0nd 14476 | The value of a subword operation for arguments not being nonnegative integers is the empty set. (Contributed by AV, 2-Dec-2022.) |
β’ ((π β Word π β§ Β¬ (πΉ β β0 β§ πΏ β β0)) β (π substr β¨πΉ, πΏβ©) = β ) | ||
Theorem | swrdnd0 14477 | The value of a subword operation for inproper arguments is the empty set. (Contributed by AV, 2-Dec-2022.) |
β’ (π β Word π β (Β¬ (πΉ β (0...πΏ) β§ πΏ β (0...(β―βπ))) β (π substr β¨πΉ, πΏβ©) = β )) | ||
Theorem | swrd0 14478 | 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.) |
β’ (β substr β¨πΉ, πΏβ©) = β | ||
Theorem | swrdrlen 14479 | Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
β’ ((π β Word π β§ πΌ β (0...(β―βπ))) β (β―β(π substr β¨πΌ, (β―βπ)β©)) = ((β―βπ) β πΌ)) | ||
Theorem | swrdlen2 14480 | Length of an extracted subword. (Contributed by AV, 5-May-2020.) |
β’ ((π β Word π β§ (πΉ β β0 β§ πΏ β (β€β₯βπΉ)) β§ πΏ β€ (β―βπ)) β (β―β(π substr β¨πΉ, πΏβ©)) = (πΏ β πΉ)) | ||
Theorem | swrdfv2 14481 | A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020.) |
β’ (((π β Word π β§ (πΉ β β0 β§ πΏ β (β€β₯βπΉ)) β§ πΏ β€ (β―βπ)) β§ π β (πΉ..^πΏ)) β ((π substr β¨πΉ, πΏβ©)β(π β πΉ)) = (πβπ)) | ||
Theorem | swrdwrdsymb 14482 | A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022.) |
β’ (π β Word π΄ β (π substr β¨π, πβ©) β Word (π β (π..^π))) | ||
Theorem | swrdsb0eq 14483 | Two subwords with the same bounds are equal if the range is not valid. (Contributed by AV, 4-May-2020.) |
β’ (((π β Word π β§ π β Word π) β§ (π β β0 β§ π β β0) β§ π β€ π) β (π substr β¨π, πβ©) = (π substr β¨π, πβ©)) | ||
Theorem | swrdsbslen 14484 | Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020.) |
β’ (((π β Word π β§ π β Word π) β§ (π β β0 β§ π β β0) β§ (π β€ (β―βπ) β§ π β€ (β―βπ))) β (β―β(π substr β¨π, πβ©)) = (β―β(π substr β¨π, πβ©))) | ||
Theorem | swrdspsleq 14485* | 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.) |
β’ (((π β Word π β§ π β Word π) β§ (π β β0 β§ π β β0) β§ (π β€ (β―βπ) β§ π β€ (β―βπ))) β ((π substr β¨π, πβ©) = (π substr β¨π, πβ©) β βπ β (π..^π)(πβπ) = (πβπ))) | ||
Theorem | swrds1 14486 | Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ ((π β Word π΄ β§ πΌ β (0..^(β―βπ))) β (π substr β¨πΌ, (πΌ + 1)β©) = β¨β(πβπΌ)ββ©) | ||
Theorem | swrdlsw 14487 | Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
β’ ((π β Word π β§ π β β ) β (π substr β¨((β―βπ) β 1), (β―βπ)β©) = β¨β(lastSβπ)ββ©) | ||
Theorem | ccatswrd 14488 | Joining two adjacent subwords makes a longer subword. (Contributed by Stefan O'Rear, 20-Aug-2015.) |
β’ ((π β Word π΄ β§ (π β (0...π) β§ π β (0...π) β§ π β (0...(β―βπ)))) β ((π substr β¨π, πβ©) ++ (π substr β¨π, πβ©)) = (π substr β¨π, πβ©)) | ||
Theorem | swrdccat2 14489 | Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ ((π β Word π΅ β§ π β Word π΅) β ((π ++ π) substr β¨(β―βπ), ((β―βπ) + (β―βπ))β©) = π) | ||
Syntax | cpfx 14490 | Syntax for the prefix operator. |
class prefix | ||
Definition | df-pfx 14491* | 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, (π prefix πΏ) is the prefix of the word π of length πΏ. 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 = (π β V, π β β0 β¦ (π substr β¨0, πβ©)) | ||
Theorem | pfxnndmnd 14492 | The value of a prefix operation for out-of-domain arguments. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6873). (Contributed by AV, 3-Dec-2022.) (New usage is discouraged.) |
β’ (Β¬ (π β V β§ πΏ β β0) β (π prefix πΏ) = β ) | ||
Theorem | pfxval 14493 | Value of a prefix operation. (Contributed by AV, 2-May-2020.) |
β’ ((π β π β§ πΏ β β0) β (π prefix πΏ) = (π substr β¨0, πΏβ©)) | ||
Theorem | pfx00 14494 | The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.) |
β’ (π prefix 0) = β | ||
Theorem | pfx0 14495 | A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.) |
β’ (β prefix πΏ) = β | ||
Theorem | pfxval0 14496 | Value of a prefix operation. This theorem should only be used in proofs if πΏ β β0 is not available. Otherwise (and usually), pfxval 14493 should be used. (Contributed by AV, 3-Dec-2022.) (New usage is discouraged.) |
β’ (π β Word π΄ β (π prefix πΏ) = (π substr β¨0, πΏβ©)) | ||
Theorem | pfxcl 14497 | Closure of the prefix extractor. (Contributed by AV, 2-May-2020.) |
β’ (π β Word π΄ β (π prefix πΏ) β Word π΄) | ||
Theorem | pfxmpt 14498* | Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020.) |
β’ ((π β Word π΄ β§ πΏ β (0...(β―βπ))) β (π prefix πΏ) = (π₯ β (0..^πΏ) β¦ (πβπ₯))) | ||
Theorem | pfxres 14499 | Value of the subword extractor for left-anchored subwords. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.) |
β’ ((π β Word π΄ β§ πΏ β (0...(β―βπ))) β (π prefix πΏ) = (π βΎ (0..^πΏ))) | ||
Theorem | pfxf 14500 | 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.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (π prefix πΏ):(0..^πΏ)βΆπ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |