1.Previous
3.Next

*
*

The notation denotes capture-avoiding substitution: substituting for every free occurrence of in , while avoiding variable capture. This operation is defined inductively as follows:
* ; if .
* .
* has three cases:
** If , becomes ( is bound; no change).
** If , becomes .
** If , first ?-rename to with fresh to avoid name collisions, then continue as above. It becomes with .

There are several

1.Previous
3.Next