2. St: Type
3. C: {C:{l:((St
Alph*)*)| ||l|| > 0 }| 
i:
(||C||-1). ||2of(C[i])|| > 0 }4. a: Alph
5. q: St
(map(
c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ])
{C:{l:((StAlph*)*)| ||l|| > 0 }| i:(||C||-1). ||2of(C[i])|| > 0 } Alph,St:Type, C:NComp(Alph;St), a:Alph, q:St. C+[a;q] NComp(Alph;St)| 1 | 1. Alph: Type 2. St: Type 3. C: {C:{l:((St Alph*)*)| ||l|| > 0 }| i:(||C||-1). ||2of(C[i])|| > 0 }4. a: Alph 5. q: St (map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ])
{C:{l:((StAlph*)*)| ||l|| > 0 }| i:(||C||-1). ||2of(C[i])|| > 0 } |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |