Nuprl Definition : mu'
mu'(P) == λx.(fst((TERMOF{p-mu-decider:o, 1:l, 1:l} P d x)))
Definitions occuring in Statement :
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
pi1: fst(t),
apply: f a
TermOfs occuring in Definition :
p-mu-decider
FDL editor aliases :
mu'
Latex:
mu'(P) == \mlambda{}x.(fst((TERMOF\{p-mu-decider:o, 1:l, 1:l\} P d x)))
Date html generated:
2016_05_15-PM-03_32_55
Last ObjectModification:
2015_09_23-AM-07_44_07
Theory : general
Home
Index