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
Latex:
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:
2016_05_16-AM-09_08_36
Last ObjectModification:
2012_10_01-PM-07_01_29
Theory : first-order!and!ancestral!logic
Home
Index