Nuprl Definition : pW-rec

let ind(p,a,f,G) = ind[p; a; f; G] in
letrec F(p,w) = let a,f=w in
                ind(p,a,f,λb.F(C[p; a; b],f(b)) in
F(par;w)
==r let a,f = w
    in ind[par; a; f; λb.let ind(p,a,f,G) = ind[p; a; f; G] in
                         letrec F(p,w) = let a,f=w in

                                         ind(p,a,f,λb.F(C[p; a; b],f(b)) in

F(C[par; a; b];f b)]

let ind(p,a,f,G) = ind[p; a; f; G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p; a; b],f(b)) in
F(par;w) ==
fix((λpW-rec,par,w. let a,f = w in ind[par; a; f; λb.(pW-rec C[par; a; b] (f b))])) par w

Definitions occuring in Statement : apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def
Definitions occuring in definition : fix: fix(F), spread: spread def, lambda: λx.A[x], apply: f a
FDL editor aliases : pW-rec

Latex:
let ind(p,a,f,G) = ind[p; a; f; G] in letrec F(p,w) = let a,f=w in ind(p,a,f,\mlambda{}b.F(C[p; a; b],f(b)) in F(par;w) ==r let a,f = w in ind[par; a; f; \mlambda{}b.let ind(p,a,f,G) = ind[p; a; f; G] in letrec F(p,w) = let a,f=w in ind(p,a,f,\mlambda{}b.F(C[p; a; b],f(b)) in F(C[par; a; b];f b)]

Latex:
let ind(p,a,f,G) = ind[p; a; f; G] in letrec F(p,w) = let a,f=w in ind(p,a,f,\mlambda{}b.F(C[p; a; b],f(b)) in F(par;w) == fix((\mlambda{}pW-rec,par,w. let a,f = w in ind[par; a; f; \mlambda{}b.(pW-rec C[par; a; b] (f b))])) par w Date html generated: 2016_05_14-AM-06_14_08 Last ObjectModification: 2015_09_22-PM-05_47_12 Theory : co-recursion Home Index