Nuprl Definition : free-group
free-group(X) == <free-word(X), λw,w'. tt, λw,w'. tt, λw,w'. w + w', 0, λw.free-word-inv(w)>
Definitions occuring in Statement :
free-word-inv: free-word-inv(w),
free-0: 0,
free-append: w + w',
free-word: free-word(X),
btrue: tt,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
free-word: free-word(X),
btrue: tt,
free-append: w + w',
pair: <a, b>,
free-0: 0,
lambda: λx.A[x]
FDL editor aliases :
free-group
Latex:
free-group(X) == <free-word(X), \mlambda{}w,w'. tt, \mlambda{}w,w'. tt, \mlambda{}w,w'. w + w', 0, \mlambda{}w.free-word-inv(w)>
Date html generated:
2020_05_20-AM-08_22_42
Last ObjectModification:
2017_01_14-PM-07_22_01
Theory : free!groups
Home
Index