Function succ 

pub fn succ() -> Term

Applied to a binary-encoded number it produces its successor.

SUCC ≡ λn.SND (n Z A B) ≡ λ SND (1 Z A B)

where

Z ≡ PAIR ZERO ONE

A ≡ λp.p (λnm.PAIR (SHL0 n) (SHL1 n)) ≡ λ 1 (λ λ PAIR (SHL0 2) (SHL1 2))

B ≡ λp.p (λnm.PAIR (SHL1 n) (SHL0 m)) ≡ λ 1 (λ λ PAIR (SHL1 2) (SHL0 1))

Example

use lambda_calculus::data::num::binary::succ;
use lambda_calculus::*;

assert_eq!(beta(app(succ(), 0.into_binary()), NOR, 0), 1.into_binary());
assert_eq!(beta(app(succ(), 1.into_binary()), NOR, 0), 2.into_binary());
assert_eq!(beta(app(succ(), 2.into_binary()), NOR, 0), 3.into_binary());