# Encoding of natural numbers

Fixpoint enc (n : nat) :=
lam(lam
match n with
| 0 ⇒ # 1
| S n# 0 (enc n)
end).

Lemma enc_lam m :
lambda (enc m).

Lemma enc_cls m :
closed (enc m).

Lemma enc_proc m :
proc (enc m).

*Procedures representing zero and the successor-function

Definition Zero : term := .\"z","s"; "z".
Definition Succ : term := .\"n","z","s"; "s" "n".

Lemma Succ_correct n : Succ (enc n) == enc (S n).

# Predecessor

Definition Pred : term := .\"n"; "n" !Zero (.\"n"; "n").

Lemma Pred_correct n : Pred (enc n) == enc (pred n).

Definition Add := R (.\ "a", "n", "m"; "n" "m" (.\"n"; !Succ ("a" "n" "m"))).

Add Zero (enc m) == enc m.

Add (enc (S n)) (enc m) == Succ (Add (enc n) (enc m)).

Add (enc n) (enc m) == enc (n + m).

# Multiplication

Definition Mul := R(.\ "Mul", "m", "n"; "m" !Zero (.\ "m"; !Add "n" ("Mul" "m" "n"))).

Lemma Mul_rec_0 m :
Mul Zero (enc m) == Zero.

Lemma Mul_rec_S n m :
Mul (enc (S n)) (enc m) == (Add (enc m)) (((lam (Mul #0)) (enc n)) (enc m)).

Lemma Mul_correct m n :
Mul (enc n) (enc m) == enc (n × m).