x occurs free in x x occurs free in A B if it appears free in A or B x does not occur free in x -> A x occurs free in y -> A if x and y are different and x occurs free in A x occurs free in (A) if it occurs free in A x occurs bound in A B if it occurs bound in A or B x occurs bound in x -> A x occurs bound in y -> A if x occurs bound in A x occurs bound in (A) if it occurs bound in A A[x/B] means a copy of A in which every occurrence of x is replaced with B x[x/Z] is Z y[x/Z] is y where y is any name other than x (A B)[x/Z] is (A[x/Z] B[x/z]) ( x -> A )[x/Z] is x -> A ( y -> A )[x/Z] is y -> A[x/Z] x -> Z may be alpha-converted to y -> Z[x/y] so long as y does not appear free in X x->A B may be beta-converted to A[x/B] so long as x does not appear bound in A This rule is talking about (x->A) B, not x->(A B).