Nuprl Definition : free-word-inv

free-word-inv(w) ==  map(λ of inl(a) => inr a  inr(a) => inl a;rev(w))

Definitions occuring in Statement :  reverse: rev(as) map: map(f;as) lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x
Definitions occuring in definition :  reverse: rev(as) inl: inl x inr: inr  decide: case of inl(x) => s[x] inr(y) => t[y] lambda: λx.A[x] map: map(f;as)
FDL editor aliases :  free-word-inv

free-word-inv(w)  ==    map(\mlambda{}  x  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a;rev(w))

Date html generated: 2017_01_19-PM-02_50_28
Last ObjectModification: 2017_01_14-PM-07_39_48

Theory : free!groups

Home Index