Nuprl Definition : predicate-shift
A_x == λn,s. (A (n + 1) seq-append(1;n;seq-single(x);s))
Definitions occuring in Statement :
seq-append: seq-append(n;m;s1;s2),
seq-single: seq-single(t),
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
apply: f a,
add: n + m,
seq-append: seq-append(n;m;s1;s2),
natural_number: $n,
seq-single: seq-single(t)
FDL editor aliases :
predicate-shift
Latex:
A\_x == \mlambda{}n,s. (A (n + 1) seq-append(1;n;seq-single(x);s))
Date html generated:
2016_05_14-PM-04_07_09
Last ObjectModification:
2015_09_22-PM-06_02_06
Theory : fan-theorem
Home
Index