![]() |
Metamath
Proof Explorer Theorem List (p. 146 of 479) | < 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | len0nnbi 14501 | The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.) |
β’ (π β Word π β (π β β β (β―βπ) β β)) | ||
Theorem | wrdlenge2n0 14502 | A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018.) (Proof shortened by AV, 14-Oct-2018.) |
β’ ((π β Word π β§ 2 β€ (β―βπ)) β π β β ) | ||
Theorem | wrdsymb1 14503 | The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.) |
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (πβ0) β π) | ||
Theorem | wrdlen1 14504* | A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018.) (Proof shortened by AV, 19-Oct-2018.) |
β’ ((π β Word π β§ (β―βπ) = 1) β βπ£ β π (πβ0) = π£) | ||
Theorem | fstwrdne 14505 | 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.) |
β’ ((π β Word π β§ π β β ) β (πβ0) β π) | ||
Theorem | fstwrdne0 14506 | 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.) |
β’ ((π β β β§ (π β Word π β§ (β―βπ) = π)) β (πβ0) β π) | ||
Theorem | eqwrd 14507* | 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.) |
β’ ((π β Word π β§ π β Word π) β (π = π β ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(πβπ) = (πβπ)))) | ||
Theorem | elovmpowrd 14508* | 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 π may depend on π§ as well as on π£ and π¦. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
β’ π = (π£ β V, π¦ β V β¦ {π§ β Word π£ β£ π}) β β’ (π β (πππ) β (π β V β§ π β V β§ π β Word π)) | ||
Theorem | elovmptnn0wrd 14509* | Implications for the value of an operation defined by the maps-to notation with a function of nonnegative integers into a class abstraction of words as a result having an element. Note that π may depend on π§ as well as on π£ and π¦ and π. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.) |
β’ π = (π£ β V, π¦ β V β¦ (π β β0 β¦ {π§ β Word π£ β£ π})) β β’ (π β ((πππ)βπ) β ((π β V β§ π β V) β§ (π β β0 β§ π β Word π))) | ||
Theorem | wrdred1 14510 | A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.) |
β’ (πΉ β Word π β (πΉ βΎ (0..^((β―βπΉ) β 1))) β Word π) | ||
Theorem | wrdred1hash 14511 | The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.) |
β’ ((πΉ β Word π β§ 1 β€ (β―βπΉ)) β (β―β(πΉ βΎ (0..^((β―βπΉ) β 1)))) = ((β―βπΉ) β 1)) | ||
Syntax | clsw 14512 | Extend class notation with the Last Symbol of a word. |
class lastS | ||
Definition | df-lsw 14513 | 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 = (π€ β V β¦ (π€β((β―βπ€) β 1))) | ||
Theorem | lsw 14514 | Extract the last symbol of a word. May be not meaningful for other sets which are not words. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
β’ (π β π β (lastSβπ) = (πβ((β―βπ) β 1))) | ||
Theorem | lsw0 14515 | 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.) |
β’ ((π β Word π β§ (β―βπ) = 0) β (lastSβπ) = β ) | ||
Theorem | lsw0g 14516 | The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.) |
β’ (lastSββ ) = β | ||
Theorem | lsw1 14517 | 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.) |
β’ ((π β Word π β§ (β―βπ) = 1) β (lastSβπ) = (πβ0)) | ||
Theorem | lswcl 14518 | Closure of the last symbol: the last symbol of a not empty word belongs to the alphabet for the word. (Contributed by AV, 2-Aug-2018.) (Proof shortened by AV, 29-Apr-2020.) |
β’ ((π β Word π β§ π β β ) β (lastSβπ) β π) | ||
Theorem | lswlgt0cl 14519 | The last symbol of a nonempty word is element of the alphabet for the word. (Contributed by Alexander van der Vekens, 1-Oct-2018.) (Proof shortened by AV, 29-Apr-2020.) |
β’ ((π β β β§ (π β Word π β§ (β―βπ) = π)) β (lastSβπ) β π) | ||
Syntax | cconcat 14520 | Syntax for the concatenation operator. |
class ++ | ||
Definition | df-concat 14521* | 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.) |
β’ ++ = (π β V, π‘ β V β¦ (π₯ β (0..^((β―βπ ) + (β―βπ‘))) β¦ if(π₯ β (0..^(β―βπ )), (π βπ₯), (π‘β(π₯ β (β―βπ )))))) | ||
Theorem | ccatfn 14522 | The concatenation operator is a two-argument function. (Contributed by Mario Carneiro, 27-Sep-2015.) (Proof shortened by AV, 29-Apr-2020.) |
β’ ++ Fn (V Γ V) | ||
Theorem | ccatfval 14523* | Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β π β§ π β π) β (π ++ π) = (π₯ β (0..^((β―βπ) + (β―βπ))) β¦ if(π₯ β (0..^(β―βπ)), (πβπ₯), (πβ(π₯ β (β―βπ)))))) | ||
Theorem | ccatcl 14524 | 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.) |
β’ ((π β Word π΅ β§ π β Word π΅) β (π ++ π) β Word π΅) | ||
Theorem | ccatlen 14525 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.) |
β’ ((π β Word π΄ β§ π β Word π΅) β (β―β(π ++ π)) = ((β―βπ) + (β―βπ))) | ||
Theorem | ccat0 14526 | 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.) |
β’ ((π β Word π΄ β§ π β Word π΅) β ((π ++ π) = β β (π = β β§ π = β ))) | ||
Theorem | ccatval1 14527 | 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.) |
β’ ((π β Word π΄ β§ π β Word π΅ β§ πΌ β (0..^(β―βπ))) β ((π ++ π)βπΌ) = (πβπΌ)) | ||
Theorem | ccatval2 14528 | 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.) |
β’ ((π β Word π΅ β§ π β Word π΅ β§ πΌ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β ((π ++ π)βπΌ) = (πβ(πΌ β (β―βπ)))) | ||
Theorem | ccatval3 14529 | 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.) |
β’ ((π β Word π΅ β§ π β Word π΅ β§ πΌ β (0..^(β―βπ))) β ((π ++ π)β(πΌ + (β―βπ))) = (πβπΌ)) | ||
Theorem | elfzelfzccat 14530 | 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.) |
β’ ((π΄ β Word π β§ π΅ β Word π) β (π β (0...(β―βπ΄)) β π β (0...(β―β(π΄ ++ π΅))))) | ||
Theorem | ccatvalfn 14531 | 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.) |
β’ ((π΄ β Word π β§ π΅ β Word π) β (π΄ ++ π΅) Fn (0..^((β―βπ΄) + (β―βπ΅)))) | ||
Theorem | ccatsymb 14532 | The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018.) (Proof shortened by AV, 24-Nov-2018.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ πΌ β β€) β ((π΄ ++ π΅)βπΌ) = if(πΌ < (β―βπ΄), (π΄βπΌ), (π΅β(πΌ β (β―βπ΄))))) | ||
Theorem | ccatfv0 14533 | 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.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ 0 < (β―βπ΄)) β ((π΄ ++ π΅)β0) = (π΄β0)) | ||
Theorem | ccatval1lsw 14534 | 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.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΄ β β ) β ((π΄ ++ π΅)β((β―βπ΄) β 1)) = (lastSβπ΄)) | ||
Theorem | ccatval21sw 14535 | The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β ) β ((π΄ ++ π΅)β(β―βπ΄)) = (π΅β0)) | ||
Theorem | ccatlid 14536 | 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 14537 | 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 14538 | Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β Word π΅ β§ π β Word π΅ β§ π β Word π΅) β ((π ++ π) ++ π) = (π ++ (π ++ π))) | ||
Theorem | ccatrn 14539 | The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β Word π΅ β§ π β Word π΅) β ran (π ++ π) = (ran π βͺ ran π)) | ||
Theorem | ccatidid 14540 | Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.) |
β’ (β ++ β ) = β | ||
Theorem | lswccatn0lsw 14541 | 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 14542 | 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 14543 | 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 14544 | 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 14545 | Syntax for the singleton word constructor. |
class β¨βπ΄ββ© | ||
Definition | df-s1 14546 | 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 14554, and not, as maybe expected, the empty word, see also s1nz 14557. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© = {β¨0, ( I βπ΄)β©} | ||
Theorem | ids1 14547 | Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© = β¨β( I βπ΄)ββ© | ||
Theorem | s1val 14548 | Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ β π β β¨βπ΄ββ© = {β¨0, π΄β©}) | ||
Theorem | s1rn 14549 | The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ (π΄ β π β ran β¨βπ΄ββ© = {π΄}) | ||
Theorem | s1eq 14550 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ = π΅ β β¨βπ΄ββ© = β¨βπ΅ββ©) | ||
Theorem | s1eqd 14551 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π β π΄ = π΅) β β’ (π β β¨βπ΄ββ© = β¨βπ΅ββ©) | ||
Theorem | s1cl 14552 | 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 14553 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π β π΄ β π΅) β β’ (π β β¨βπ΄ββ© β Word π΅) | ||
Theorem | s1prc 14554 | Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.) |
β’ (Β¬ π΄ β V β β¨βπ΄ββ© = β¨ββ ββ©) | ||
Theorem | s1cli 14555 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© β Word V | ||
Theorem | s1len 14556 | Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (β―ββ¨βπ΄ββ©) = 1 | ||
Theorem | s1nz 14557 | 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 14558 | The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.) |
β’ dom β¨βπ΄ββ© = {0} | ||
Theorem | s1dmALT 14559 | Alternate version of s1dm 14558, 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 14560 | Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ β π΅ β (β¨βπ΄ββ©β0) = π΄) | ||
Theorem | lsws1 14561 | The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.) |
β’ (π΄ β π β (lastSββ¨βπ΄ββ©) = π΄) | ||
Theorem | eqs1 14562 | 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 14563* | A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.) |
β’ ((π β Word π β§ (β―βπ) = 1) β βπ β π π = β¨βπ ββ©) | ||
Theorem | wrdl1s1 14564 | 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 14565 | The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ ((π β π΄ β§ π β π΄) β (β¨βπββ© = β¨βπββ© β π = π)) | ||
Theorem | ccatws1cl 14566 | 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 14567 | 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 14568 | The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
β’ ((π β π β§ π β π) β (β¨βπββ© ++ β¨βπββ©) β Word π) | ||
Theorem | ccats1alpha 14569 | 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 14570 | 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 14571 | 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 14572 | 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 14573 | 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 14574 | 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 14575 | 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 14576 | 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 14577 | 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 14578 | 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 14579 | 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 14580 | 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 14581 | Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
β’ (π β Word π β ((π ++ β¨βπββ©) ++ β¨βπββ©) = (π ++ (β¨βπββ© ++ β¨βπββ©))) | ||
Theorem | ccatws1n0 14582 | 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 14583 | 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 14584 | 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 14585 | 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 14586 | 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 | ccatw2s1p2 14587 | 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 14588 | 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 | ccat2s1fst 14589 | 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)) | ||
Syntax | csubstr 14590 | Syntax for the subword operator. |
class substr | ||
Definition | df-substr 14591* | 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 14592 | 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 6927). (Contributed by AV, 2-Dec-2022.) (New usage is discouraged.) |
β’ (Β¬ (πΉ β β€ β§ πΏ β β€) β (π substr β¨πΉ, πΏβ©) = β ) | ||
Theorem | swrdval 14593* | Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β π β§ πΉ β β€ β§ πΏ β β€) β (π substr β¨πΉ, πΏβ©) = if((πΉ..^πΏ) β dom π, (π₯ β (0..^(πΏ β πΉ)) β¦ (πβ(π₯ + πΉ))), β )) | ||
Theorem | swrd00 14594 | A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ (π substr β¨π, πβ©) = β | ||
Theorem | swrdcl 14595 | 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 14596* | 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 14597 | Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ ((π β Word π΄ β§ πΉ β (0...πΏ) β§ πΏ β (0...(β―βπ))) β (β―β(π substr β¨πΉ, πΏβ©)) = (πΏ β πΉ)) | ||
Theorem | swrdfv 14598 | 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 14599 | The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022.) |
β’ ((π β Word π΄ β§ πΉ β (0..^πΏ) β§ πΏ β (0...(β―βπ))) β ((π substr β¨πΉ, πΏβ©)β0) = (πβπΉ)) | ||
Theorem | swrdf 14600 | 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..^(π β π))βΆπ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |