P. 111 of Theorem List - Intuitionistic Logic Explorer

Type

Label

Description

Statement

4.7  Words over a set

This section is about words (or strings) over a set (alphabet) defined as finite sequences of symbols (or characters) being elements of the alphabet. Although it is often required that the underlying set/alphabet be nonempty, finite and not a proper class, these restrictions are not made in the current definition df-word 11002. Note that the empty word ∅ (i.e., the empty set) is the only word over an empty alphabet, see 0wrd0 11027. The set Word 𝑆 of words over 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word. Besides the definition of words themselves, several operations on words are defined in this section:

Name	Reference	Explanation	Example	Remarks
Length (or size) of a word	df-ihash 10928: (♯‘𝑊)	Operation which determines the number of the symbols within the word.	𝑊:(0..^𝑁)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 𝑁	This is not a special definition for words, but for arbitrary sets.
First symbol of a word	df-fv 5284: (𝑊‘0)	Operation which extracts the first symbol of a word. The result is the symbol at the first place in the sequence representing the word.	𝑊:(0..^1)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (𝑊‘0) ∈ 𝑆	This is not a special definition for words, but for arbitrary functions with a half-open range of nonnegative integers as domain.
Last symbol of a word	df-lsw 11046: (lastS‘𝑊)	Operation which extracts the last symbol of a word. The result is the symbol at the last place in the sequence representing the word.	𝑊:(0..^3)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (lastS‘𝑊) = (𝑊‘2)	Note that the index of the last symbol is less by 1 than the length of the word.
Subword (or substring) of a word	df-substr 11107: (𝑊 substr ⟨𝐼, 𝐽⟩)	Operation which extracts a portion of a word. The result is a consecutive, reindexed part of the sequence representing the word.	𝑊:(0..^3)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (𝑊 substr ⟨1, 2⟩) ∈ Word 𝑆 ∧ (♯‘(𝑊 substr ⟨1, 2⟩)) = 1	Note that the last index of the range defining the subword is greater by 1 than the index of the last symbol of the subword in the sequence of the original word.
Concatenation of two words	df-concat 11055: (𝑊 ++ 𝑈)	Operation combining two words to one new word. The result is a combined, reindexed sequence build from the sequences representing the two words.	(𝑊 ∈ Word 𝑆 ∧ 𝑈 ∈ Word 𝑆) → (♯‘(𝑊 ++ 𝑈)) = ((♯‘𝑊) + (♯‘𝑈))	Note that the index of the first symbol of the second concatenated word is the length of the first word in the concatenation.
Singleton word	df-s1 11078: ⟨“𝑆”⟩	Constructor building a word of length 1 from a symbol.	(♯‘⟨“𝑆”⟩) = 1

Conventions:

• Words are usually represented by class variable 𝑊, or if two words are involved, by 𝑊 and 𝑈 or by 𝐴 and 𝐵.
• The alphabets are usually represented by class variable 𝑉 (because any arbitrary set can be an alphabet), sometimes also by 𝑆 (especially as codomain of the function representing a word, because the alphabet is the set of symbols).
• The symbols are usually represented by class variables 𝑆 or 𝐴, or if two symbols are involved, by 𝑆 and 𝑇 or by 𝐴 and 𝐵.
• The indices of the sequence representing a word are usually represented by class variable 𝐼, if two indices are involved (especially for subwords) by 𝐼 and 𝐽, or by 𝑀 and 𝑁.
• The length of a word is usually represented by class variables 𝑁 or 𝐿.
• The number of positions by which to cyclically shift a word is usually represented by class variables 𝑁 or 𝐿.

4.7.1  Definitions and basic theorems

Syntax

cword 11001

Syntax for the Word operator.

class Word 𝑆

Definition

df-word 11002*

Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) 𝑆. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of ℕ₀ so that two words with the same symbols in the same order be equal. The set Word 𝑆 is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word 𝑆 equipped with concatenation is the free monoid over 𝑆, and the monoid unit is the empty word. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ₀ 𝑤:(0..^𝑙)⟶𝑆}

Theorem

iswrd 11003*

Property of being a word over a set with an existential quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)

⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆)

