*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        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()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1,appendAll3#1/1} / {::/2,nil/0}
      Obligation:
        Innermost
        basic terms: {append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}/{::,nil}
    Applied Processor:
      Bounds {initialAutomaton = minimal, enrichment = match}
    Proof:
      The problem is match-bounded by 4.
      The enriched problem is compatible with follwoing automaton.
        ::_0(2,2) -> 1
        ::_0(2,2) -> 2
        ::_0(2,2) -> 3
        ::_1(2,1) -> 1
        ::_1(2,3) -> 1
        ::_1(2,3) -> 3
        ::_1(2,4) -> 1
        ::_1(2,4) -> 4
        ::_2(2,7) -> 1
        ::_2(2,7) -> 5
        ::_2(2,7) -> 7
        ::_3(2,8) -> 1
        ::_3(2,8) -> 6
        ::_3(2,8) -> 8
        append_0(2,2) -> 1
        append_1(2,2) -> 3
        append_1(2,4) -> 1
        append_1(2,4) -> 4
        append_1(4,5) -> 1
        append_1(4,5) -> 5
        append_1(4,5) -> 7
        append_1(5,6) -> 1
        append_1(5,6) -> 6
        append_1(5,6) -> 8
        append_2(4,5) -> 7
        append_3(7,6) -> 8
        append#1_0(2,2) -> 1
        append#1_1(2,2) -> 1
        append#1_2(2,2) -> 3
        append#1_2(2,4) -> 1
        append#1_2(2,4) -> 4
        append#1_2(4,5) -> 1
        append#1_2(4,5) -> 5
        append#1_2(4,5) -> 7
        append#1_2(5,6) -> 1
        append#1_2(5,6) -> 6
        append#1_2(5,6) -> 8
        append#1_3(4,5) -> 7
        append#1_4(7,6) -> 8
        appendAll_0(2) -> 1
        appendAll_1(2) -> 1
        appendAll_1(2) -> 4
        appendAll#1_0(2) -> 1
        appendAll#1_1(2) -> 1
        appendAll#1_2(2) -> 1
        appendAll#1_2(2) -> 4
        appendAll2_0(2) -> 1
        appendAll2_1(2) -> 1
        appendAll2_1(2) -> 5
        appendAll2_1(2) -> 7
        appendAll2#1_0(2) -> 1
        appendAll2#1_1(2) -> 1
        appendAll2#1_2(2) -> 1
        appendAll2#1_2(2) -> 5
        appendAll2#1_2(2) -> 7
        appendAll3_0(2) -> 1
        appendAll3_1(2) -> 1
        appendAll3_1(2) -> 6
        appendAll3_1(2) -> 8
        appendAll3#1_0(2) -> 1
        appendAll3#1_1(2) -> 1
        appendAll3#1_2(2) -> 1
        appendAll3#1_2(2) -> 6
        appendAll3#1_2(2) -> 8
        nil_0() -> 1
        nil_0() -> 2
        nil_0() -> 3
        nil_1() -> 1
        nil_1() -> 4
        nil_1() -> 5
        nil_1() -> 6
        nil_1() -> 7
        nil_1() -> 8
        2 -> 1
        2 -> 3
        4 -> 1
        5 -> 1
        5 -> 7
        6 -> 1
        6 -> 8
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        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()
      Signature:
        {append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1,appendAll3#1/1} / {::/2,nil/0}
      Obligation:
        Innermost
        basic terms: {append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}/{::,nil}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).