%********************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 *********************************************************