![]() |
Metamath
Proof Explorer Theorem List (p. 147 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | swrdval2 14601* | 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 14602 | Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ ((π β Word π΄ β§ πΉ β (0...πΏ) β§ πΏ β (0...(β―βπ))) β (β―β(π substr β¨πΉ, πΏβ©)) = (πΏ β πΉ)) | ||
Theorem | swrdfv 14603 | 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 14604 | The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022.) |
β’ ((π β Word π΄ β§ πΉ β (0..^πΏ) β§ πΏ β (0...(β―βπ))) β ((π substr β¨πΉ, πΏβ©)β0) = (πβπΉ)) | ||
Theorem | swrdf 14605 | 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 14606 | 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 14607 | 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 14608 | 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 14609 | 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 14610 | Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.) |
β’ ((π β Word π β§ π΄ β β€ β§ π΅ β β€) β ((π΅ β€ π΄ β¨ (β―βπ) β€ π΄ β¨ π΅ β€ 0) β (π substr β¨π΄, π΅β©) = β )) | ||
Theorem | swrdnnn0nd 14611 | 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 14612 | 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 14613 | 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 14614 | Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
β’ ((π β Word π β§ πΌ β (0...(β―βπ))) β (β―β(π substr β¨πΌ, (β―βπ)β©)) = ((β―βπ) β πΌ)) | ||
Theorem | swrdlen2 14615 | Length of an extracted subword. (Contributed by AV, 5-May-2020.) |
β’ ((π β Word π β§ (πΉ β β0 β§ πΏ β (β€β₯βπΉ)) β§ πΏ β€ (β―βπ)) β (β―β(π substr β¨πΉ, πΏβ©)) = (πΏ β πΉ)) | ||
Theorem | swrdfv2 14616 | A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020.) |
β’ (((π β Word π β§ (πΉ β β0 β§ πΏ β (β€β₯βπΉ)) β§ πΏ β€ (β―βπ)) β§ π β (πΉ..^πΏ)) β ((π substr β¨πΉ, πΏβ©)β(π β πΉ)) = (πβπ)) | ||
Theorem | swrdwrdsymb 14617 | A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022.) |
β’ (π β Word π΄ β (π substr β¨π, πβ©) β Word (π β (π..^π))) | ||
Theorem | swrdsb0eq 14618 | 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 14619 | Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020.) |
β’ (((π β Word π β§ π β Word π) β§ (π β β0 β§ π β β0) β§ (π β€ (β―βπ) β§ π β€ (β―βπ))) β (β―β(π substr β¨π, πβ©)) = (β―β(π substr β¨π, πβ©))) | ||
Theorem | swrdspsleq 14620* | 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 14621 | Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ ((π β Word π΄ β§ πΌ β (0..^(β―βπ))) β (π substr β¨πΌ, (πΌ + 1)β©) = β¨β(πβπΌ)ββ©) | ||
Theorem | swrdlsw 14622 | Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
β’ ((π β Word π β§ π β β ) β (π substr β¨((β―βπ) β 1), (β―βπ)β©) = β¨β(lastSβπ)ββ©) | ||
Theorem | ccatswrd 14623 | 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 14624 | Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ ((π β Word π΅ β§ π β Word π΅) β ((π ++ π) substr β¨(β―βπ), ((β―βπ) + (β―βπ))β©) = π) | ||
Syntax | cpfx 14625 | Syntax for the prefix operator. |
class prefix | ||
Definition | df-pfx 14626* | 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 14627 | 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 6927). (Contributed by AV, 3-Dec-2022.) (New usage is discouraged.) |
β’ (Β¬ (π β V β§ πΏ β β0) β (π prefix πΏ) = β ) | ||
Theorem | pfxval 14628 | Value of a prefix operation. (Contributed by AV, 2-May-2020.) |
β’ ((π β π β§ πΏ β β0) β (π prefix πΏ) = (π substr β¨0, πΏβ©)) | ||
Theorem | pfx00 14629 | The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.) |
β’ (π prefix 0) = β | ||
Theorem | pfx0 14630 | A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.) |
β’ (β prefix πΏ) = β | ||
Theorem | pfxval0 14631 | Value of a prefix operation. This theorem should only be used in proofs if πΏ β β0 is not available. Otherwise (and usually), pfxval 14628 should be used. (Contributed by AV, 3-Dec-2022.) (New usage is discouraged.) |
β’ (π β Word π΄ β (π prefix πΏ) = (π substr β¨0, πΏβ©)) | ||
Theorem | pfxcl 14632 | Closure of the prefix extractor. (Contributed by AV, 2-May-2020.) |
β’ (π β Word π΄ β (π prefix πΏ) β Word π΄) | ||
Theorem | pfxmpt 14633* | Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020.) |
β’ ((π β Word π΄ β§ πΏ β (0...(β―βπ))) β (π prefix πΏ) = (π₯ β (0..^πΏ) β¦ (πβπ₯))) | ||
Theorem | pfxres 14634 | 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 14635 | 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..^πΏ)βΆπ) | ||
Theorem | pfxfn 14636 | Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (π prefix πΏ) Fn (0..^πΏ)) | ||
Theorem | pfxfv 14637 | 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.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ πΌ β (0..^πΏ)) β ((π prefix πΏ)βπΌ) = (πβπΌ)) | ||
Theorem | pfxlen 14638 | Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.) |
β’ ((π β Word π΄ β§ πΏ β (0...(β―βπ))) β (β―β(π prefix πΏ)) = πΏ) | ||
Theorem | pfxid 14639 | A word is a prefix of itself. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by AV, 2-May-2020.) |
β’ (π β Word π΄ β (π prefix (β―βπ)) = π) | ||
Theorem | pfxrn 14640 | 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.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β ran (π prefix πΏ) β π) | ||
Theorem | pfxn0 14641 | 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.) |
β’ ((π β Word π β§ πΏ β β β§ πΏ β€ (β―βπ)) β (π prefix πΏ) β β ) | ||
Theorem | pfxnd 14642 | 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 ndmfv 6927). (Contributed by AV, 3-May-2020.) |
β’ ((π β Word π β§ πΏ β β0 β§ (β―βπ) < πΏ) β (π prefix πΏ) = β ) | ||
Theorem | pfxnd0 14643 | The value of a prefix operation for a length argument not in the range of the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6927). (Contributed by AV, 3-Dec-2022.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (π prefix πΏ) = β ) | ||
Theorem | pfxwrdsymb 14644 | A prefix of a word is a word over the symbols it consists of. (Contributed by AV, 3-Dec-2022.) |
β’ (π β Word π΄ β (π prefix πΏ) β Word (π β (0..^πΏ))) | ||
Theorem | addlenrevpfx 14645 | The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (Revised by AV, 3-May-2020.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β ((β―β(π substr β¨π, (β―βπ)β©)) + (β―β(π prefix π))) = (β―βπ)) | ||
Theorem | addlenpfx 14646 | 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.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β ((β―β(π prefix π)) + (β―β(π substr β¨π, (β―βπ)β©))) = (β―βπ)) | ||
Theorem | pfxfv0 14647 | 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.) |
β’ ((π β Word π β§ πΏ β (1...(β―βπ))) β ((π prefix πΏ)β0) = (πβ0)) | ||
Theorem | pfxtrcfv 14648 | A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.) |
β’ ((π β Word π β§ π β β β§ πΌ β (0..^((β―βπ) β 1))) β ((π prefix ((β―βπ) β 1))βπΌ) = (πβπΌ)) | ||
Theorem | pfxtrcfv0 14649 | 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.) |
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((π prefix ((β―βπ) β 1))β0) = (πβ0)) | ||
Theorem | pfxfvlsw 14650 | 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.) |
β’ ((π β Word π β§ πΏ β (1...(β―βπ))) β (lastSβ(π prefix πΏ)) = (πβ(πΏ β 1))) | ||
Theorem | pfxeq 14651* | 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.) |
β’ (((π β Word π β§ π β Word π) β§ (π β β0 β§ π β β0) β§ (π β€ (β―βπ) β§ π β€ (β―βπ))) β ((π prefix π) = (π prefix π) β (π = π β§ βπ β (0..^π)(πβπ) = (πβπ)))) | ||
Theorem | pfxtrcfvl 14652 | The last symbol in a word truncated by one symbol. (Contributed by AV, 16-Jun-2018.) (Revised by AV, 5-May-2020.) |
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (lastSβ(π prefix ((β―βπ) β 1))) = (πβ((β―βπ) β 2))) | ||
Theorem | pfxsuffeqwrdeq 14653 | 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.) |
β’ ((π β Word π β§ π β Word π β§ πΌ β (0..^(β―βπ))) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix πΌ) = (π prefix πΌ) β§ (π substr β¨πΌ, (β―βπ)β©) = (π substr β¨πΌ, (β―βπ)β©))))) | ||
Theorem | pfxsuff1eqwrdeq 14654 | 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.) |
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 1)) = (π prefix ((β―βπ) β 1)) β§ (lastSβπ) = (lastSβπ))))) | ||
Theorem | disjwrdpfx 14655* | Sets of words are disjoint if each set contains exactly the extensions of distinct words of a fixed length. Remark: A word π is called an "extension" of a word π if π is a prefix of π. (Contributed by AV, 29-Jul-2018.) (Revised by AV, 6-May-2020.) |
β’ Disj π¦ β π {π₯ β Word π β£ (π₯ prefix π) = π¦} | ||
Theorem | ccatpfx 14656 | Concatenating a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020.) |
β’ ((π β Word π΄ β§ π β (0...π) β§ π β (0...(β―βπ))) β ((π prefix π) ++ (π substr β¨π, πβ©)) = (π prefix π)) | ||
Theorem | pfxccat1 14657 | Recover the left half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by AV, 6-May-2020.) |
β’ ((π β Word π΅ β§ π β Word π΅) β ((π ++ π) prefix (β―βπ)) = π) | ||
Theorem | pfx1 14658 | The prefix of length one of a nonempty word expressed as a singleton word. (Contributed by AV, 15-May-2020.) |
β’ ((π β Word π β§ π β β ) β (π prefix 1) = β¨β(πβ0)ββ©) | ||
Theorem | swrdswrdlem 14659 | Lemma for swrdswrd 14660. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
β’ (((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β§ (πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π)))) β (π β Word π β§ (π + πΎ) β (0...(π + πΏ)) β§ (π + πΏ) β (0...(β―βπ)))) | ||
Theorem | swrdswrd 14660 | A subword of a subword is a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
β’ ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π))) β ((π substr β¨π, πβ©) substr β¨πΎ, πΏβ©) = (π substr β¨(π + πΎ), (π + πΏ)β©))) | ||
Theorem | pfxswrd 14661 | A prefix of a subword is a subword. (Contributed by AV, 2-Apr-2018.) (Revised by AV, 8-May-2020.) |
β’ ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β (πΏ β (0...(π β π)) β ((π substr β¨π, πβ©) prefix πΏ) = (π substr β¨π, (π + πΏ)β©))) | ||
Theorem | swrdpfx 14662 | A subword of a prefix is a subword. (Contributed by Alexander van der Vekens, 6-Apr-2018.) (Revised by AV, 8-May-2020.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β ((πΎ β (0...π) β§ πΏ β (πΎ...π)) β ((π prefix π) substr β¨πΎ, πΏβ©) = (π substr β¨πΎ, πΏβ©))) | ||
Theorem | pfxpfx 14663 | A prefix of a prefix is a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by AV, 8-May-2020.) |
β’ ((π β Word π β§ π β (0...(β―βπ)) β§ πΏ β (0...π)) β ((π prefix π) prefix πΏ) = (π prefix πΏ)) | ||
Theorem | pfxpfxid 14664 | A prefix of a prefix with the same length is the original prefix. In other words, the operation "prefix of length π " is idempotent. (Contributed by AV, 5-Apr-2018.) (Revised by AV, 8-May-2020.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β ((π prefix π) prefix π) = (π prefix π)) | ||
Theorem | pfxcctswrd 14665 | 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.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β ((π prefix π) ++ (π substr β¨π, (β―βπ)β©)) = π) | ||
Theorem | lenpfxcctswrd 14666 | 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.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β (β―β((π prefix π) ++ (π substr β¨π, (β―βπ)β©))) = (β―βπ)) | ||
Theorem | lenrevpfxcctswrd 14667 | 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.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β (β―β((π substr β¨π, (β―βπ)β©) ++ (π prefix π))) = (β―βπ)) | ||
Theorem | pfxlswccat 14668 | 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.) |
β’ ((π β Word π β§ π β β ) β ((π prefix ((β―βπ) β 1)) ++ β¨β(lastSβπ)ββ©) = π) | ||
Theorem | ccats1pfxeq 14669 | 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.) |
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π prefix (β―βπ)) β π = (π ++ β¨β(lastSβπ)ββ©))) | ||
Theorem | ccats1pfxeqrex 14670* | 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.) |
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π prefix (β―βπ)) β βπ β π π = (π ++ β¨βπ ββ©))) | ||
Theorem | ccatopth 14671 | An opth 5477-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.) |
β’ (((π΄ β Word π β§ π΅ β Word π) β§ (πΆ β Word π β§ π· β Word π) β§ (β―βπ΄) = (β―βπΆ)) β ((π΄ ++ π΅) = (πΆ ++ π·) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | ccatopth2 14672 | An opth 5477-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ (((π΄ β Word π β§ π΅ β Word π) β§ (πΆ β Word π β§ π· β Word π) β§ (β―βπ΅) = (β―βπ·)) β ((π΄ ++ π΅) = (πΆ ++ π·) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | ccatlcan 14673 | Concatenation of words is left-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ πΆ β Word π) β ((πΆ ++ π΄) = (πΆ ++ π΅) β π΄ = π΅)) | ||
Theorem | ccatrcan 14674 | Concatenation of words is right-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ πΆ β Word π) β ((π΄ ++ πΆ) = (π΅ ++ πΆ) β π΄ = π΅)) | ||
Theorem | wrdeqs1cat 14675 | 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.) |
β’ ((π β Word π΄ β§ π β β ) β π = (β¨β(πβ0)ββ© ++ (π substr β¨1, (β―βπ)β©))) | ||
Theorem | cats1un 14676 | Express a word with an extra symbol as the union of the word and the new value. (Contributed by Mario Carneiro, 28-Feb-2016.) |
β’ ((π΄ β Word π β§ π΅ β π) β (π΄ ++ β¨βπ΅ββ©) = (π΄ βͺ {β¨(β―βπ΄), π΅β©})) | ||
Theorem | wrdind 14677* | 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.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ ((π¦ β Word π΅ β§ π§ β π΅) β (π β π)) β β’ (π΄ β Word π΅ β π) | ||
Theorem | wrd2ind 14678* | 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.) |
β’ ((π₯ = β β§ π€ = β ) β (π β π)) & β’ ((π₯ = π¦ β§ π€ = π’) β (π β π)) & β’ ((π₯ = (π¦ ++ β¨βπ§ββ©) β§ π€ = (π’ ++ β¨βπ ββ©)) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π€ = π΅ β (π β π)) & β’ π & β’ (((π¦ β Word π β§ π§ β π) β§ (π’ β Word π β§ π β π) β§ (β―βπ¦) = (β―βπ’)) β (π β π)) β β’ ((π΄ β Word π β§ π΅ β Word π β§ (β―βπ΄) = (β―βπ΅)) β π) | ||
Theorem | swrdccatfn 14679 | The subword of a concatenation as function. (Contributed by Alexander van der Vekens, 27-May-2018.) |
β’ (((π΄ β Word π β§ π΅ β Word π) β§ (π β (0...π) β§ π β (0...((β―βπ΄) + (β―βπ΅))))) β ((π΄ ++ π΅) substr β¨π, πβ©) Fn (0..^(π β π))) | ||
Theorem | swrdccatin1 14680 | The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) |
β’ ((π΄ β Word π β§ π΅ β Word π) β ((π β (0...π) β§ π β (0...(β―βπ΄))) β ((π΄ ++ π΅) substr β¨π, πβ©) = (π΄ substr β¨π, πβ©))) | ||
Theorem | pfxccatin12lem4 14681 | Lemma 4 for pfxccatin12 14688. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.) |
β’ ((πΏ β β0 β§ π β β0 β§ π β β€) β ((πΎ β (0..^(π β π)) β§ Β¬ πΎ β (0..^(πΏ β π))) β πΎ β ((πΏ β π)..^((πΏ β π) + (π β πΏ))))) | ||
Theorem | pfxccatin12lem2a 14682 | Lemma for pfxccatin12lem2 14686. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
β’ ((π β (0...πΏ) β§ π β (πΏ...π)) β ((πΎ β (0..^(π β π)) β§ Β¬ πΎ β (0..^(πΏ β π))) β (πΎ + π) β (πΏ..^π))) | ||
Theorem | pfxccatin12lem1 14683 | Lemma 1 for pfxccatin12 14688. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.) |
β’ ((π β (0...πΏ) β§ π β (πΏ...π)) β ((πΎ β (0..^(π β π)) β§ Β¬ πΎ β (0..^(πΏ β π))) β (πΎ β (πΏ β π)) β (0..^(π β πΏ)))) | ||
Theorem | swrdccatin2 14684 | The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
β’ πΏ = (β―βπ΄) β β’ ((π΄ β Word π β§ π΅ β Word π) β ((π β (πΏ...π) β§ π β (πΏ...(πΏ + (β―βπ΅)))) β ((π΄ ++ π΅) substr β¨π, πβ©) = (π΅ substr β¨(π β πΏ), (π β πΏ)β©))) | ||
Theorem | pfxccatin12lem2c 14685 | Lemma for pfxccatin12lem2 14686 and pfxccatin12lem3 14687. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
β’ πΏ = (β―βπ΄) β β’ (((π΄ β Word π β§ π΅ β Word π) β§ (π β (0...πΏ) β§ π β (πΏ...(πΏ + (β―βπ΅))))) β ((π΄ ++ π΅) β Word π β§ π β (0...π) β§ π β (0...(β―β(π΄ ++ π΅))))) | ||
Theorem | pfxccatin12lem2 14686 | Lemma 2 for pfxccatin12 14688. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.) |
β’ πΏ = (β―βπ΄) β β’ (((π΄ β Word π β§ π΅ β Word π) β§ (π β (0...πΏ) β§ π β (πΏ...(πΏ + (β―βπ΅))))) β ((πΎ β (0..^(π β π)) β§ Β¬ πΎ β (0..^(πΏ β π))) β (((π΄ ++ π΅) substr β¨π, πβ©)βπΎ) = ((π΅ prefix (π β πΏ))β(πΎ β (β―β(π΄ substr β¨π, πΏβ©)))))) | ||
Theorem | pfxccatin12lem3 14687 | Lemma 3 for pfxccatin12 14688. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
β’ πΏ = (β―βπ΄) β β’ (((π΄ β Word π β§ π΅ β Word π) β§ (π β (0...πΏ) β§ π β (πΏ...(πΏ + (β―βπ΅))))) β ((πΎ β (0..^(π β π)) β§ πΎ β (0..^(πΏ β π))) β (((π΄ ++ π΅) substr β¨π, πβ©)βπΎ) = ((π΄ substr β¨π, πΏβ©)βπΎ))) | ||
Theorem | pfxccatin12 14688 | The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by AV, 9-May-2020.) |
β’ πΏ = (β―βπ΄) β β’ ((π΄ β Word π β§ π΅ β Word π) β ((π β (0...πΏ) β§ π β (πΏ...(πΏ + (β―βπ΅)))) β ((π΄ ++ π΅) substr β¨π, πβ©) = ((π΄ substr β¨π, πΏβ©) ++ (π΅ prefix (π β πΏ))))) | ||
Theorem | pfxccat3 14689 | The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by AV, 10-May-2020.) |
β’ πΏ = (β―βπ΄) β β’ ((π΄ β Word π β§ π΅ β Word π) β ((π β (0...π) β§ π β (0...(πΏ + (β―βπ΅)))) β ((π΄ ++ π΅) substr β¨π, πβ©) = if(π β€ πΏ, (π΄ substr β¨π, πβ©), if(πΏ β€ π, (π΅ substr β¨(π β πΏ), (π β πΏ)β©), ((π΄ substr β¨π, πΏβ©) ++ (π΅ prefix (π β πΏ))))))) | ||
Theorem | swrdccat 14690 | The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.) |
β’ πΏ = (β―βπ΄) β β’ ((π΄ β Word π β§ π΅ β Word π) β ((π β (0...π) β§ π β (0...(πΏ + (β―βπ΅)))) β ((π΄ ++ π΅) substr β¨π, πβ©) = ((π΄ substr β¨π, if(π β€ πΏ, π, πΏ)β©) ++ (π΅ substr β¨if(0 β€ (π β πΏ), (π β πΏ), 0), (π β πΏ)β©)))) | ||
Theorem | pfxccatpfx1 14691 | A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020.) |
β’ πΏ = (β―βπ΄) β β’ ((π΄ β Word π β§ π΅ β Word π β§ π β (0...πΏ)) β ((π΄ ++ π΅) prefix π) = (π΄ prefix π)) | ||
Theorem | pfxccatpfx2 14692 | A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020.) |
β’ πΏ = (β―βπ΄) & β’ π = (β―βπ΅) β β’ ((π΄ β Word π β§ π΅ β Word π β§ π β ((πΏ + 1)...(πΏ + π))) β ((π΄ ++ π΅) prefix π) = (π΄ ++ (π΅ prefix (π β πΏ)))) | ||
Theorem | pfxccat3a 14693 | A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by AV, 10-May-2020.) |
β’ πΏ = (β―βπ΄) & β’ π = (β―βπ΅) β β’ ((π΄ β Word π β§ π΅ β Word π) β (π β (0...(πΏ + π)) β ((π΄ ++ π΅) prefix π) = if(π β€ πΏ, (π΄ prefix π), (π΄ ++ (π΅ prefix (π β πΏ)))))) | ||
Theorem | swrdccat3blem 14694 | Lemma for swrdccat3b 14695. (Contributed by AV, 30-May-2018.) |
β’ πΏ = (β―βπ΄) β β’ ((((π΄ β Word π β§ π΅ β Word π) β§ π β (0...(πΏ + (β―βπ΅)))) β§ (πΏ + (β―βπ΅)) β€ πΏ) β if(πΏ β€ π, (π΅ substr β¨(π β πΏ), (β―βπ΅)β©), ((π΄ substr β¨π, πΏβ©) ++ π΅)) = (π΄ substr β¨π, (πΏ + (β―βπ΅))β©)) | ||
Theorem | swrdccat3b 14695 | A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 30-May-2018.) (Proof shortened by AV, 14-Oct-2022.) |
β’ πΏ = (β―βπ΄) β β’ ((π΄ β Word π β§ π΅ β Word π) β (π β (0...(πΏ + (β―βπ΅))) β ((π΄ ++ π΅) substr β¨π, (πΏ + (β―βπ΅))β©) = if(πΏ β€ π, (π΅ substr β¨(π β πΏ), (β―βπ΅)β©), ((π΄ substr β¨π, πΏβ©) ++ π΅)))) | ||
Theorem | pfxccatid 14696 | A prefix of a concatenation of length of the first concatenated word is the first word itself. (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 10-May-2020.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ π = (β―βπ΄)) β ((π΄ ++ π΅) prefix π) = π΄) | ||
Theorem | ccats1pfxeqbi 14697 | A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. (Contributed by AV, 24-Oct-2018.) (Revised by AV, 10-May-2020.) |
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π prefix (β―βπ)) β π = (π ++ β¨β(lastSβπ)ββ©))) | ||
Theorem | swrdccatin1d 14698 | The subword of a concatenation of two words within the first of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.) |
β’ (π β (β―βπ΄) = πΏ) & β’ (π β (π΄ β Word π β§ π΅ β Word π)) & β’ (π β π β (0...π)) & β’ (π β π β (0...πΏ)) β β’ (π β ((π΄ ++ π΅) substr β¨π, πβ©) = (π΄ substr β¨π, πβ©)) | ||
Theorem | swrdccatin2d 14699 | The subword of a concatenation of two words within the second of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.) |
β’ (π β (β―βπ΄) = πΏ) & β’ (π β (π΄ β Word π β§ π΅ β Word π)) & β’ (π β π β (πΏ...π)) & β’ (π β π β (πΏ...(πΏ + (β―βπ΅)))) β β’ (π β ((π΄ ++ π΅) substr β¨π, πβ©) = (π΅ substr β¨(π β πΏ), (π β πΏ)β©)) | ||
Theorem | pfxccatin12d 14700 | The subword of a concatenation of two words within both of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by AV, 10-May-2020.) |
β’ (π β (β―βπ΄) = πΏ) & β’ (π β (π΄ β Word π β§ π΅ β Word π)) & β’ (π β π β (0...πΏ)) & β’ (π β π β (πΏ...(πΏ + (β―βπ΅)))) β β’ (π β ((π΄ ++ π΅) substr β¨π, πβ©) = ((π΄ substr β¨π, πΏβ©) ++ (π΅ prefix (π β πΏ)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |