Problem:
 active(incr(nil())) -> mark(nil())
 active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
 active(adx(nil())) -> mark(nil())
 active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
 active(nats()) -> mark(adx(zeros()))
 active(zeros()) -> mark(cons(0(),zeros()))
 active(head(cons(X,L))) -> mark(X)
 active(tail(cons(X,L))) -> mark(L)
 mark(incr(X)) -> active(incr(mark(X)))
 mark(nil()) -> active(nil())
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(s(X)) -> active(s(mark(X)))
 mark(adx(X)) -> active(adx(mark(X)))
 mark(nats()) -> active(nats())
 mark(zeros()) -> active(zeros())
 mark(0()) -> active(0())
 mark(head(X)) -> active(head(mark(X)))
 mark(tail(X)) -> active(tail(mark(X)))
 incr(mark(X)) -> incr(X)
 incr(active(X)) -> incr(X)
 cons(mark(X1),X2) -> cons(X1,X2)
 cons(X1,mark(X2)) -> cons(X1,X2)
 cons(active(X1),X2) -> cons(X1,X2)
 cons(X1,active(X2)) -> cons(X1,X2)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 adx(mark(X)) -> adx(X)
 adx(active(X)) -> adx(X)
 head(mark(X)) -> head(X)
 head(active(X)) -> head(X)
 tail(mark(X)) -> tail(X)
 tail(active(X)) -> tail(X)

