Problem:
 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()

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {10,9,8,7,6,5,4,3}
   transitions:
    nil1() -> 24,19,16,9,7,5,10,8,6
    append1(2,16) -> 17,5,6
    append1(17,22) -> 22,7,8
    append1(22,24) -> 25,9,10
    append1(19,24) -> 25,9,10
    append1(1,2) -> 12*
    append1(1,16) -> 17,5,6
    append1(16,22) -> 22,7,8
    append1(2,1) -> 12*
    append1(17,19) -> 22,7,8
    append1(2,17) -> 17,5,6
    append1(22,25) -> 25,9,10
    append1(19,25) -> 25,9,10
    append1(1,1) -> 13*
    append1(16,19) -> 22,7,8
    append1(1,17) -> 17,5,6
    append1(2,2) -> 12*
    appendAll21(2) -> 19*
    appendAll21(1) -> 22*
    appendAll31(2) -> 24*
    appendAll31(1) -> 25*
    appendAll3#11(2) -> 9*
    appendAll3#11(1) -> 9*
    appendAll1(2) -> 16*
    appendAll1(1) -> 17*
    appendAll2#11(2) -> 7*
    appendAll2#11(1) -> 7*
    appendAll#11(2) -> 5*
    appendAll#11(1) -> 5*
    ::1(2,12) -> 12,13,3,4
    ::1(1,12) -> 12,13,3,4
    ::1(2,5) -> 17,5,6
    ::1(2,13) -> 13,3,4
    ::1(1,5) -> 17,5,6
    ::1(1,13) -> 13,3,4
    append#11(1,2) -> 3*
    append#11(2,1) -> 3*
    append#11(1,1) -> 3*
    append#11(2,2) -> 3*
    appendAll3#12(2) -> 24*
    appendAll3#12(1) -> 25*
    append0(1,2) -> 3*
    append0(2,1) -> 3*
    append0(1,1) -> 3*
    append0(2,2) -> 3*
    appendAll2#12(2) -> 19*
    appendAll2#12(1) -> 22*
    append#10(1,2) -> 4*
    append#10(2,1) -> 4*
    append#10(1,1) -> 4*
    append#10(2,2) -> 4*
    appendAll#12(2) -> 16*
    appendAll#12(1) -> 17*
    ::0(1,2) -> 1*
    ::0(2,1) -> 1*
    ::0(1,1) -> 1*
    ::0(2,2) -> 1*
    append#12(2,16) -> 17,5,6
    append#12(17,22) -> 22,7,8
    append#12(22,24) -> 25,9,10
    append#12(19,24) -> 25,9,10
    append#12(1,2) -> 12*
    append#12(1,16) -> 17,5,6
    append#12(16,22) -> 22,7,8
    append#12(2,1) -> 12*
    append#12(17,19) -> 22,7,8
    append#12(2,17) -> 17,5,6
    append#12(22,25) -> 25,9,10
    append#12(19,25) -> 25,9,10
    append#12(1,1) -> 13*
    append#12(16,19) -> 22,7,8
    append#12(1,17) -> 17,5,6
    append#12(2,2) -> 12*
    nil0() -> 2*
    ::2(2,28) -> 28,22,7
    ::2(1,28) -> 28,22,7
    appendAll0(2) -> 5*
    appendAll0(1) -> 5*
    append2(5,19) -> 28*
    append2(5,22) -> 28*
    appendAll#10(2) -> 6*
    appendAll#10(1) -> 6*
    ::3(1,29) -> 29,25,9
    ::3(2,29) -> 29,25,9
    appendAll20(2) -> 7*
    appendAll20(1) -> 7*
    append3(28,25) -> 29*
    appendAll2#10(2) -> 8*
    appendAll2#10(1) -> 8*
    append#13(5,22) -> 28*
    appendAll30(2) -> 9*
    appendAll30(1) -> 9*
    append#14(28,25) -> 29*
    appendAll3#10(2) -> 10*
    appendAll3#10(1) -> 10*
    1 -> 12,3,4
    2 -> 12,3,4
    16 -> 17,5,6
    17 -> 5,6
    19 -> 22,7,8
    22 -> 28,7,8
    24 -> 25,9,10
    25 -> 29,9,10
  problem:
   
  Qed