Theorem

wrdval 11004*

Value of the set of words over a set. (Contributed by Stefan O'Rear, 10-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ (𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ₀ (𝑆 ↑_𝑚 (0..^𝑙)))

Theorem

lencl 11005

The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015.)

⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ₀)

Theorem

iswrdinn0 11006

A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.)

⊢ ((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℕ₀) → 𝑊 ∈ Word 𝑆)

Theorem

wrdf 11007

A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Theorem

iswrdiz 11008

A zero-based sequence is a word. In iswrdinn0 11006 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.)

⊢ ((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℤ) → 𝑊 ∈ Word 𝑆)

Theorem

wrddm 11009

The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020.)

⊢ (𝑊 ∈ Word 𝑆 → dom 𝑊 = (0..^(♯‘𝑊)))

Theorem

sswrd 11010

The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)

⊢ (𝑆 ⊆ 𝑇 → Word 𝑆 ⊆ Word 𝑇)

Theorem

snopiswrd 11011

A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018.) (Proof shortened by AV, 18-Apr-2021.)

⊢ (𝑆 ∈ 𝑉 → {⟨0, 𝑆⟩} ∈ Word 𝑉)

Theorem

wrdexg 11012

The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by JJ, 18-Nov-2022.)

⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V)

Theorem

wrdexb 11013

The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)

⊢ (𝑆 ∈ V ↔ Word 𝑆 ∈ V)

Theorem

wrdexi 11014

The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.)

⊢ 𝑆 ∈ V    ⇒   ⊢ Word 𝑆 ∈ V

Theorem

wrdsymbcl 11015

A symbol within a word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝐼) ∈ 𝑉)

Theorem

wrdfn 11016

A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊 Fn (0..^(♯‘𝑊)))

Theorem

wrdv 11017

A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) (Proof shortened by JJ, 18-Nov-2022.)

⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V)

Theorem

wrdlndm 11018

The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021.) (Proof shortened by JJ, 18-Nov-2022.)

⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∉ dom 𝑊)

Theorem

iswrdsymb 11019*

An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021.)

⊢ ((𝑊 ∈ Word V ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ∈ 𝑉) → 𝑊 ∈ Word 𝑉)

Theorem

wrdfin 11020

A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015.) (Proof shortened by AV, 18-Nov-2018.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin)

Theorem

lennncl 11021

The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.)

⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)

Theorem

wrdffz 11022

A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆)

Theorem

wrdeq 11023

Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇)

Theorem

wrdeqi 11024

Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.)

⊢ 𝑆 = 𝑇    ⇒   ⊢ Word 𝑆 = Word 𝑇

Theorem

iswrddm0 11025

A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.)

⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆)

Theorem

wrd0 11026

The empty set is a word (the empty word, frequently denoted ε in this context). This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 13-May-2020.)

⊢ ∅ ∈ Word 𝑆

Theorem

0wrd0 11027

The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)

⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅)

Theorem

wrdsymb 11028

A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.)

⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆))))

Theorem

nfwrd 11029

Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ Ⅎ𝑥𝑆    ⇒   ⊢ Ⅎ𝑥Word 𝑆

Theorem

csbwrdg 11030*

Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)

⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆)

Theorem

wrdnval 11031*

Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Proof shortened by AV, 13-May-2020.)

⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ₀) → {𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁} = (𝑉 ↑_𝑚 (0..^𝑁)))

Theorem

wrdmap 11032

Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)

⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ₀) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑_𝑚 (0..^𝑁))))

Theorem

wrdsymb0 11033

A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018.) (Proof shortened by AV, 2-May-2020.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐼 < 0 ∨ (♯‘𝑊) ≤ 𝐼) → (𝑊‘𝐼) = ∅))

Theorem

wrdlenge1n0 11034

A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)

⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊)))

Theorem

len0nnbi 11035

The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.)

⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ))

Theorem

wrdlenge2n0 11036

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 11037

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 11038*

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 11039

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 11040

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 11041*

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 11042*

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

wrdred1 11043

A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)

⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆)

Theorem

wrdred1hash 11044

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))

4.7.2  Last symbol of a word

Syntax

clsw 11045

