Nuprl Definition : pi-names
pi-names(p) ==
F(p) where
F(0) = []
F(pre.P) = pi-prefix-names(pre) ∪ P1 where
P1 = F(P)
F(P + Q) = P1 ∪ Q1 where
P1 = F(P)
Q1 = F(Q)
F(P | Q) = P1 ∪ Q1 where
P1 = F(P)
Q1 = F(Q)
F(!P) = P1 where
P1 = F(P)
F(new v.R) = [v / R1] where
R1 = F(R)
Definitions occuring in Statement :
pi-prefix-names: pi-prefix-names(p),
pi_term_ind: pi_term_ind(v;zero;pre,body,rec1....;left,right,rec2,rec3....;left,right,rec4,rec5....;body,rec6....;name,body,rec7....),
name-deq: NameDeq,
l-union: as ∪ bs,
cons: [a / b],
nil: []
FDL editor aliases :
pi-names
Latex:
pi-names(p) ==
F(p) where
F(0) = []
F(pre.P) = pi-prefix-names(pre) \mcup{} P1 where
P1 = F(P)
F(P + Q) = P1 \mcup{} Q1 where
P1 = F(P)
Q1 = F(Q)
F(P | Q) = P1 \mcup{} Q1 where
P1 = F(P)
Q1 = F(Q)
F(!P) = P1 where
P1 = F(P)
F(new v.R) = [v / R1] where
R1 = F(R)
Date html generated:
2015_07_23-AM-11_33_34
Last ObjectModification:
2012_08_30-PM-01_19_09
Home
Index