Nuprl Definition : pi-level
pi-level(p) ==
F(p) where
F(0) = 0
F(pre.P) = lvl where
lvl = F(P)
F(P + Q) = imax(lvl_P;lvl_Q) where
lvl_P = F(P)
lvl_Q = F(Q)
F(P | Q) = imax(lvl_P;lvl_Q) + 1 where
lvl_P = F(P)
lvl_Q = F(Q)
F(!P) = lvl_P + 1 where
lvl_P = F(P)
F(new v.R) = lvl_R where
lvl_R = F(R)
Definitions occuring in Statement :
pi_term_ind: pi_term_ind(v;zero;pre,body,rec1....;left,right,rec2,rec3....;left,right,rec4,rec5....;body,rec6....;name,body,rec7....),
imax: imax(a;b),
add: n + m,
natural_number: $n
FDL editor aliases :
pi-level
Latex:
pi-level(p) ==
F(p) where
F(0) = 0
F(pre.P) = lvl where
lvl = F(P)
F(P + Q) = imax(lvl$_{P}$;lvl$_{Q}$) where
lvl$_{P}$ = F(P)
lvl$_{Q}$ = F(Q)
F(P | Q) = imax(lvl$_{P}$;lvl$_{Q}$) + 1 where
lvl$_{P}$ = F(P)
lvl$_{Q}$ = F(Q)
F(!P) = lvl$_{P}$ + 1 where
lvl$_{P}$ = F(P)
F(new v.R) = lvl$_{R}$ where
lvl$_{R}$ = F(R)
Date html generated:
2015_07_23-AM-11_33_23
Last ObjectModification:
2012_08_30-PM-01_18_47
Home
Index