Home | Metamath
Proof Explorer Theorem List (p. 146 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 | pfxfn 14501 | Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (π prefix πΏ) Fn (0..^πΏ)) | ||
Theorem | pfxfv 14502 | 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 14503 | Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.) |
β’ ((π β Word π΄ β§ πΏ β (0...(β―βπ))) β (β―β(π prefix πΏ)) = πΏ) | ||
Theorem | pfxid 14504 | 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 14505 | 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 14506 | 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 14507 | 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 6873). (Contributed by AV, 3-May-2020.) |
β’ ((π β Word π β§ πΏ β β0 β§ (β―βπ) < πΏ) β (π prefix πΏ) = β ) | ||
Theorem | pfxnd0 14508 | 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 6873). (Contributed by AV, 3-Dec-2022.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (π prefix πΏ) = β ) | ||
Theorem | pfxwrdsymb 14509 | 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 14510 | 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 14511 | 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 14512 | 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 14513 | 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 14514 | 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 14515 | 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 14516* | 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 14517 | 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 14518 | 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 14519 | 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 14520* | 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 14521 | 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 14522 | 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 14523 | 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 14524 | Lemma for swrdswrd 14525. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
β’ (((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β§ (πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π)))) β (π β Word π β§ (π + πΎ) β (0...(π + πΏ)) β§ (π + πΏ) β (0...(β―βπ)))) | ||
Theorem | swrdswrd 14525 | 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 14526 | 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 14527 | 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 14528 | 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 14529 | 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 14530 | 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 14531 | 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 14532 | 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 14533 | 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 14534 | 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 14535* | 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 14536 | An opth 5432-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 14537 | An opth 5432-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ (((π΄ β Word π β§ π΅ β Word π) β§ (πΆ β Word π β§ π· β Word π) β§ (β―βπ΅) = (β―βπ·)) β ((π΄ ++ π΅) = (πΆ ++ π·) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | ccatlcan 14538 | Concatenation of words is left-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ πΆ β Word π) β ((πΆ ++ π΄) = (πΆ ++ π΅) β π΄ = π΅)) | ||
Theorem | ccatrcan 14539 | Concatenation of words is right-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ πΆ β Word π) β ((π΄ ++ πΆ) = (π΅ ++ πΆ) β π΄ = π΅)) | ||
Theorem | wrdeqs1cat 14540 | 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 14541 | 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 14542* | 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 14543* | 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 14544 | 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 14545 | 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 14546 | Lemma 4 for pfxccatin12 14553. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.) |
β’ ((πΏ β β0 β§ π β β0 β§ π β β€) β ((πΎ β (0..^(π β π)) β§ Β¬ πΎ β (0..^(πΏ β π))) β πΎ β ((πΏ β π)..^((πΏ β π) + (π β πΏ))))) | ||
Theorem | pfxccatin12lem2a 14547 | Lemma for pfxccatin12lem2 14551. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
β’ ((π β (0...πΏ) β§ π β (πΏ...π)) β ((πΎ β (0..^(π β π)) β§ Β¬ πΎ β (0..^(πΏ β π))) β (πΎ + π) β (πΏ..^π))) | ||
Theorem | pfxccatin12lem1 14548 | Lemma 1 for pfxccatin12 14553. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.) |
β’ ((π β (0...πΏ) β§ π β (πΏ...π)) β ((πΎ β (0..^(π β π)) β§ Β¬ πΎ β (0..^(πΏ β π))) β (πΎ β (πΏ β π)) β (0..^(π β πΏ)))) | ||
Theorem | swrdccatin2 14549 | 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 14550 | Lemma for pfxccatin12lem2 14551 and pfxccatin12lem3 14552. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
β’ πΏ = (β―βπ΄) β β’ (((π΄ β Word π β§ π΅ β Word π) β§ (π β (0...πΏ) β§ π β (πΏ...(πΏ + (β―βπ΅))))) β ((π΄ ++ π΅) β Word π β§ π β (0...π) β§ π β (0...(β―β(π΄ ++ π΅))))) | ||
Theorem | pfxccatin12lem2 14551 | Lemma 2 for pfxccatin12 14553. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.) |
β’ πΏ = (β―βπ΄) β β’ (((π΄ β Word π β§ π΅ β Word π) β§ (π β (0...πΏ) β§ π β (πΏ...(πΏ + (β―βπ΅))))) β ((πΎ β (0..^(π β π)) β§ Β¬ πΎ β (0..^(πΏ β π))) β (((π΄ ++ π΅) substr β¨π, πβ©)βπΎ) = ((π΅ prefix (π β πΏ))β(πΎ β (β―β(π΄ substr β¨π, πΏβ©)))))) | ||
Theorem | pfxccatin12lem3 14552 | Lemma 3 for pfxccatin12 14553. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
β’ πΏ = (β―βπ΄) β β’ (((π΄ β Word π β§ π΅ β Word π) β§ (π β (0...πΏ) β§ π β (πΏ...(πΏ + (β―βπ΅))))) β ((πΎ β (0..^(π β π)) β§ πΎ β (0..^(πΏ β π))) β (((π΄ ++ π΅) substr β¨π, πβ©)βπΎ) = ((π΄ substr β¨π, πΏβ©)βπΎ))) | ||
Theorem | pfxccatin12 14553 | 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 14554 | 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 14555 | 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 14556 | 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 14557 | 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 14558 | 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 14559 | Lemma for swrdccat3b 14560. (Contributed by AV, 30-May-2018.) |
β’ πΏ = (β―βπ΄) β β’ ((((π΄ β Word π β§ π΅ β Word π) β§ π β (0...(πΏ + (β―βπ΅)))) β§ (πΏ + (β―βπ΅)) β€ πΏ) β if(πΏ β€ π, (π΅ substr β¨(π β πΏ), (β―βπ΅)β©), ((π΄ substr β¨π, πΏβ©) ++ π΅)) = (π΄ substr β¨π, (πΏ + (β―βπ΅))β©)) | ||
Theorem | swrdccat3b 14560 | 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 14561 | 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 14562 | 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 14563 | 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 14564 | 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 14565 | 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 (π β πΏ)))) | ||
Theorem | reuccatpfxs1lem 14566* | Lemma for reuccatpfxs1 14567. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 9-May-2020.) |
β’ (((π β Word π β§ π β π) β§ βπ β π ((π ++ β¨βπ ββ©) β π β π = π ) β§ βπ₯ β π (π₯ β Word π β§ (β―βπ₯) = ((β―βπ) + 1))) β (π = (π prefix (β―βπ)) β π = (π ++ β¨βπββ©))) | ||
Theorem | reuccatpfxs1 14567* | There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Revised by AV, 13-Oct-2022.) |
β’ β²π£π β β’ ((π β Word π β§ βπ₯ β π (π₯ β Word π β§ (β―βπ₯) = ((β―βπ) + 1))) β (β!π£ β π (π ++ β¨βπ£ββ©) β π β β!π₯ β π π = (π₯ prefix (β―βπ)))) | ||
Theorem | reuccatpfxs1v 14568* | There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Revised by AV, 10-May-2022.) (Proof shortened by AV, 13-Oct-2022.) |
β’ ((π β Word π β§ βπ₯ β π (π₯ β Word π β§ (β―βπ₯) = ((β―βπ) + 1))) β (β!π£ β π (π ++ β¨βπ£ββ©) β π β β!π₯ β π π = (π₯ prefix (β―βπ)))) | ||
Syntax | csplice 14569 | Syntax for the word splicing operator. |
class splice | ||
Definition | df-splice 14570* | Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by AV, 14-Oct-2022.) |
β’ splice = (π β V, π β V β¦ (((π prefix (1st β(1st βπ))) ++ (2nd βπ)) ++ (π substr β¨(2nd β(1st βπ)), (β―βπ )β©))) | ||
Theorem | splval 14571 | Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by AV, 11-May-2020.) (Revised by AV, 15-Oct-2022.) |
β’ ((π β π β§ (πΉ β π β§ π β π β§ π β π)) β (π splice β¨πΉ, π, π β©) = (((π prefix πΉ) ++ π ) ++ (π substr β¨π, (β―βπ)β©))) | ||
Theorem | splcl 14572 | Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Proof shortened by AV, 15-Oct-2022.) |
β’ ((π β Word π΄ β§ π β Word π΄) β (π splice β¨πΉ, π, π β©) β Word π΄) | ||
Theorem | splid 14573 | Splicing a subword for the same subword makes no difference. (Contributed by Stefan O'Rear, 20-Aug-2015.) (Proof shortened by AV, 14-Oct-2022.) |
β’ ((π β Word π΄ β§ (π β (0...π) β§ π β (0...(β―βπ)))) β (π splice β¨π, π, (π substr β¨π, πβ©)β©) = π) | ||
Theorem | spllen 14574 | The length of a splice. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 15-Oct-2022.) |
β’ (π β π β Word π΄) & β’ (π β πΉ β (0...π)) & β’ (π β π β (0...(β―βπ))) & β’ (π β π β Word π΄) β β’ (π β (β―β(π splice β¨πΉ, π, π β©)) = ((β―βπ) + ((β―βπ ) β (π β πΉ)))) | ||
Theorem | splfv1 14575 | Symbols to the left of a splice are unaffected. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 15-Oct-2022.) |
β’ (π β π β Word π΄) & β’ (π β πΉ β (0...π)) & β’ (π β π β (0...(β―βπ))) & β’ (π β π β Word π΄) & β’ (π β π β (0..^πΉ)) β β’ (π β ((π splice β¨πΉ, π, π β©)βπ) = (πβπ)) | ||
Theorem | splfv2a 14576 | Symbols within the replacement region of a splice, expressed using the coordinates of the replacement region. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 15-Oct-2022.) |
β’ (π β π β Word π΄) & β’ (π β πΉ β (0...π)) & β’ (π β π β (0...(β―βπ))) & β’ (π β π β Word π΄) & β’ (π β π β (0..^(β―βπ ))) β β’ (π β ((π splice β¨πΉ, π, π β©)β(πΉ + π)) = (π βπ)) | ||
Theorem | splval2 14577 | Value of a splice, assuming the input word π has already been decomposed into its pieces. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 15-Oct-2022.) |
β’ (π β π΄ β Word π) & β’ (π β π΅ β Word π) & β’ (π β πΆ β Word π) & β’ (π β π β Word π) & β’ (π β π = ((π΄ ++ π΅) ++ πΆ)) & β’ (π β πΉ = (β―βπ΄)) & β’ (π β π = (πΉ + (β―βπ΅))) β β’ (π β (π splice β¨πΉ, π, π β©) = ((π΄ ++ π ) ++ πΆ)) | ||
Syntax | creverse 14578 | Syntax for the word reverse operator. |
class reverse | ||
Definition | df-reverse 14579* | Define an operation which reverses the order of symbols in a word. This operation is also known as "word reversal" and "word mirroring". (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ reverse = (π β V β¦ (π₯ β (0..^(β―βπ )) β¦ (π β(((β―βπ ) β 1) β π₯)))) | ||
Theorem | revval 14580* | Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ (π β π β (reverseβπ) = (π₯ β (0..^(β―βπ)) β¦ (πβ(((β―βπ) β 1) β π₯)))) | ||
Theorem | revcl 14581 | The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ (π β Word π΄ β (reverseβπ) β Word π΄) | ||
Theorem | revlen 14582 | The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ (π β Word π΄ β (β―β(reverseβπ)) = (β―βπ)) | ||
Theorem | revfv 14583 | Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ ((π β Word π΄ β§ π β (0..^(β―βπ))) β ((reverseβπ)βπ) = (πβ(((β―βπ) β 1) β π))) | ||
Theorem | rev0 14584 | The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ (reverseββ ) = β | ||
Theorem | revs1 14585 | Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (reverseββ¨βπββ©) = β¨βπββ© | ||
Theorem | revccat 14586 | Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ ((π β Word π΄ β§ π β Word π΄) β (reverseβ(π ++ π)) = ((reverseβπ) ++ (reverseβπ))) | ||
Theorem | revrev 14587 | Reversal is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ (π β Word π΄ β (reverseβ(reverseβπ)) = π) | ||
Syntax | creps 14588 | Extend class notation with words consisting of one repeated symbol. |
class repeatS | ||
Definition | df-reps 14589* | Definition to construct a word consisting of one repeated symbol, often called "repeated symbol word" for short in the following. (Contributed by Alexander van der Vekens, 4-Nov-2018.) |
β’ repeatS = (π β V, π β β0 β¦ (π₯ β (0..^π) β¦ π )) | ||
Theorem | reps 14590* | Construct a function mapping a half-open range of nonnegative integers to a constant. (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0) β (π repeatS π) = (π₯ β (0..^π) β¦ π)) | ||
Theorem | repsundef 14591 | A function mapping a half-open range of nonnegative integers with an upper bound not being a nonnegative integer to a constant is the empty set (in the meaning of "undefined"). (Contributed by AV, 5-Nov-2018.) |
β’ (π β β0 β (π repeatS π) = β ) | ||
Theorem | repsconst 14592 | Construct a function mapping a half-open range of nonnegative integers to a constant, see also fconstmpt 5691. (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0) β (π repeatS π) = ((0..^π) Γ {π})) | ||
Theorem | repsf 14593 | The constructed function mapping a half-open range of nonnegative integers to a constant is a function. (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0) β (π repeatS π):(0..^π)βΆπ) | ||
Theorem | repswsymb 14594 | The symbols of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0 β§ πΌ β (0..^π)) β ((π repeatS π)βπΌ) = π) | ||
Theorem | repsw 14595 | A function mapping a half-open range of nonnegative integers to a constant is a word consisting of one symbol repeated several times ("repeated symbol word"). (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0) β (π repeatS π) β Word π) | ||
Theorem | repswlen 14596 | The length of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0) β (β―β(π repeatS π)) = π) | ||
Theorem | repsw0 14597 | The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018.) |
β’ (π β π β (π repeatS 0) = β ) | ||
Theorem | repsdf2 14598* | Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018.) |
β’ ((π β π β§ π β β0) β (π = (π repeatS π) β (π β Word π β§ (β―βπ) = π β§ βπ β (0..^π)(πβπ) = π))) | ||
Theorem | repswsymball 14599* | All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018.) |
β’ ((π β Word π β§ π β π) β (π = (π repeatS (β―βπ)) β βπ β (0..^(β―βπ))(πβπ) = π)) | ||
Theorem | repswsymballbi 14600* | A word is a "repeated symbol word" iff each of its symbols equals the first symbol of the word. (Contributed by AV, 10-Nov-2018.) |
β’ (π β Word π β (π = ((πβ0) repeatS (β―βπ)) β βπ β (0..^(β―βπ))(πβπ) = (πβ0))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |