Nuprl Definition : FOAssigment-rename
FOAssigment-rename(a;fmla;x;y) == if y ∈b mFOL-freevars(fmla) then a[y := a x] else a fi
Definitions occuring in Statement :
mFOL-freevars: mFOL-freevars(fmla),
update-assignment: a[x := v],
deq-member: x ∈b L,
int-deq: IntDeq,
ifthenelse: if b then t else f fi ,
apply: f a
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
deq-member: x ∈b L,
int-deq: IntDeq,
mFOL-freevars: mFOL-freevars(fmla),
update-assignment: a[x := v],
apply: f a
FDL editor aliases :
FOAssigment-rename
Latex:
FOAssigment-rename(a;fmla;x;y) == if y \mmember{}\msubb{} mFOL-freevars(fmla) then a[y := a x] else a fi
Date html generated:
2019_10_16-AM-11_39_02
Last ObjectModification:
2018_11_30-PM-11_56_18
Theory : minimal-first-order-logic
Home
Index