PUBS: A Practical Upper Bounds Solver

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

%********************Series output*******************************
% Upper Bound of add(A,B) is 2*nat(B)+2.
% Upper Bound of mult(A,B) is 1*nat(A)*nat(A)+4*nat(A)+1.
% Upper Bound of subp(A,B,C) is 2*nat(B)+1.
% Upper Bound of mult3(A,B,C) is 2* (1*nat(A)*nat(A))+8*nat(A)+3.

%**********************RAML Output*******************************
%The number of ticks consumed by add is at most:
%          2.0*n + 2.0
%where
%   n is the length of the first component of the input
%
%The number of ticks consumed by mult is at most:
%          2.0*m*n + 3.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
%The number of ticks consumed by sub' is at most:
%          2.0*m + 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
%
%The number of ticks consumed by mult3 is at most:
%          4.0*m*n + 6.0*n + 3.0
%where
%   n is the length of the first component of the input
%   m is the length of the second component of the input
%   x is the length of the third component of the input

*********************************************************