# Understanding First conversion rules from church's lambda bible

While going through Church's text on Lambda calculus , I cam across the first set of conversion rules .

Before writing out my query I would like to put the notation that church has used for substitution which is as follow :

$\ S$ $^x_yM$ means the act of substituting $y$ in place of $x$ all through out $M$ .

(I think there should be a mention of free variables but do not know why has that been left out)

The following are the rules of conversion that he has introduced :

I. To replace any part $M$ of a formula by $\ S$ $^x_yM$ , provided that $x$ is not a free variable of $M$ and $y$ does not occur in N.

II. To replace any part $( (\lambda x M)N)$ of a formula by $\ S$ $^x_yM$ provided that the bound variables of $M$ are distinct both from x and from the free variables of $N$.

III. To replace any part $\ S$ $^x_yM$ of a formula by $( (\lambda x M)y)$ provided that $( (\lambda x M)N)$ is well-formed and the bound variables of $N$ are distinct both from $x$ and from the free variables of $N$ .

Now next church writes that Rule 1 may be used to transform $ab (\lambda a a)(\lambda a a)$ into $ab (\lambda b b)(\lambda a a)$

and rule III can be used to transform $\lambda a a$ into $\lambda a .(\lambda a a) a$ .

I tried figuring out the above usage of rule 3 but could not be sure .

So , if in $\lambda a a$ if we think "a has been substituted in place of a" ,i.e., $\ S$ $^x_yM$ where $M$ is $\lambda a a$ and $x$ and $y$ are both $a$ , then I can see that application of rule 3 leads to $\lambda a .(\lambda a a) a$ .

Is this understanding of mine correct ?