Extend class notation with the Last Symbol of a word.

class lastS

Definition

df-lsw 11046

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

lswwrd 11047

Extract the last symbol of a word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Jim Kingdon, 18-Dec-2025.)

⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Theorem

lsw0 11048

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 11049

The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)

⊢ (lastS‘∅) = ∅

Theorem

lsw1 11050

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 11051

Closure of the last symbol: the last symbol of a nonempty word belongs to the alphabet for the word. (Contributed by AV, 2-Aug-2018.) (Proof shortened by AV, 29-Apr-2020.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (lastS‘𝑊) ∈ 𝑉)

Theorem

lswex 11052

Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11049 or lswcl 11051 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.)

⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) ∈ V)

Theorem

lswlgt0cl 11053

The last symbol of a nonempty word is an 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‘𝑊) ∈ 𝑉)

4.7.3  Concatenations of words

Syntax

cconcat 11054

Syntax for the concatenation operator.

class ++

Definition

df-concat 11055*

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

ccatfvalfi 11056*

Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ ((𝑆 ∈ Fin ∧ 𝑇 ∈ Fin) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))))

Theorem

ccatcl 11057

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

ccatclab 11058

The concatenation of words over two sets is a word over the union of those sets. (Contributed by Jim Kingdon, 19-Dec-2025.)

⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word (𝐴 ∪ 𝐵))

Theorem

ccatlen 11059

The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.)

⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇)))

Theorem

ccat0 11060

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 11061

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 11062

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 11063

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 11064

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 11065

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 11066

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 11067

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 11068

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 11069

The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.)

⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0))

Theorem

ccatlid 11070

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 11071

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 11072

Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈)))

Theorem

ccatrn 11073

The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇))

Theorem

ccatidid 11074

Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)

⊢ (∅ ++ ∅) = ∅

Theorem

lswccatn0lsw 11075

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 11076

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‘𝑊))

4.7.4  Singleton words

Syntax

cs1 11077

Syntax for the singleton word constructor.

class ⟨“𝐴”⟩

Definition

df-s1 11078

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 11085, and not, as maybe expected, the empty word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

Theorem

s1val 11079

Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ (𝐴 ∈ 𝑉 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})

Theorem

s1rn 11080

The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)

⊢ (𝐴 ∈ 𝑉 → ran ⟨“𝐴”⟩ = {𝐴})

Theorem

s1eq 11081

Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)

Theorem

s1eqd 11082

Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)

Theorem

s1cl 11083

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 11084

A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ ∈ Word 𝐵)

Theorem

s1prc 11085

Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)

⊢ (¬ 𝐴 ∈ V → ⟨“𝐴”⟩ = ⟨“∅”⟩)

Theorem

s1leng 11086

Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ (𝐴 ∈ 𝑉 → (♯‘⟨“𝐴”⟩) = 1)

Theorem

s1dmg 11087

The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)

⊢ (𝐴 ∈ 𝑆 → dom ⟨“𝐴”⟩ = {0})

Theorem

s1fv 11088

Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)

Theorem

lsws1 11089

The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)

⊢ (𝐴 ∈ 𝑉 → (lastS‘⟨“𝐴”⟩) = 𝐴)

Theorem

eqs1 11090

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 11091*

A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.)

⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = ⟨“𝑠”⟩)

Theorem

wrdl1s1 11092

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 11093

The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (⟨“𝑆”⟩ = ⟨“𝑇”⟩ ↔ 𝑆 = 𝑇))

4.7.5  Concatenations with singleton words

Theorem

ccatws1cl 11094

The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)

Theorem

ccat2s1cl 11095

The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)

⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩) ∈ Word 𝑉)

Theorem

ccatws1leng 11096

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

ccatws1lenp1bg 11097

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 𝑉 ∧ 𝑋 ∈ 𝑌 ∧ 𝑁 ∈ ℕ₀) → ((♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) ↔ (♯‘𝑊) = 𝑁))

Theorem

ccatw2s1cl 11098

The concatenation of a word with two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) ∈ Word 𝑉)

Theorem

ccats1val1g 11099

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 11100

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 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ 𝐼 = (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑆”⟩)‘𝐼) = 𝑆)