Nuprl Definition : W_ind
W_ind(F;w) == letrec H(par)=λw.let a,f = w in F a f (λb.(H Ax (f b))) in H(Ax) w
Definitions occuring in Statement :
genrec-ap: genrec-ap,
apply: f a,
lambda: λx.A[x],
spread: spread def,
axiom: Ax
Definitions occuring in definition :
genrec-ap: genrec-ap,
spread: spread def,
lambda: λx.A[x],
apply: f a,
axiom: Ax
FDL editor aliases :
W_ind
Latex:
W\_ind(F;w) == letrec H(par)=\mlambda{}w.let a,f = w in F a f (\mlambda{}b.(H Ax (f b))) in H(Ax) w
Date html generated:
2016_05_14-AM-06_15_34
Last ObjectModification:
2015_12_16-PM-02_41_05
Theory : co-recursion
Home
Index