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

%****************************Series Output********************************
Upper Bound of append(A,B) is nat(A)+1

Upper Bound of out_appendall(A,B) is nat(A)*nat(B)

Upper Bound of appendall(A,B) is nat(A)*nat(B)+2*nat(A)+1

Upper Bound of out_appendall2(A,B,C) is nat(A)*nat(B)*nat(C)

Upper Bound of appendall2(A,B,C) is 2*nat(A)*nat(B)*nat(C)+2*nat(A)*nat(B)+3*nat(A)+1

Upper Bound of appendall2(A,B,C) is 2*nat(A)*nat(B)*nat(C)+2*nat(A)*nat(B)+ (3*nat(A)+1).

Upper Bound of out_appendall3(A,B,C,D) is nat(A)*nat(B)*nat(C)*nat(D)

Upper Bound of appendall3(A,B,C,D) is 3*nat(A)*nat(B)*nat(C)*nat(D)+2*nat(A)*nat(B)*nat(C)+3*nat(A)*nat(B)+3*nat(A)+1

%****************************RAML Output********************************
The number of ticks consumed by append 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 appendAll is at most:
          n*m + 2.0*n + 1.0
where
   n is the length of the input
   m is the length of the elements of the input

The number of ticks consumed by appendAll2 is at most:
          2.0*n*m*x + 2.0*n*m + 3.0*n + 1.0
where
   n is the length of the input
   m is the length of the elements of the input
   x is the length of the elements of the elements of the input

The number of ticks consumed by appendAll3 is at most:
          3.0*n*m*x*y + 2.0*n*m*x + 3.0*n*m + 3.0*n + 1.0
where
   n is the length of the input
   m is the length of the elements of the input
   x is the length of the elements of the elements of the input
   y is the length of the elements of the elements of the elements of the input