Function lambda_calculus::data::num::signed::simplify

pub fn simplify(encoding: Encoding) -> Term

Applied to a signed integer with a specified encoding, ensure that at least one element of the pair representing it is equal to zero.

SIMPLIFY ≡ Z (λzx.IS_ZERO (FST x) (λy.x) (λy.IS_ZERO (SND x) x (z (PAIR (PRED (FST x)) (PRED (SND x))))) I) ≡ Z (λ λ IS_ZERO (FST 1) (λ 2) (λ IS_ZERO (SND 2) 2 (3 (PAIR (PRED (FST 2)) (PRED (SND 2))))) I)

Example

use lambda_calculus::data::num::signed::simplify;
use lambda_calculus::*;

assert_eq!(beta(app(simplify(Church), (3, 0).into_church()), NOR, 0), (3, 0).into_church());
assert_eq!(beta(app(simplify(Church), (0, 3).into_church()), NOR, 0), (0, 3).into_church());
assert_eq!(beta(app(simplify(Church), (4, 1).into_church()), NOR, 0), (3, 0).into_church());