n f x := fn x
L’entier de CHURCH n permet donc d’itérer une fonction f sur un argument x.
Démonstration. Par récurrence.
Si n = 0,n f x ≡0 f x≡ K I f x := I x := x ≡ f0 xSi n = k+1,k+1 f x ≡s k f x ≡ S B k f x := B f (k f) x = f (k f x) = f (fk x) = f k+1 x