Problem appendAll.raml

tct

Execution Time (secs)	0.607
Answer	YES(O(1),O(n^1))
Input	appendAll.raml

YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add following dependency tuples

Strict DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
  , append#1^#(nil(), @l2) -> c_3()
  , appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll#1^#(nil()) -> c_6()
  , appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll2#1^#(nil()) -> c_9()
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls))
  , appendAll3#1^#(nil()) -> c_12() }

and replace the set of basic marked basic terms accordingly.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
  , append#1^#(nil(), @l2) -> c_3()
  , appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll#1^#(nil()) -> c_6()
  , appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll2#1^#(nil()) -> c_9()
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls))
  , appendAll3#1^#(nil()) -> c_12() }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We consider the (estimated) dependency graph

  1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
     -->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
     -->_1 append#1^#(nil(), @l2) -> c_3() :3

  2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  3: append#1^#(nil(), @l2) -> c_3()

  4: appendAll^#(@l) -> appendAll#1^#(@l)
     -->_1 appendAll#1^#(::(@l1, @ls)) ->
           c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls)) :5
     -->_1 appendAll#1^#(nil()) -> c_6() :6

  5: appendAll#1^#(::(@l1, @ls)) ->
     c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :4
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  6: appendAll#1^#(nil()) -> c_6()

  7: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_8(append^#(appendAll(@l1), appendAll2(@ls)),
               appendAll^#(@l1),
               appendAll2^#(@ls)) :8
     -->_1 appendAll2#1^#(nil()) -> c_9() :9

  8: appendAll2#1^#(::(@l1, @ls)) ->
     c_8(append^#(appendAll(@l1), appendAll2(@ls)),
         appendAll^#(@l1),
         appendAll2^#(@ls))
     -->_3 appendAll2^#(@l) -> appendAll2#1^#(@l) :7
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :4
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  9: appendAll2#1^#(nil()) -> c_9()

  10: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
                appendAll2^#(@l1),
                appendAll3^#(@ls)) :11
     -->_1 appendAll3#1^#(nil()) -> c_12() :12

  11: appendAll3#1^#(::(@l1, @ls)) ->
      c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
           appendAll2^#(@l1),
           appendAll3^#(@ls))
     -->_3 appendAll3^#(@l) -> appendAll3#1^#(@l) :10
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :7
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  12: appendAll3#1^#(nil()) -> c_12()

We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {12} and add Pre({12}) = {10} to the strict component.
- We remove {9} and add Pre({9}) = {7} to the strict component.
- We remove {6} and add Pre({6}) = {4} to the strict component.
- We remove {3} and add Pre({3}) = {1} to the strict component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
  , appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }
Weak DPs:
  { append#1^#(nil(), @l2) -> c_3()
  , appendAll#1^#(nil()) -> c_6()
  , appendAll2#1^#(nil()) -> c_9()
  , appendAll3#1^#(nil()) -> c_12() }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We consider the the dependency graph

  ->1:{7,8}
     |
     |->7:{1,2}
     |   |
     |   `->8:{9}                              Weak SCC
     |
     |->3:{5,6}
     |   |
     |   |->7:{1,2}
     |   |   |
     |   |   `->8:{9}                          Weak SCC
     |   |
     |   |->5:{3,4}
     |   |   |
     |   |   |->7:{1,2}
     |   |   |   |
     |   |   |   `->8:{9}                      Weak SCC
     |   |   |
     |   |   `->6:{10}                         Weak SCC
     |   |
     |   `->4:{11}                             Weak SCC
     |
     `->2:{12}                                 Weak SCC


  Here dependency-pairs are as follows:

  Strict DPs:
    { 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
    , 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
    , 3: appendAll^#(@l) -> appendAll#1^#(@l)
    , 4: appendAll#1^#(::(@l1, @ls)) ->
         c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
    , 5: appendAll2^#(@l) -> appendAll2#1^#(@l)
    , 6: appendAll2#1^#(::(@l1, @ls)) ->
         c_8(append^#(appendAll(@l1), appendAll2(@ls)),
             appendAll^#(@l1),
             appendAll2^#(@ls))
    , 7: appendAll3^#(@l) -> appendAll3#1^#(@l)
    , 8: appendAll3#1^#(::(@l1, @ls)) ->
         c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
              appendAll2^#(@l1),
              appendAll3^#(@ls)) }
  Weak DPs:
    { 9: append#1^#(nil(), @l2) -> c_3()
    , 10: appendAll#1^#(nil()) -> c_6()
    , 11: appendAll2#1^#(nil()) -> c_9()
    , 12: appendAll3#1^#(nil()) -> c_12() }

The following rules are part of trailing weak paths, and thus they
can be removed:

  { 12: appendAll3#1^#(nil()) -> c_12()
  , 11: appendAll2#1^#(nil()) -> c_9()
  , 10: appendAll#1^#(nil()) -> c_6()
  , 9: append#1^#(nil(), @l2) -> c_3() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
  , appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We consider the (estimated) dependency graph

  1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
     -->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2

  2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  3: appendAll^#(@l) -> appendAll#1^#(@l)
     -->_1 appendAll#1^#(::(@l1, @ls)) ->
           c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls)) :4

  4: appendAll#1^#(::(@l1, @ls)) ->
     c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :3
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  5: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_8(append^#(appendAll(@l1), appendAll2(@ls)),
               appendAll^#(@l1),
               appendAll2^#(@ls)) :6

  6: appendAll2#1^#(::(@l1, @ls)) ->
     c_8(append^#(appendAll(@l1), appendAll2(@ls)),
         appendAll^#(@l1),
         appendAll2^#(@ls))
     -->_3 appendAll2^#(@l) -> appendAll2#1^#(@l) :5
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :3
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  7: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
                appendAll2^#(@l1),
                appendAll3^#(@ls)) :8

  8: appendAll3#1^#(::(@l1, @ls)) ->
     c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
          appendAll2^#(@l1),
          appendAll3^#(@ls))
     -->_3 appendAll3^#(@l) -> appendAll3#1^#(@l) :7
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :5
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }
Weak DPs: { append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We consider the (estimated) dependency graph

  1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
     -->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :8

  2: appendAll^#(@l) -> appendAll#1^#(@l)
     -->_1 appendAll#1^#(::(@l1, @ls)) ->
           c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls)) :3

  3: appendAll#1^#(::(@l1, @ls)) ->
     c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :2
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  4: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_8(append^#(appendAll(@l1), appendAll2(@ls)),
               appendAll^#(@l1),
               appendAll2^#(@ls)) :5

  5: appendAll2#1^#(::(@l1, @ls)) ->
     c_8(append^#(appendAll(@l1), appendAll2(@ls)),
         appendAll^#(@l1),
         appendAll2^#(@ls))
     -->_3 appendAll2^#(@l) -> appendAll2#1^#(@l) :4
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :2
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  6: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
                appendAll2^#(@l1),
                appendAll3^#(@ls)) :7

  7: appendAll3#1^#(::(@l1, @ls)) ->
     c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
          appendAll2^#(@l1),
          appendAll3^#(@ls))
     -->_3 appendAll3^#(@l) -> appendAll3#1^#(@l) :6
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :4
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  8: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }
Weak DPs:
  { append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls)) }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We consider the (estimated) dependency graph

  1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
     -->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :7

  2: appendAll^#(@l) -> appendAll#1^#(@l)
     -->_1 appendAll#1^#(::(@l1, @ls)) ->
           c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls)) :8

  3: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_8(append^#(appendAll(@l1), appendAll2(@ls)),
               appendAll^#(@l1),
               appendAll2^#(@ls)) :4

  4: appendAll2#1^#(::(@l1, @ls)) ->
     c_8(append^#(appendAll(@l1), appendAll2(@ls)),
         appendAll^#(@l1),
         appendAll2^#(@ls))
     -->_3 appendAll2^#(@l) -> appendAll2#1^#(@l) :3
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :2
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  5: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
                appendAll2^#(@l1),
                appendAll3^#(@ls)) :6

  6: appendAll3#1^#(::(@l1, @ls)) ->
     c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
          appendAll2^#(@l1),
          appendAll3^#(@ls))
     -->_3 appendAll3^#(@l) -> appendAll3#1^#(@l) :5
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :3
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  7: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  8: appendAll#1^#(::(@l1, @ls)) ->
     c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :2
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {3} to the strict component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }
Weak DPs:
  { append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls)) }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We consider the (estimated) dependency graph

  1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
     -->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :6

  2: appendAll^#(@l) -> appendAll#1^#(@l)
     -->_1 appendAll#1^#(::(@l1, @ls)) ->
           c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls)) :7

  3: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_8(append^#(appendAll(@l1), appendAll2(@ls)),
               appendAll^#(@l1),
               appendAll2^#(@ls)) :8

  4: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
                appendAll2^#(@l1),
                appendAll3^#(@ls)) :5

  5: appendAll3#1^#(::(@l1, @ls)) ->
     c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
          appendAll2^#(@l1),
          appendAll3^#(@ls))
     -->_3 appendAll3^#(@l) -> appendAll3#1^#(@l) :4
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :3
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  6: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  7: appendAll#1^#(::(@l1, @ls)) ->
     c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :2
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  8: appendAll2#1^#(::(@l1, @ls)) ->
     c_8(append^#(appendAll(@l1), appendAll2(@ls)),
         appendAll^#(@l1),
         appendAll2^#(@ls))
     -->_3 appendAll2^#(@l) -> appendAll2#1^#(@l) :3
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :2
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll3^#(@l) -> appendAll3#1^#(@l) }
Weak DPs:
  { append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , 8: appendAll3#1^#(::(@l1, @ls)) ->
       c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
            appendAll2^#(@l1),
            appendAll3^#(@ls)) }
Trs:
  { appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
    Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
    Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
    Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {},
    Uargs(append^#) = {}, Uargs(append#1^#) = {},
    Uargs(appendAll^#) = {}, Uargs(appendAll#1^#) = {},
    Uargs(c_5) = {1, 2}, Uargs(appendAll2^#) = {},
    Uargs(appendAll2#1^#) = {}, Uargs(c_8) = {1, 2, 3},
    Uargs(appendAll3^#) = {}, Uargs(appendAll3#1^#) = {},
    Uargs(c_11) = {1, 2, 3}

  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).

        [append](x1, x2) = [1] x1 + [1] x2 + [0]

      [append#1](x1, x2) = [1] x1 + [1] x2 + [0]

            [::](x1, x2) = [1] x1 + [1] x2 + [1]

                   [nil] = [0]

         [appendAll](x1) = [1] x1 + [0]

       [appendAll#1](x1) = [1] x1 + [0]

        [appendAll2](x1) = [1] x1 + [0]

      [appendAll2#1](x1) = [1] x1 + [0]

        [appendAll3](x1) = [1] x1 + [0]

      [appendAll3#1](x1) = [1] x1 + [0]

      [append^#](x1, x2) = [1] x1 + [1]

    [append#1^#](x1, x2) = [1] x1 + [0]

       [appendAll^#](x1) = [1] x1 + [0]

     [appendAll#1^#](x1) = [1] x1 + [0]

           [c_5](x1, x2) = [1] x1 + [1] x2 + [0]

      [appendAll2^#](x1) = [2] x1 + [0]

    [appendAll2#1^#](x1) = [2] x1 + [0]

       [c_8](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]

      [appendAll3^#](x1) = [3] x1 + [0]

    [appendAll3#1^#](x1) = [3] x1 + [0]

      [c_11](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]

  This order satisfies following ordering constraints

                [append(@l1, @l2)] =  [1] @l1 + [1] @l2 + [0]
                                   >= [1] @l1 + [1] @l2 + [0]
                                   =  [append#1(@l1, @l2)]

      [append#1(::(@x, @xs), @l2)] =  [1] @l2 + [1] @x + [1] @xs + [1]
                                   >= [1] @l2 + [1] @x + [1] @xs + [1]
                                   =  [::(@x, append(@xs, @l2))]

            [append#1(nil(), @l2)] =  [1] @l2 + [0]
                                   >= [1] @l2 + [0]
                                   =  [@l2]

                   [appendAll(@l)] =  [1] @l + [0]
                                   >= [1] @l + [0]
                                   =  [appendAll#1(@l)]

       [appendAll#1(::(@l1, @ls))] =  [1] @l1 + [1] @ls + [1]
                                   >  [1] @l1 + [1] @ls + [0]
                                   =  [append(@l1, appendAll(@ls))]

              [appendAll#1(nil())] =  [0]
                                   >= [0]
                                   =  [nil()]

                  [appendAll2(@l)] =  [1] @l + [0]
                                   >= [1] @l + [0]
                                   =  [appendAll2#1(@l)]

      [appendAll2#1(::(@l1, @ls))] =  [1] @l1 + [1] @ls + [1]
                                   >  [1] @l1 + [1] @ls + [0]
                                   =  [append(appendAll(@l1), appendAll2(@ls))]

             [appendAll2#1(nil())] =  [0]
                                   >= [0]
                                   =  [nil()]

                  [appendAll3(@l)] =  [1] @l + [0]
                                   >= [1] @l + [0]
                                   =  [appendAll3#1(@l)]

      [appendAll3#1(::(@l1, @ls))] =  [1] @l1 + [1] @ls + [1]
                                   >  [1] @l1 + [1] @ls + [0]
                                   =  [append(appendAll2(@l1), appendAll3(@ls))]

             [appendAll3#1(nil())] =  [0]
                                   >= [0]
                                   =  [nil()]

              [append^#(@l1, @l2)] =  [1] @l1 + [1]
                                   >  [1] @l1 + [0]
                                   =  [append#1^#(@l1, @l2)]

    [append#1^#(::(@x, @xs), @l2)] =  [1] @x + [1] @xs + [1]
                                   >= [1] @xs + [1]
                                   =  [append^#(@xs, @l2)]

                 [appendAll^#(@l)] =  [1] @l + [0]
                                   >= [1] @l + [0]
                                   =  [appendAll#1^#(@l)]

     [appendAll#1^#(::(@l1, @ls))] =  [1] @l1 + [1] @ls + [1]
                                   >= [1] @l1 + [1] @ls + [1]
                                   =  [c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))]

                [appendAll2^#(@l)] =  [2] @l + [0]
                                   >= [2] @l + [0]
                                   =  [appendAll2#1^#(@l)]

    [appendAll2#1^#(::(@l1, @ls))] =  [2] @l1 + [2] @ls + [2]
                                   >= [2] @l1 + [2] @ls + [2]
                                   =  [c_8(append^#(appendAll(@l1), appendAll2(@ls)),
                                           appendAll^#(@l1),
                                           appendAll2^#(@ls))]

                [appendAll3^#(@l)] =  [3] @l + [0]
                                   >= [3] @l + [0]
                                   =  [appendAll3#1^#(@l)]

    [appendAll3#1^#(::(@l1, @ls))] =  [3] @l1 + [3] @ls + [3]
                                   >  [3] @l1 + [3] @ls + [2]
                                   =  [c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
                                            appendAll2^#(@l1),
                                            appendAll3^#(@ls))]


Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules {1,8}.
Here rules are labeled according to the (estimated) dependency
graph

  1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
     -->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :5

  2: appendAll^#(@l) -> appendAll#1^#(@l)
     -->_1 appendAll#1^#(::(@l1, @ls)) ->
           c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls)) :6

  3: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_8(append^#(appendAll(@l1), appendAll2(@ls)),
               appendAll^#(@l1),
               appendAll2^#(@ls)) :7

  4: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
                appendAll2^#(@l1),
                appendAll3^#(@ls)) :8

  5: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  6: appendAll#1^#(::(@l1, @ls)) ->
     c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :2
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  7: appendAll2#1^#(::(@l1, @ls)) ->
     c_8(append^#(appendAll(@l1), appendAll2(@ls)),
         appendAll^#(@l1),
         appendAll2^#(@ls))
     -->_3 appendAll2^#(@l) -> appendAll2#1^#(@l) :3
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :2
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1

  8: appendAll3#1^#(::(@l1, @ls)) ->
     c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
          appendAll2^#(@l1),
          appendAll3^#(@ls))
     -->_3 appendAll3^#(@l) -> appendAll3#1^#(@l) :4
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :3
     -->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1


- The rules {1,8} have known complexity. These cover all
  predecessors of {4,5}, their complexity is equally bounded.

Overall, we obtain that the number of applications of rules
{1,4,5,8} is given by YES(?,O(n^1)).

We apply the transformation 'removetails' on the sub-problem:

Strict DPs:
  { appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll2^#(@l) -> appendAll2#1^#(@l) }
Weak DPs:
  { append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
  , appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost

We consider the the dependency graph

  ->1:{7,8}                                    Weak SCC
     |
     |->2:{2,6}
     |   |
     |   |->3:{1,5}
     |   |   |
     |   |   `->4:{3,4}                        Weak SCC
     |   |
     |   `->4:{3,4}                            Weak SCC
     |
     `->4:{3,4}                                Weak SCC


  Here dependency-pairs are as follows:

  Strict DPs:
    { 1: appendAll^#(@l) -> appendAll#1^#(@l)
    , 2: appendAll2^#(@l) -> appendAll2#1^#(@l) }
  Weak DPs:
    { 3: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
    , 4: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
    , 5: appendAll#1^#(::(@l1, @ls)) ->
         c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
    , 6: appendAll2#1^#(::(@l1, @ls)) ->
         c_8(append^#(appendAll(@l1), appendAll2(@ls)),
             appendAll^#(@l1),
             appendAll2^#(@ls))
    , 7: appendAll3^#(@l) -> appendAll3#1^#(@l)
    , 8: appendAll3#1^#(::(@l1, @ls)) ->
         c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
              appendAll2^#(@l1),
              appendAll3^#(@ls)) }

The following rules are part of trailing weak paths, and thus they
can be removed:

  { 3: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
  , 4: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }

We apply the transformation 'simpDPRHS' on the sub-problem:

Strict DPs:
  { appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll2^#(@l) -> appendAll2#1^#(@l) }
Weak DPs:
  { appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost

We consider the following dependency-graph

  1: appendAll^#(@l) -> appendAll#1^#(@l)
     -->_1 appendAll#1^#(::(@l1, @ls)) ->
           c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls)) :3

  2: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_8(append^#(appendAll(@l1), appendAll2(@ls)),
               appendAll^#(@l1),
               appendAll2^#(@ls)) :4

  3: appendAll#1^#(::(@l1, @ls)) ->
     c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :1

  4: appendAll2#1^#(::(@l1, @ls)) ->
     c_8(append^#(appendAll(@l1), appendAll2(@ls)),
         appendAll^#(@l1),
         appendAll2^#(@ls))
     -->_3 appendAll2^#(@l) -> appendAll2#1^#(@l) :2
     -->_2 appendAll^#(@l) -> appendAll#1^#(@l) :1

  5: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
                appendAll2^#(@l1),
                appendAll3^#(@ls)) :6

  6: appendAll3#1^#(::(@l1, @ls)) ->
     c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
          appendAll2^#(@l1),
          appendAll3^#(@ls))
     -->_3 appendAll3^#(@l) -> appendAll3#1^#(@l) :5
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :2

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { appendAll#1^#(::(@l1, @ls)) ->
    c_5(append^#(@l1, appendAll(@ls)), appendAll^#(@ls))
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_8(append^#(appendAll(@l1), appendAll2(@ls)),
        appendAll^#(@l1),
        appendAll2^#(@ls))
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_11(append^#(appendAll2(@l1), appendAll3(@ls)),
         appendAll2^#(@l1),
         appendAll3^#(@ls)) }

We apply the transformation 'usablerules' on the sub-problem:

Strict DPs:
  { appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll2^#(@l) -> appendAll2#1^#(@l) }
Weak DPs:
  { appendAll#1^#(::(@l1, @ls)) -> appendAll^#(@ls)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_1(appendAll^#(@l1), appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_2(appendAll2^#(@l1), appendAll3^#(@ls)) }
Weak Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost

No rule is usable.

We apply the transformation 'simpKP' on the sub-problem:

Strict DPs:
  { appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll2^#(@l) -> appendAll2#1^#(@l) }
Weak DPs:
  { appendAll#1^#(::(@l1, @ls)) -> appendAll^#(@ls)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_1(appendAll^#(@l1), appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_2(appendAll2^#(@l1), appendAll3^#(@ls)) }
StartTerms: basic terms
Strategy: innermost

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 1: appendAll^#(@l) -> appendAll#1^#(@l)
  , 3: appendAll#1^#(::(@l1, @ls)) -> appendAll^#(@ls)
  , 6: appendAll3#1^#(::(@l1, @ls)) ->
       c_2(appendAll2^#(@l1), appendAll3^#(@ls)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
    Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
    Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
    Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {},
    Uargs(append^#) = {}, Uargs(append#1^#) = {},
    Uargs(appendAll^#) = {}, Uargs(appendAll#1^#) = {},
    Uargs(c_5) = {}, Uargs(appendAll2^#) = {},
    Uargs(appendAll2#1^#) = {}, Uargs(c_8) = {},
    Uargs(appendAll3^#) = {}, Uargs(appendAll3#1^#) = {},
    Uargs(c_11) = {}, Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2}

  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).

        [append](x1, x2) = [0]

      [append#1](x1, x2) = [0]

            [::](x1, x2) = [1] x1 + [1] x2 + [2]

                   [nil] = [0]

         [appendAll](x1) = [0]

       [appendAll#1](x1) = [0]

        [appendAll2](x1) = [0]

      [appendAll2#1](x1) = [0]

        [appendAll3](x1) = [0]

      [appendAll3#1](x1) = [0]

      [append^#](x1, x2) = [0]

    [append#1^#](x1, x2) = [0]

       [appendAll^#](x1) = [2] x1 + [1]

     [appendAll#1^#](x1) = [2] x1 + [0]

           [c_5](x1, x2) = [0]

      [appendAll2^#](x1) = [2] x1 + [0]

    [appendAll2#1^#](x1) = [2] x1 + [0]

       [c_8](x1, x2, x3) = [0]

      [appendAll3^#](x1) = [2] x1 + [0]

    [appendAll3#1^#](x1) = [2] x1 + [0]

      [c_11](x1, x2, x3) = [0]

                     [c] = [0]

           [c_1](x1, x2) = [1] x1 + [1] x2 + [3]

           [c_2](x1, x2) = [1] x1 + [1] x2 + [0]

  This order satisfies following ordering constraints

                 [appendAll^#(@l)] =  [2] @l + [1]
                                   >  [2] @l + [0]
                                   =  [appendAll#1^#(@l)]

     [appendAll#1^#(::(@l1, @ls))] =  [2] @l1 + [2] @ls + [4]
                                   >  [2] @ls + [1]
                                   =  [appendAll^#(@ls)]

                [appendAll2^#(@l)] =  [2] @l + [0]
                                   >= [2] @l + [0]
                                   =  [appendAll2#1^#(@l)]

    [appendAll2#1^#(::(@l1, @ls))] =  [2] @l1 + [2] @ls + [4]
                                   >= [2] @l1 + [2] @ls + [4]
                                   =  [c_1(appendAll^#(@l1), appendAll2^#(@ls))]

                [appendAll3^#(@l)] =  [2] @l + [0]
                                   >= [2] @l + [0]
                                   =  [appendAll3#1^#(@l)]

    [appendAll3#1^#(::(@l1, @ls))] =  [2] @l1 + [2] @ls + [4]
                                   >  [2] @l1 + [2] @ls + [0]
                                   =  [c_2(appendAll2^#(@l1), appendAll3^#(@ls))]


Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules
{1,3,6}. Here rules are labeled according to the (estimated)
dependency graph

  1: appendAll^#(@l) -> appendAll#1^#(@l)
     -->_1 appendAll#1^#(::(@l1, @ls)) -> appendAll^#(@ls) :3

  2: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_1(appendAll^#(@l1), appendAll2^#(@ls)) :4

  3: appendAll#1^#(::(@l1, @ls)) -> appendAll^#(@ls)
     -->_1 appendAll^#(@l) -> appendAll#1^#(@l) :1

  4: appendAll2#1^#(::(@l1, @ls)) ->
     c_1(appendAll^#(@l1), appendAll2^#(@ls))
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :2
     -->_1 appendAll^#(@l) -> appendAll#1^#(@l) :1

  5: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_2(appendAll2^#(@l1), appendAll3^#(@ls)) :6

  6: appendAll3#1^#(::(@l1, @ls)) ->
     c_2(appendAll2^#(@l1), appendAll3^#(@ls))
     -->_2 appendAll3^#(@l) -> appendAll3#1^#(@l) :5
     -->_1 appendAll2^#(@l) -> appendAll2#1^#(@l) :2


- The rules {1,3,6} have known complexity. These cover all
  predecessors of {5}, their complexity is equally bounded.

Overall, we obtain that the number of applications of rules
{1,3,5,6} is given by YES(?,O(n^1)).

We apply the transformation 'removetails' on the sub-problem:

Strict DPs: { appendAll2^#(@l) -> appendAll2#1^#(@l) }
Weak DPs:
  { appendAll^#(@l) -> appendAll#1^#(@l)
  , appendAll#1^#(::(@l1, @ls)) -> appendAll^#(@ls)
  , appendAll2#1^#(::(@l1, @ls)) ->
    c_1(appendAll^#(@l1), appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_2(appendAll2^#(@l1), appendAll3^#(@ls)) }
StartTerms: basic terms
Strategy: innermost

We consider the the dependency graph

  ->1:{5,6}                                    Weak SCC
     |
     `->2:{1,4}
         |
         `->3:{2,3}                            Weak SCC


  Here dependency-pairs are as follows:

  Strict DPs:
    { 1: appendAll2^#(@l) -> appendAll2#1^#(@l) }
  Weak DPs:
    { 2: appendAll^#(@l) -> appendAll#1^#(@l)
    , 3: appendAll#1^#(::(@l1, @ls)) -> appendAll^#(@ls)
    , 4: appendAll2#1^#(::(@l1, @ls)) ->
         c_1(appendAll^#(@l1), appendAll2^#(@ls))
    , 5: appendAll3^#(@l) -> appendAll3#1^#(@l)
    , 6: appendAll3#1^#(::(@l1, @ls)) ->
         c_2(appendAll2^#(@l1), appendAll3^#(@ls)) }

The following rules are part of trailing weak paths, and thus they
can be removed:

  { 2: appendAll^#(@l) -> appendAll#1^#(@l)
  , 3: appendAll#1^#(::(@l1, @ls)) -> appendAll^#(@ls) }

We apply the transformation 'simpDPRHS' on the sub-problem:

Strict DPs: { appendAll2^#(@l) -> appendAll2#1^#(@l) }
Weak DPs:
  { appendAll2#1^#(::(@l1, @ls)) ->
    c_1(appendAll^#(@l1), appendAll2^#(@ls))
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_2(appendAll2^#(@l1), appendAll3^#(@ls)) }
StartTerms: basic terms
Strategy: innermost

We consider the following dependency-graph

  1: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) ->
           c_1(appendAll^#(@l1), appendAll2^#(@ls)) :2

  2: appendAll2#1^#(::(@l1, @ls)) ->
     c_1(appendAll^#(@l1), appendAll2^#(@ls))
     -->_2 appendAll2^#(@l) -> appendAll2#1^#(@l) :1

  3: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_2(appendAll2^#(@l1), appendAll3^#(@ls)) :4

  4: appendAll3#1^#(::(@l1, @ls)) ->
     c_2(appendAll2^#(@l1), appendAll3^#(@ls))
     -->_2 appendAll3^#(@l) -> appendAll3#1^#(@l) :3
     -->_1 appendAll2^#(@l) -> appendAll2#1^#(@l) :1

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { appendAll2#1^#(::(@l1, @ls)) ->
    c_1(appendAll^#(@l1), appendAll2^#(@ls)) }

We apply the transformation 'simpKP' on the sub-problem:

Strict DPs: { appendAll2^#(@l) -> appendAll2#1^#(@l) }
Weak DPs:
  { appendAll2#1^#(::(@l1, @ls)) -> appendAll2^#(@ls)
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_1(appendAll2^#(@l1), appendAll3^#(@ls)) }
StartTerms: basic terms
Strategy: innermost

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 1: appendAll2^#(@l) -> appendAll2#1^#(@l)
  , 2: appendAll2#1^#(::(@l1, @ls)) -> appendAll2^#(@ls)
  , 4: appendAll3#1^#(::(@l1, @ls)) ->
       c_1(appendAll2^#(@l1), appendAll3^#(@ls)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
    Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
    Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
    Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {},
    Uargs(append^#) = {}, Uargs(append#1^#) = {},
    Uargs(appendAll^#) = {}, Uargs(appendAll#1^#) = {},
    Uargs(c_5) = {}, Uargs(appendAll2^#) = {},
    Uargs(appendAll2#1^#) = {}, Uargs(c_8) = {},
    Uargs(appendAll3^#) = {}, Uargs(appendAll3#1^#) = {},
    Uargs(c_11) = {}, Uargs(c_1) = {}, Uargs(c_2) = {},
    Uargs(c_1) = {1, 2}

  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).

        [append](x1, x2) = [0]

      [append#1](x1, x2) = [0]

            [::](x1, x2) = [1] x1 + [1] x2 + [2]

                   [nil] = [0]

         [appendAll](x1) = [0]

       [appendAll#1](x1) = [0]

        [appendAll2](x1) = [0]

      [appendAll2#1](x1) = [0]

        [appendAll3](x1) = [0]

      [appendAll3#1](x1) = [0]

      [append^#](x1, x2) = [0]

    [append#1^#](x1, x2) = [0]

       [appendAll^#](x1) = [0]

     [appendAll#1^#](x1) = [0]

           [c_5](x1, x2) = [0]

      [appendAll2^#](x1) = [2] x1 + [1]

    [appendAll2#1^#](x1) = [2] x1 + [0]

       [c_8](x1, x2, x3) = [0]

      [appendAll3^#](x1) = [2] x1 + [0]

    [appendAll3#1^#](x1) = [2] x1 + [0]

      [c_11](x1, x2, x3) = [0]

                     [c] = [0]

           [c_1](x1, x2) = [0]

           [c_2](x1, x2) = [0]

                     [c] = [0]

           [c_1](x1, x2) = [1] x1 + [1] x2 + [1]

  This order satisfies following ordering constraints

                [appendAll2^#(@l)] =  [2] @l + [1]
                                   >  [2] @l + [0]
                                   =  [appendAll2#1^#(@l)]

    [appendAll2#1^#(::(@l1, @ls))] =  [2] @l1 + [2] @ls + [4]
                                   >  [2] @ls + [1]
                                   =  [appendAll2^#(@ls)]

                [appendAll3^#(@l)] =  [2] @l + [0]
                                   >= [2] @l + [0]
                                   =  [appendAll3#1^#(@l)]

    [appendAll3#1^#(::(@l1, @ls))] =  [2] @l1 + [2] @ls + [4]
                                   >  [2] @l1 + [2] @ls + [2]
                                   =  [c_1(appendAll2^#(@l1), appendAll3^#(@ls))]


Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules
{1,2,4}. Here rules are labeled according to the (estimated)
dependency graph

  1: appendAll2^#(@l) -> appendAll2#1^#(@l)
     -->_1 appendAll2#1^#(::(@l1, @ls)) -> appendAll2^#(@ls) :2

  2: appendAll2#1^#(::(@l1, @ls)) -> appendAll2^#(@ls)
     -->_1 appendAll2^#(@l) -> appendAll2#1^#(@l) :1

  3: appendAll3^#(@l) -> appendAll3#1^#(@l)
     -->_1 appendAll3#1^#(::(@l1, @ls)) ->
           c_1(appendAll2^#(@l1), appendAll3^#(@ls)) :4

  4: appendAll3#1^#(::(@l1, @ls)) ->
     c_1(appendAll2^#(@l1), appendAll3^#(@ls))
     -->_2 appendAll3^#(@l) -> appendAll3#1^#(@l) :3
     -->_1 appendAll2^#(@l) -> appendAll2#1^#(@l) :1


- The rules {1,2,4} have known complexity. These cover all
  predecessors of {3}, their complexity is equally bounded.

Overall, we obtain that the number of applications of rules
{1,2,3,4} is given by YES(?,O(n^1)).

We apply the transformation 'removetails' on the sub-problem:

Weak DPs:
  { appendAll2^#(@l) -> appendAll2#1^#(@l)
  , appendAll2#1^#(::(@l1, @ls)) -> appendAll2^#(@ls)
  , appendAll3^#(@l) -> appendAll3#1^#(@l)
  , appendAll3#1^#(::(@l1, @ls)) ->
    c_1(appendAll2^#(@l1), appendAll3^#(@ls)) }
StartTerms: basic terms
Strategy: innermost

We consider the the dependency graph

  ->1:{3,4}                                    Weak SCC
     |
     `->2:{1,2}                                Weak SCC


  Here dependency-pairs are as follows:

  Weak DPs:
    { 1: appendAll2^#(@l) -> appendAll2#1^#(@l)
    , 2: appendAll2#1^#(::(@l1, @ls)) -> appendAll2^#(@ls)
    , 3: appendAll3^#(@l) -> appendAll3#1^#(@l)
    , 4: appendAll3#1^#(::(@l1, @ls)) ->
         c_1(appendAll2^#(@l1), appendAll3^#(@ls)) }

The following rules are part of trailing weak paths, and thus they
can be removed:

  { 3: appendAll3^#(@l) -> appendAll3#1^#(@l)
  , 4: appendAll3#1^#(::(@l1, @ls)) ->
       c_1(appendAll2^#(@l1), appendAll3^#(@ls))
  , 1: appendAll2^#(@l) -> appendAll2#1^#(@l)
  , 2: appendAll2#1^#(::(@l1, @ls)) -> appendAll2^#(@ls) }

We apply the transformation 'usablerules' on the sub-problem:

Rules: Empty
StartTerms: basic terms
Strategy: innermost

We apply the transformation 'trivial' on the sub-problem:

Rules: Empty
StartTerms: basic terms
Strategy: innermost

We consider the dependency graph

  empty

All SCCs are trivial and dependency pairs can be removed.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))

tct-popstar

Execution Time (secs)	1.007
Answer	YES(O(1),O(n^1))
Input	appendAll.raml