ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-word Unicode version

Definition df-word 10905
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 equipped with concatenation is the free monoid over  S, 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.)
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
StepHypRef Expression
1 cS . . 3  class  S
21cword 10904 . 2  class Word  S
3 cc0 7862 . . . . . 6  class  0
4 vl . . . . . . 7  setvar  l
54cv 1363 . . . . . 6  class  l
6 cfzo 10198 . . . . . 6  class ..^
73, 5, 6co 5910 . . . . 5  class  ( 0..^ l )
8 vw . . . . . 6  setvar  w
98cv 1363 . . . . 5  class  w
107, 1, 9wf 5242 . . . 4  wff  w : ( 0..^ l ) --> S
11 cn0 9230 . . . 4  class  NN0
1210, 4, 11wrex 2473 . . 3  wff  E. l  e.  NN0  w : ( 0..^ l ) --> S
1312, 8cab 2179 . 2  class  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
142, 13wceq 1364 1  wff Word  S  =  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
Colors of variables: wff set class
This definition is referenced by:  iswrd  10906  wrdval  10907  nfwrd  10932  csbwrdg  10933
  Copyright terms: Public domain W3C validator