Conventions Body of extends as far to the right as possible Ax.M N means Ax.(M N),not (x.M)N ·入x.fx=入x.(fx) ·x.入f.fx=入x.(入f.fx) Function applications are left-associative MN P means(M N)P,not M(N P) ·(2x.y.x-yW53=((x.y.x-y)5)3 ·(2f.入x.fx)(x.x+1)2=((2f.入x.fx)(2x.×+1))2Conventions • Body of  extends as far to the right as possible x. M N means x. (M N), not (x. M) N • x. f x = x. ( f x ) • x. f. f x = x. ( f. f x ) • Function applications are left-associative M N P means (M N) P, not M (N P) • (x. y. x - y) 5 3 = ( (x. y. x - y) 5 ) 3 • (f. x. f x) (x. x + 1) 2 = ( (f. x. f x) (x. x + 1) ) 2