Nuprl Definition : alpha-avoid
alpha-avoid(L;t) ==  alpha-rename(alist-map(VarDeq;alpha-rename-alist(t;L));t)
Definitions occuring in Statement : 
alpha-rename-alist: alpha-rename-alist(t;L)
, 
alpha-rename: alpha-rename(f;t)
, 
var-deq: VarDeq
, 
alist-map: alist-map(eq;L)
Definitions occuring in definition : 
alpha-rename: alpha-rename(f;t)
, 
alist-map: alist-map(eq;L)
, 
var-deq: VarDeq
, 
alpha-rename-alist: alpha-rename-alist(t;L)
FDL editor aliases : 
alpha-avoid
Latex:
alpha-avoid(L;t)  ==    alpha-rename(alist-map(VarDeq;alpha-rename-alist(t;L));t)
Date html generated:
2020_05_19-PM-09_57_20
Last ObjectModification:
2020_03_09-PM-04_09_41
Theory : terms
Home
Index