Nuprl Definition : pi_level
pi_level(pi-term) ==
pi_term_ind(pi-term;0;pr,P,l.l;P,Q,l_P,l_Q.imax(l_P;l_Q);P,Q,l_P,l_Q.imax(l_P;l_Q) + 1;P,l.l + 1;x,P,l.l)
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(pi-term) ==
pi\_term\_ind(pi-term;0;pr,P,l.l;P,Q,l$_{P}$,l$_{Q}$.imax(l\mbackslash{}\000Cff24_{P}$;l$_{Q}$);P,Q,l$_{P}$,l$_\mbackslash{}f\000Cf7bQ}$.imax(l$_{P}$;l$_{Q}$) + 1;P,l.l + 1;x,P,l.l)
Date html generated:
2015_07_23-AM-11_33_53
Last ObjectModification:
2012_08_30-PM-01_19_41
Home
Index