PUBS: A Practical Upper Bounds Solver

%*******************Result***********************************

%********************Series Output***************************

%Upper Bound of mult(A,B) is nat(B)+1
%Upper Bound of dyade(A,B) is nat(A)*nat(B)+2*nat(A)+1

%********************RAML Output*****************************

% The number of ticks consumed by mult is at most:
%           n + 1.0
% where
%    n is the length of the second component of the input
% 
% The number of ticks consumed by dyade is at most:
%           m*n + 2.0*n + 1.0
% where
%    n is the length of the first component of the input
%    m is the length of the second component of the input
%************************************************************