Nuprl Definition : unshuffle
unshuffle(L) == fix((λunshuffle,L. if ||L|| <z 2 then [] else [<hd(L), hd(tl(L))> / (unshuffle tl(tl(L)))] fi )) L
Definitions occuring in Statement :
hd: hd(l),
length: ||as||,
tl: tl(l),
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
length: ||as||,
natural_number: $n,
nil: [],
cons: [a / b],
pair: <a, b>,
hd: hd(l),
apply: f a,
tl: tl(l)
FDL editor aliases :
unshuffle
Latex:
unshuffle(L) ==
fix((\mlambda{}unshuffle,L. if ||L|| <z 2 then [] else [<hd(L), hd(tl(L))> / (unshuffle tl(tl(L)))] fi )) L
Date html generated:
2016_05_14-PM-03_16_31
Last ObjectModification:
2015_09_22-PM-05_59_13
Theory : list_1
Home
Index