Nuprl Definition : pi-simple-subst-aux
pi-simple-subst-aux(t;x;P;avoid) ==
Y
(λpi-simple-subst-aux,P,avoid. F(P) where
F(0) = pizero()
F(pre.R) = pi_prefix_ind(pre;
pisend(c,v)⇒ let c1 = if name_eq(c;x) then t else c fi in
let v1 = if name_eq(v;x) then t else v fi in
picomm(pisend(c1;v1);pi-simple-subst-aux R
avoid);
pircv(c,v)⇒ let w = maybe-new(v;avoid) in
let c1 = if name_eq(c;x) then t else c fi in
let R1 = pi-replace(w;v;R) in
picomm(pircv(c1;w);pi-simple-subst-aux R1
[w / avoid])) where
A = F(R)
F(P + Q) = pioption(pi-simple-subst-aux P avoid;pi-simple-subst-aux Q avoid) where
A = F(P)
B = F(Q)
F(P | Q) = pipar(pi-simple-subst-aux P avoid;pi-simple-subst-aux Q avoid) where
A = F(P)
B = F(Q)
F(!P) = pirep(pi-simple-subst-aux P avoid) where
A = F(P)
F(new v.P) = let w = maybe-new(v;avoid) in
let P1 = pi-replace(w;v;P) in
pinew(w;pi-simple-subst-aux P1 [w / avoid]) where
A = F(P))
P
avoid
Definitions occuring in Statement :
pi-replace: pi-replace(t;x;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....),
pinew: pinew(name;body),
pirep: pirep(body),
pipar: pipar(left;right),
pioption: pioption(left;right),
picomm: picomm(pre;body),
pizero: pizero(),
pi_prefix_ind: pi_prefix_ind,
pircv: pircv(chan;var),
pisend: pisend(chan;var),
maybe-new: maybe-new(s;avoid),
name_eq: name_eq(x;y),
cons: [a / b],
ifthenelse: if b then t else f fi ,
let: let,
ycomb: Y,
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
pi-simple-subst-aux
Latex:
pi-simple-subst-aux(t;x;P;avoid) ==
Y
(\mlambda{}pi-simple-subst-aux,P,avoid.
F(P) where
F(0) = pizero()
F(pre.R) = pi\_prefix\_ind(pre;
pisend(c,v){}\mRightarrow{} let c1 = if name\_eq(c;x)
then t
else c
fi in
let v1 = if name\_eq(v;x)
then t
else v
fi in
picomm(pisend(c1;v1);...
R
avoid);
pircv(c,v){}\mRightarrow{} let w = maybe-new(v;avoid) in
let c1 = if name\_eq(c;x)
then t
else c
fi in
let R1 = pi-replace(w;v;R) in
picomm(pircv(c1;w);...
R1
[w /
avoid])) \000C where
A = F(R)
F(P + Q) = pioption(pi-simple-subst-aux P avoid;pi-simple-subst-aux
Q
avoid) where
A = F(P)
B = F(Q)
F(P | Q) = pipar(pi-simple-subst-aux P avoid;pi-simple-subst-aux Q
avoid) where
A = F(P)
B = F(Q)
F(!P) = pirep(pi-simple-subst-aux P avoid) where
A = F(P)
F(new v.P) = let w = maybe-new(v;avoid) in
let P1 = pi-replace(w;v;P) in
pinew(w;pi-simple-subst-aux P1 [w / avoid]) where
A = F(P))
P
avoid
Date html generated:
2015_07_23-AM-11_33_40
Last ObjectModification:
2012_08_30-PM-01_19_17
Home
Index