********************Result*************************************************

********************* Series Output****************************************
Upper Bound of leq(A,B) is nat(B)+1
Upper Bound of insert(A,B,C) is nat(B)*nat(C)+nat(C)+2*nat(B)+2
Upper Bound of isortlist(A,B) is 
  nat(A)* (nat(A)+1)*nat(B)/2+nat(A)*nat(B)+nat(A)* (nat(A)+1)+3*nat(A)+1

************************RAML Output*****************************************
The number of ticks consumed by leq is at most:
          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 insert is at most:
          m*x + 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
   x is the length of the elements of the second component of the input
The number of ticks consumed by isortlist is at most:
          0.5*n^2*m + n^2 - 0.5*n*m + n + 1.0
where
   n is the length of the input
   m is the length of the elements of the input

%***************************************************