Nuprl Definition : regextW
regextW(G;t)==r Wsup(t;λi.regextW(G;G t i))
regextW(G;t) == fix((λregextW,t. Wsup(t;λi.(regextW (G t i))))) t
Definitions occuring in Statement :
Wsup: Wsup(a;b),
apply: f a,
fix: fix(F),
lambda: λx.A[x]
Definitions occuring in definition :
fix: fix(F),
Wsup: Wsup(a;b),
lambda: λx.A[x],
apply: f a
FDL editor aliases :
regextW
Latex:
regextW(G;t)==r Wsup(t;\mlambda{}i.regextW(G;G t i))
Latex:
regextW(G;t) == fix((\mlambda{}regextW,t. Wsup(t;\mlambda{}i.(regextW (G t i))))) t
Date html generated:
2019_10_31-AM-06_34_19
Last ObjectModification:
2018_08_04-PM-04_04_08
Theory : constructive!set!theory
Home
Index