Nuprl Definition : free-word-inv
free-word-inv(w) == map(λx.case x 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 b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
Definitions occuring in definition :
reverse: rev(as),
inl: inl x,
inr: inr x ,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
lambda: λx.A[x],
map: map(f;as)
FDL editor aliases :
free-word-inv
Latex:
free-word-inv(w) == map(\mlambda{}x.case 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