pi-subst(t;x;p) ==  pi-subst-aux(p) [t / pi-names(p)] [<x, t>]



Definitions :  apply: f a,  pi-subst-aux: pi-subst-aux(p),  pi-names: pi-names(p),  cons: [car / cdr],  pair: <a, b>,  nil: []
FDL editor aliases :  pi-subst

pi-subst(t;x;p)  ==    pi-subst-aux(p)  [t  /  pi-names(p)]  [<x,  t>]


Date html generated: 2010_08_27-PM-08_42_00
Last ObjectModification: 2010_02_16-PM-01_22_26

Home Index