Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-word Structured version   Visualization version   Unicode version

Definition df-word 12664
 Description: Define the class of words over a set. A word (or 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 so that two words with the same symbols in the same order will be the same. This is sometimes denoted with the Kleene star, although properly speaking that is an operator on languages. (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 ..^
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-word
StepHypRef Expression
1 cS . . 3
21cword 12656 . 2 Word
3 cc0 9539 . . . . . 6
4 vl . . . . . . 7
54cv 1443 . . . . . 6
6 cfzo 11915 . . . . . 6 ..^
73, 5, 6co 6290 . . . . 5 ..^
8 vw . . . . . 6
98cv 1443 . . . . 5
107, 1, 9wf 5578 . . . 4 ..^
11 cn0 10869 . . . 4
1210, 4, 11wrex 2738 . . 3 ..^
1312, 8cab 2437 . 2 ..^
142, 13wceq 1444 1 Word ..^
 Colors of variables: wff setvar class This definition is referenced by:  iswrd  12672  iswrdOLD  12673  wrdval  12674  nfwrd  12695  csbwrdg  12696
 Copyright terms: Public domain W3C validator