E.3.4 Add_Num_Efficiently

spec

Add_Num_Efficiently =

generated type

Num ::= 0 | 1 | __0(Num) | __1(Num)

ops

__+__ , __ ++ __ : Num×Num -> Num

vars

x,y : Num

axioms

 

0 0=0;	0 1=1;
x 0+y 0=(x+y) 0;	x 0 ++ y 0=(x+y) 1;
x 0+y 1=(x+y) 1;	x 0 ++ y 1=(x ++ y) 0;
x 1+y 0=(x+y) 1;	x 1 ++ y 0=(x ++ y) 0;
x 1+y 1=(x ++ y) 0;	x 1 ++ y 1=(x ++ y) 1

%% __+__ is binary addition;
%% __ ++ __ is binary addition with carry

end