Nuprl Definition : pi-replace
pi-replace(t;x;P) ==
F(P) where
F(0) = pizero()
F(pre.P) = picomm(prefix-replace(t;x;pre);P1) where
P1 = F(P)
F(P + Q) = pioption(P1;Q1) where
P1 = F(P)
Q1 = F(Q)
F(P | Q) = pipar(P1;Q1) where
P1 = F(P)
Q1 = F(Q)
F(!P) = pirep(P1) where
P1 = F(P)
F(new v.R) = let v1 = if name_eq(v;x) then t else v fi in
pinew(v1;P1) where
P1 = F(R)
Definitions occuring in Statement :
prefix-replace: prefix-replace(t;x;pre),
pi_term_ind: pi_term_ind(v;zero;pre,body,rec1....;left,right,rec2,rec3....;left,right,rec4,rec5....;body,rec6....;name,body,rec7....),
pinew: pinew(name;body),
pirep: pirep(body),
pipar: pipar(left;right),
pioption: pioption(left;right),
picomm: picomm(pre;body),
pizero: pizero(),
name_eq: name_eq(x;y),
ifthenelse: if b then t else f fi ,
let: let
FDL editor aliases :
pi-replace
Latex:
pi-replace(t;x;P) ==
F(P) where
F(0) = pizero()
F(pre.P) = picomm(prefix-replace(t;x;pre);P1) where
P1 = F(P)
F(P + Q) = pioption(P1;Q1) where
P1 = F(P)
Q1 = F(Q)
F(P | Q) = pipar(P1;Q1) where
P1 = F(P)
Q1 = F(Q)
F(!P) = pirep(P1) where
P1 = F(P)
F(new v.R) = let v1 = if name\_eq(v;x) then t else v fi in
pinew(v1;P1) where
P1 = F(R)
Date html generated:
2015_07_23-AM-11_33_27
Last ObjectModification:
2012_08_30-PM-01_18_55
Home
Index