number 0 == "z"
number n == ["s", number (n - 1)]

decode "z"      == 0
decode ["s", X] == 1 + decode X

add X "z"      == X
add X ["s", Y] == ["s", add X Y]

sub X "z"             == X
sub ["s", X] ["s", Y] == sub X Y

mul X "z"      == "z"
mul X ["s", Y] == add X (mul X Y)

pow "z" ["s", Y] == "z"
pow ["s", X] "z" == ["s", "z"]
pow X ["s", Y]   == mul X (pow X Y)

eql "z" "z"           == ["s", "z"]
eql ["s", X] ["s", Y] == eql X Y
eql X Y               == "z"

lss "z" ["s", Y]      == ["s", "z"]
lss ["s", X] ["s", Y] == lss X Y
lss X Y               == "z"

leq "z" "z"            == ["s", "z"]
leq "z" ["s", Y]       == ["s", "z"]
leq ["s", X] "z"       == "z"
leq ["s", X] ["s", Y]  == leq X Y

xif "z" A B == B
xif X A B   == A

div X Y == xif (lss X Y) "z" ["s", div (sub X Y) Y]

mod X Y == xif (lss X Y) X (mod (sub X Y) Y)