Proof:
 Bounds Processor:
  bound: 9
  enrichment: match
  automaton:
   final states: {12,11,10,9,8,7,6,5}
   transitions:
    zeros4() -> 45*
    cons5(75,58) -> 84*
    cons5(61,45) -> 62*
    cons5(136,65) -> 66*
    cons5(61,65) -> 101*
    cons5(89,111) -> 113*
    cons5(46,65) -> 66*
    cons5(112,88) -> 90*
    cons5(53,65) -> 66*
    cons5(43,65) -> 66*
    cons5(100,65) -> 101*
    cons5(75,65) -> 66*
    cons5(89,88) -> 90*
    cons5(114,94) -> 115*
    cons5(46,42) -> 54*
    cons5(61,58) -> 99*
    cons5(46,58) -> 84*
    cons5(43,42) -> 54*
    cons5(53,58) -> 84*
    cons5(43,58) -> 84*
    cons5(75,42) -> 54*
    cons5(112,111) -> 113*
    active5(115) -> 5*
    active5(75) -> 137,122,53,61
    active5(112) -> 114*
    active5(62) -> 37*
    active5(99) -> 73*
    active5(101) -> 77*
    active5(78) -> 6*
    mark5(95) -> 114*
    mark5(90) -> 5*
    mark5(75) -> 61*
    mark5(66) -> 77*
    mark5(61) -> 100*
    mark5(46) -> 61*
    mark5(113) -> 6*
    mark5(53) -> 61*
    mark5(43) -> 61*
    incr3(59) -> 60*
    cons6(75,58) -> 84,99
    cons6(46,45) -> 62*
    cons6(136,65) -> 101*
    cons6(120,88) -> 121*
    cons6(61,65) -> 101*
    cons6(95,94) -> 115*
    cons6(46,65) -> 101*
    cons6(53,45) -> 62*
    cons6(43,45) -> 62*
    cons6(112,94) -> 115*
    cons6(53,65) -> 101*
    cons6(43,65) -> 101*
    cons6(107,106) -> 108*
    cons6(75,45) -> 62*
    cons6(134,94) -> 115*
    cons6(75,65) -> 66,101
    cons6(136,58) -> 99*
    cons6(134,106) -> 108*
    cons6(46,58) -> 99*
    cons6(122,65) -> 123*
    cons6(120,111) -> 127*
    cons6(53,58) -> 99*
    cons6(43,58) -> 99*
    cons6(136,45) -> 62*
    05() -> 75*
    incr4(66) -> 67*
    incr4(73) -> 74*
    incr4(58) -> 94*
    incr5(65) -> 111*
    incr5(77) -> 78*
    incr5(99) -> 74*
    incr5(84) -> 74*
    incr5(59) -> 74*
    incr5(58) -> 88*
    incr6(65) -> 106*
    incr6(101) -> 78*
    incr6(66) -> 78*
    incr6(123) -> 78*
    s4(46) -> 95*
    s4(53) -> 95*
    s4(43) -> 95*
    s5(75) -> 95,89
    s5(61) -> 112*
    s5(46) -> 95,89
    s5(83) -> 89*
    s5(53) -> 89*
    s5(43) -> 95,89
    active6(127) -> 6*
    active6(134) -> 120,114
    active6(136) -> 137,122,61
    active6(121) -> 5*
    active6(123) -> 77*
    active0(2) -> 5*
    active0(4) -> 5*
    active0(1) -> 5*
    active0(3) -> 5*
    mark6(75) -> 122*
    mark6(112) -> 120*
    mark6(89) -> 120*
    mark6(136) -> 122*
    mark6(61) -> 122*
    mark6(46) -> 122*
    mark6(108) -> 6*
    mark6(83) -> 122*
    mark6(53) -> 122*
    mark6(43) -> 122*
    incr0(2) -> 7*
    incr0(4) -> 7*
    incr0(1) -> 7*
    incr0(3) -> 7*
    s6(100) -> 107*
    s6(75) -> 142,134,89,112,107
    s6(122) -> 134*
    s6(136) -> 112*
    s6(61) -> 142,107
    s6(46) -> 142,112,107
    s6(53) -> 142,138,112,107
    s6(43) -> 142,112,107
    nil0() -> 1*
    cons7(136,65) -> 101,123
    cons7(134,111) -> 127*
    cons7(61,65) -> 123*
    cons7(89,111) -> 127*
    cons7(46,65) -> 123*
    cons7(130,106) -> 131*
    cons7(112,88) -> 121*
    cons7(83,65) -> 123*
    cons7(53,65) -> 123*
    cons7(43,65) -> 123*
    cons7(134,88) -> 121*
    cons7(138,111) -> 127*
    cons7(75,65) -> 123*
    cons7(89,88) -> 121*
    cons7(147,65) -> 123*
    cons7(138,88) -> 121*
    cons7(112,111) -> 127*
    mark0(2) -> 6*
    mark0(4) -> 6*
    mark0(1) -> 6*
    mark0(3) -> 6*
    06() -> 136*
    cons0(3,1) -> 8*
    cons0(3,3) -> 8*
    cons0(4,2) -> 8*
    cons0(4,4) -> 8*
    cons0(1,2) -> 8*
    cons0(1,4) -> 8*
    cons0(2,1) -> 8*
    cons0(2,3) -> 8*
    cons0(3,2) -> 8*
    cons0(3,4) -> 8*
    cons0(4,1) -> 8*
    cons0(4,3) -> 8*
    cons0(1,1) -> 8*
    cons0(1,3) -> 8*
    cons0(2,2) -> 8*
    cons0(2,4) -> 8*
    active7(147) -> 143,122,137
    active7(142) -> 130*
    active7(131) -> 6*
    active7(138) -> 130,120
    s0(2) -> 9*
    s0(4) -> 9*
    s0(1) -> 9*
    s0(3) -> 9*
    mark7(100) -> 141*
    mark7(75) -> 137*
    mark7(122) -> 137*
    mark7(107) -> 130*
    mark7(134) -> 130*
    mark7(136) -> 137*
    mark7(61) -> 137*
    mark7(46) -> 137*
    mark7(53) -> 137*
    mark7(43) -> 137*
    adx0(2) -> 10*
    adx0(4) -> 10*
    adx0(1) -> 10*
    adx0(3) -> 10*
    s7(75) -> 134*
    s7(147) -> 134*
    s7(137) -> 138*
    s7(141) -> 142*
    s7(136) -> 142,138,134,107
    s7(61) -> 134*
    s7(46) -> 134*
    s7(83) -> 138,134
    s7(53) -> 134*
    s7(43) -> 134*
    nats0() -> 2*
    cons8(142,106) -> 131*
    cons8(107,106) -> 131*
    cons8(144,106) -> 131*
    cons8(134,106) -> 131*
    cons8(138,106) -> 131*
    zeros0() -> 3*
    s8(100) -> 142*
    s8(75) -> 138*
    s8(147) -> 144,138
    s8(122) -> 138*
    s8(136) -> 138*
    s8(61) -> 138*
    s8(46) -> 138*
    s8(143) -> 144*
    s8(53) -> 138*
    s8(43) -> 138*
    00() -> 4*
    active8(149) -> 143*
    active8(144) -> 130*
    head0(2) -> 11*
    head0(4) -> 11*
    head0(1) -> 11*
    head0(3) -> 11*
    mark8(75) -> 143*
    mark8(147) -> 143*
    mark8(136) -> 143*
    mark8(61) -> 143*
    mark8(46) -> 143*
    mark8(83) -> 143*
    mark8(53) -> 143*
    mark8(43) -> 143*
    tail0(2) -> 12*
    tail0(4) -> 12*
    tail0(1) -> 12*
    tail0(3) -> 12*
    s9(75) -> 144*
    s9(147) -> 144*
    s9(149) -> 144*
    s9(136) -> 144*
    s9(61) -> 144*
    s9(46) -> 144*
    s9(83) -> 144*
    s9(53) -> 144*
    s9(43) -> 144*
    active1(20) -> 6*
    active1(15) -> 6*
    active1(17) -> 6*
    07() -> 147*
    01() -> 17*
    08() -> 149*
    zeros1() -> 15*
    nats1() -> 20*
    nil1() -> 20*
    mark1(16) -> 5*
    cons1(17,15) -> 16*
    adx1(15) -> 16*
    active2(30) -> 5*
    active2(25) -> 29*
    active2(23) -> 31*
    adx2(31) -> 30*
    adx2(23) -> 24*
    mark2(15) -> 31*
    mark2(17) -> 29*
    mark2(24) -> 6*
    cons2(25,23) -> 24*
    cons2(29,15) -> 30*
    02() -> 25*
    zeros2() -> 23*
    adx3(15) -> 30*
    adx3(42) -> 58*
    adx3(37) -> 36*
    adx3(54) -> 30*
    adx3(44) -> 30*
    adx3(23) -> 30*
    cons3(25,15) -> 30*
    cons3(35,23) -> 36*
    cons3(17,15) -> 30*
    cons3(46,58) -> 59*
    cons3(43,42) -> 44*
    cons3(53,58) -> 59*
    cons3(43,58) -> 59*
    active3(42) -> 37*
    active3(36) -> 6*
    active3(43) -> 35*
    mark3(60) -> 5*
    mark3(25) -> 35*
    mark3(44) -> 31*
    mark3(23) -> 37*
    adx4(45) -> 65*
    adx4(62) -> 36*
    adx4(47) -> 36*
    adx4(42) -> 36*
    adx4(23) -> 36*
    cons4(46,45) -> 47*
    cons4(61,65) -> 66*
    cons4(43,23) -> 36*
    cons4(95,94) -> 96*
    cons4(46,65) -> 66*
    cons4(25,23) -> 36*
    cons4(75,65) -> 66*
    cons4(46,58) -> 59*
    cons4(53,42) -> 54*
    cons4(83,58) -> 84*
    cons4(53,58) -> 84*
    cons4(43,58) -> 59*
    cons4(75,58) -> 59*
    03() -> 43*
    zeros3() -> 42*
    active4(84) -> 73*
    active4(74) -> 5*
    active4(54) -> 31*
    active4(46) -> 137,53
    mark4(67) -> 6*
    mark4(47) -> 37*
    mark4(59) -> 73*
    mark4(96) -> 5*
    mark4(46) -> 53*
    mark4(53) -> 83*
    mark4(43) -> 53*
    04() -> 46*
  problem:
   
  Qed