From ordinary variables x, y, z… to λβη

x ∈ Λ;
M, N ∈ Λ ⇒ λx.M ∈ Λ ∧ M N ∈ Λ;
(M) = M, M N P = (M N) P.

x[x := P] = P;
y[x := P] = y;
(λx.M)[x := P] = λx.M;
(λy.M)[x := P] = λy.M[x := P];
(M N)[x := P] = M[x := P] N[x := P].

FV(x) = {x};
FV(λx.M) = FV(M) ∖ {x};
FV(M N) = FV(M) ∪ FV(N).

y ∉ FV(M) ⇒ λx.M = λy.M[x := y].

β = {((λx.M) N, M[x := N]) | M, N ∈ Λ};
η = {(λx.M x, M) | M ∈ Λ, x ∉ FV(M)};
βη = β ∪ η.

M ⊂ M ⊂ λx.M;
M ⊂ M N ⊃ N;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.

Fˡ(x) = x;
∃Q ∈ Λ: (M, Q) ∈ βη ⇒ Fˡ(M) = Q;
∄Q ∈ Λ: (λx.M, Q) ∈ βη ⇒ Fˡ(λx.M) = λx.Fˡ(M);
∄Q ∈ Λ: (M N, Q) ∈ βη ∧ ∃P ⊂ M: ∃Q ∈ Λ: (P, Q) ∈ βη ⇒ Fˡ(M N) = Fˡ(M) N;
∄Q ∈ Λ: (M N, Q) ∈ βη ∧ ∄P ⊂ M: ∃Q ∈ Λ: (P, Q) ∈ βη ⇒ Fˡ(M N) = M Fˡ(N).