Nuprl Definition : pi-rank
pi-rank(p) ==
F(p) where
F(0) = 0
F(pre.P) = P1 + 1 where
P1 = F(P)
F(P + Q) = P1 + Q1 + 1 where
P1 = F(P)
Q1 = F(Q)
F(P | Q) = P1 + Q1 + 1 where
P1 = F(P)
Q1 = F(Q)
F(!P) = P1 + 1 where
P1 = F(P)
F(new v.R) = R1 + 1 where
R1 = 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....),
add: n + m,
natural_number: $n
FDL editor aliases :
pi-rank
Latex:
pi-rank(p) ==
F(p) where
F(0) = 0
F(pre.P) = P1 + 1 where
P1 = F(P)
F(P + Q) = P1 + Q1 + 1 where
P1 = F(P)
Q1 = F(Q)
F(P | Q) = P1 + Q1 + 1 where
P1 = F(P)
Q1 = F(Q)
F(!P) = P1 + 1 where
P1 = F(P)
F(new v.R) = R1 + 1 where
R1 = F(R)
Date html generated:
2015_07_23-AM-11_33_05
Last ObjectModification:
2012_08_30-PM-01_18_11
Home
Index