Nuprl Definition : DNSF
DNSF(isphi;K;n;v) == fix((λDNSF,isphi. if isphi then K (λx.(DNSF ff x)) else λx.if x <z n then v.x else λz.Ax fi fi ))\000C isphi
Definitions occuring in Statement :
select-tuple: x.n,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
bfalse: ff,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
axiom: Ax
FDL editor aliases :
DNSF
DNSF(isphi;K;n;v) ==
fix((\mlambda{}DNSF,isphi. if isphi then K (\mlambda{}x.(DNSF ff x)) else \mlambda{}x.if x <z n then v.x else \mlambda{}z.Ax fi fi ))\000C isphi
Date html generated:
2015_07_17-AM-07_53_03
Last ObjectModification:
2012_10_01-PM-07_01_29
Home
Index