Definition df-word 13299

Description: 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) S. Definition in section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of NN0 so that two words with the same symbols in the same order be equal. The set Word S 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 S is the free monoid over S, where the monoid law is concatenation and the monoid unit is the empty word (see frmdval 17388). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-word	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }

Distinct variable group:   w, l, S

Detailed syntax breakdown of Definition df-word

Step	Hyp	Ref	Expression
1		cS	. . 3 class S
2	1	cword 13291	. 2 class Word S
3		cc0 9936	. . . . . 6 class 0
4		vl	. . . . . . 7 setvar l
5	4	cv 1482	. . . . . 6 class l
6		cfzo 12465	. . . . . 6 class ..^
7	3, 5, 6	co 6650	. . . . 5 class ( 0..^ l )
8		vw	. . . . . 6 setvar w
9	8	cv 1482	. . . . 5 class w
10	7, 1, 9	wf 5884	. . . 4 wff w : ( 0..^ l ) --> S
11		cn0 11292	. . . 4 class NN0
12	10, 4, 11	wrex 2913	. . 3 wff E. l e. NN0 w : ( 0..^ l ) --> S
13	12, 8	cab 2608	. 2 class { w | E. l e. NN0 w : ( 0..^ l ) --> S }
14	2, 13	wceq 1483	1 wff Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }

This definition is referenced by:  iswrd  13307  wrdval  13308  nfwrd  13333  csbwrdg  13334