Nuprl Definition : permutation-s-group
Perm(rv) ==
mk-s-group(permutation-ss(rv);
<λx.x, λx.x>;
λfg.let f,g = fg
in <g, f>;
λfg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g>;
TERMOF{permutation-s-group-sep-or:o, 1:l, 1:l} rv sepw;
λx,y,d. case d of inl(asep) => inr asep | inr(asep) => inl asep)
Definitions occuring in Statement :
permutation-ss: permutation-ss(ss),
mk-s-group: mk-s-group(ss; e; i; o; sep; invsep),
compose: f o g,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
Definitions occuring in definition :
mk-s-group: mk-s-group(ss; e; i; o; sep; invsep),
permutation-ss: permutation-ss(ss),
spread: spread def,
pair: <a, b>,
compose: f o g,
apply: f a,
permutation-s-group-sep-or,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
TermOfs occuring in Definition :
permutation-s-group-sep-or
FDL editor aliases :
permutation-s-group
Latex:
Perm(rv) ==
mk-s-group(permutation-ss(rv);
<\mlambda{}x.x, \mlambda{}x.x>
\mlambda{}fg.let f,g = fg
in <g, f>
\mlambda{}fg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g>
TERMOF\{permutation-s-group-sep-or:o, 1:l, 1:l\} rv sepw;
\mlambda{}x,y,d. case d of inl(asep) => inr asep | inr(asep) => inl asep)
Date html generated:
2017_10_02-PM-03_25_20
Last ObjectModification:
2017_07_12-PM-01_54_38
Theory : constructive!algebra
Home
Index