P. 113 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11201-11300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	swrdrlen 11201	Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨𝐼, (♯‘𝑊)⟩)) = ((♯‘𝑊) − 𝐼))
Theorem	swrdlen2 11202	Length of an extracted subword. (Contributed by AV, 5-May-2020.)
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (♯‘(𝑆 substr ⟨𝐹, 𝐿⟩)) = (𝐿 − 𝐹))
Theorem	swrdfv2 11203	A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020.)
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr ⟨𝐹, 𝐿⟩)‘(𝑋 − 𝐹)) = (𝑆‘𝑋))
Theorem	swrdwrdsymbg 11204	A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) → (𝑆 substr ⟨𝑀, 𝑁⟩) ∈ Word (𝑆 “ (𝑀..^𝑁)))
Theorem	swrdsb0eq 11205	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 11206	Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)))
Theorem	swrdspsleq 11207*	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 11208	Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 1)⟩) = ⟨“(𝑊‘𝐼)”⟩)
Theorem	swrdlsw 11209	Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr ⟨((♯‘𝑊) − 1), (♯‘𝑊)⟩) = ⟨“(lastS‘𝑊)”⟩)
Theorem	ccatswrd 11210	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 11211	Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr ⟨(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))⟩) = 𝑇)
4.7.7  Prefixes of a word
Syntax	cpfx 11212	Syntax for the prefix operator.
class prefix
Definition	df-pfx 11213*	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	pfxval 11214	Value of a prefix operation. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = (𝑆 substr ⟨0, 𝐿⟩))
Theorem	pfx00g 11215	The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 prefix 0) = ∅)
Theorem	pfx0g 11216	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
⊢ (𝐿 ∈ ℕ0 → (∅ prefix 𝐿) = ∅)
Theorem	fnpfx 11217	The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
⊢ prefix Fn (V × ℕ0)
Theorem	pfxclg 11218	Closure of the prefix extractor. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) ∈ Word 𝐴)
Theorem	pfxclz 11219	Closure of the prefix extractor. This extends pfxclg 11218 from ℕ0 to ℤ (negative lengths are trivial, resulting in the empty word). (Contributed by Jim Kingdon, 8-Jan-2026.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ℤ) → (𝑆 prefix 𝐿) ∈ Word 𝐴)
Theorem	pfxmpt 11220*	Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) = (𝑥 ∈ (0..^𝐿) ↦ (𝑆‘𝑥)))
Theorem	pfxres 11221	Value of the prefix extractor as the restriction of a word. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) = (𝑆 ↾ (0..^𝐿)))
Theorem	pfxf 11222	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 11223	Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) Fn (0..^𝐿))
Theorem	pfxfv 11224	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 11225	Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐿)) = 𝐿)
Theorem	pfxid 11226	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 11227	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 11228	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 11229	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 ndmfvg 5660). (Contributed by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (♯‘𝑊) < 𝐿) → (𝑊 prefix 𝐿) = ∅)
Theorem	pfxwrdsymbg 11230	A prefix of a word is a word over the symbols it consists of. (Contributed by AV, 3-Dec-2022.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) ∈ Word (𝑆 “ (0..^𝐿)))
Theorem	addlenpfx 11231	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 11232	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 11233	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 11234	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 11235	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 11236*	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 11237	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 11238	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 11239	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 11240*	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 11241	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 11242	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 11243	The prefix of length one of a nonempty word expressed as a singleton word. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 prefix 1) = ⟨“(𝑊‘0)”⟩)
4.7.8  Subwords of subwords
Theorem	swrdswrdlem 11244	Lemma for swrdswrd 11245. (Contributed by Alexander van der Vekens, 4-Apr-2018.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊))))
Theorem	swrdswrd 11245	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 11246	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 11247	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 11248	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 11249	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 𝑁))
4.7.9  Subwords and concatenations
Theorem	pfxcctswrd 11250	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 11251	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 11252	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 11253	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 11254	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 11255*	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 11256	An opth 4323-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 11257	An opth 4323-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (♯‘𝐵) = (♯‘𝐷)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	ccatlcan 11258	Concatenation of words is left-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) → ((𝐶 ++ 𝐴) = (𝐶 ++ 𝐵) ↔ 𝐴 = 𝐵))
Theorem	ccatrcan 11259	Concatenation of words is right-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	wrdeqs1cat 11260	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 11261	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 11262*	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 11263*	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 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝜏)
4.7.10  Subwords of concatenations
Theorem	swrdccatfn 11264	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 11265	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 11266	Lemma 4 for pfxccatin12 11273. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.)
⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))))
Theorem	pfxccatin12lem2a 11267	Lemma for pfxccatin12lem2 11271. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋)))
Theorem	pfxccatin12lem1 11268	Lemma 1 for pfxccatin12 11273. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.)
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿))))
Theorem	swrdccatin2 11269	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 11270	Lemma for pfxccatin12lem2 11271 and pfxccatin12lem3 11272. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
⊢ 𝐿 = (♯‘𝐴)    ⇒   ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))))
Theorem	pfxccatin12lem2 11271	Lemma 2 for pfxccatin12 11273. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.)
⊢ 𝐿 = (♯‘𝐴)    ⇒   ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝐾 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))))
Theorem	pfxccatin12lem3 11272	Lemma 3 for pfxccatin12 11273. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
⊢ 𝐿 = (♯‘𝐴)    ⇒   ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝐾)))
Theorem	pfxccatin12 11273	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 11274	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 11275	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 11276	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 11277	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 11278	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 11279	Lemma for swrdccat3b 11280. (Contributed by AV, 30-May-2018.)
⊢ 𝐿 = (♯‘𝐴)    ⇒   ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))
Theorem	swrdccat3b 11280	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 11281	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 11282	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 11283	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 11284	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 11285	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 11286*	Lemma for reuccatpfxs1 11287. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 9-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ ∀𝑠 ∈ 𝑉 ((𝑊 ++ ⟨“𝑠”⟩) ∈ 𝑋 → 𝑆 = 𝑠) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑊) + 1))) → (𝑊 = (𝑈 prefix (♯‘𝑊)) → 𝑈 = (𝑊 ++ ⟨“𝑆”⟩)))
Theorem	reuccatpfxs1 11287*	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 11288*	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 (♯‘𝑊))))
4.7.11  Longer string literals
Syntax	cs2 11289	Syntax for the length 2 word constructor.
class ⟨“𝐴𝐵”⟩
Syntax	cs3 11290	Syntax for the length 3 word constructor.
class ⟨“𝐴𝐵𝐶”⟩
Syntax	cs4 11291	Syntax for the length 4 word constructor.
class ⟨“𝐴𝐵𝐶𝐷”⟩
Syntax	cs5 11292	Syntax for the length 5 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸”⟩
Syntax	cs6 11293	Syntax for the length 6 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩
Syntax	cs7 11294	Syntax for the length 7 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩
Syntax	cs8 11295	Syntax for the length 8 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩
Definition	df-s2 11296	Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Definition	df-s3 11297	Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Definition	df-s4 11298	Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Definition	df-s5 11299	Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸”⟩)
Definition	df-s6 11300	Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹”⟩)