Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-frsmgrp Unicode version

Definition df-frsmgrp 25493
 Description: Definition of a free semigroup. The definition is somewhat cryptic. Let's say it guarantees the elements of the semigroup can be decomposed into elementary components and that the decomposition is unique. As a consequence you define the elements of the semigroup with nice recursive function by giving the value for every elementary component and the recursive equation . This is not true in every semigroup. For intance if you take the semigroup of strings generated by the elementary components "ab", "c", "a", "bc", the string "abc" is equal to "ab" "c" or to "a" "bc" and those beautiful recursive function can't exist. (See a nice explanation in Gallier p. 20.) Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-frsmgrp
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-frsmgrp
StepHypRef Expression
1 cfsm 25492 . 2
2 vg . . . . . 6
32cv 1631 . . . . 5
4 vx . . . . . . . 8
54cv 1631 . . . . . . 7
63, 5cop 3656 . . . . . 6
7 csbsgrg 25488 . . . . . 6
86, 7cfv 5271 . . . . 5
93, 8wceq 1632 . . . 4
10 vu . . . . . . . . . 10
1110cv 1631 . . . . . . . . 9
1211, 5cres 4707 . . . . . . . 8
13 va . . . . . . . . 9
1413cv 1631 . . . . . . . 8
1512, 14wceq 1632 . . . . . . 7
16 vh . . . . . . . . . 10
1716cv 1631 . . . . . . . . 9
183, 17cop 3656 . . . . . . . 8
19 csmhom 25490 . . . . . . . 8
2018, 19cfv 5271 . . . . . . 7
2115, 10, 20wrex 2557 . . . . . 6
2217cdm 4705 . . . . . . . 8
2322cdm 4705 . . . . . . 7
24 cmap 6788 . . . . . . 7
2523, 5, 24co 5874 . . . . . 6
2621, 13, 25wral 2556 . . . . 5
27 csem 21013 . . . . 5
2826, 16, 27wral 2556 . . . 4
299, 28wa 358 . . 3
3029, 2, 4copab 4092 . 2
311, 30wceq 1632 1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator