Problem:
 active(nats()) -> mark(adx(zeros()))
 active(zeros()) -> mark(cons(0(),zeros()))
 active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
 active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
 active(hd(cons(X,Y))) -> mark(X)
 active(tl(cons(X,Y))) -> mark(Y)
 mark(nats()) -> active(nats())
 mark(adx(X)) -> active(adx(mark(X)))
 mark(zeros()) -> active(zeros())
 mark(cons(X1,X2)) -> active(cons(X1,X2))
 mark(0()) -> active(0())
 mark(incr(X)) -> active(incr(mark(X)))
 mark(s(X)) -> active(s(X))
 mark(hd(X)) -> active(hd(mark(X)))
 mark(tl(X)) -> active(tl(mark(X)))
 adx(mark(X)) -> adx(X)
 adx(active(X)) -> adx(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)
 incr(mark(X)) -> incr(X)
 incr(active(X)) -> incr(X)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 hd(mark(X)) -> hd(X)
 hd(active(X)) -> hd(X)
 tl(mark(X)) -> tl(X)
 tl(active(X)) -> tl(X)

Proof:
 Bounds Processor:
  bound: 7
  enrichment: match
  automaton:
   final states: {11,10,9,8,7,6,5,4}
   transitions:
    04() -> 44*
    zeros4() -> 43*
    active5(54) -> 32*
    active5(71) -> 5*
    active5(93) -> 4*
    active5(78) -> 70*
    cons5(84,83) -> 85*
    cons5(76,75) -> 93*
    cons5(87,86) -> 88*
    cons5(44,43) -> 54*
    cons5(44,59) -> 78*
    incr3(52) -> 53*
    incr4(60) -> 61*
    incr4(62) -> 63*
    incr4(51) -> 75*
    incr5(70) -> 71*
    incr5(52) -> 63*
    incr5(59) -> 86*
    incr5(66) -> 63*
    incr5(51) -> 83*
    mark5(85) -> 4*
    mark5(60) -> 70*
    mark5(88) -> 5*
    incr6(60) -> 71*
    incr6(59) -> 97*
    incr6(78) -> 71*
    s4(38) -> 76*
    s5(44) -> 87*
    s5(38) -> 84*
    active6(100) -> 5*
    active6(103) -> 4*
    active0(2) -> 4*
    active0(1) -> 4*
    active0(3) -> 4*
    cons6(84,83) -> 103*
    cons6(87,86) -> 100*
    cons6(98,97) -> 99*
    nats0() -> 1*
    mark6(99) -> 5*
    mark0(2) -> 5*
    mark0(1) -> 5*
    mark0(3) -> 5*
    s6(44) -> 98*
    adx0(2) -> 6*
    adx0(1) -> 6*
    adx0(3) -> 6*
    active7(104) -> 5*
    zeros0() -> 2*
    cons7(98,97) -> 104*
    cons0(3,1) -> 7*
    cons0(3,3) -> 7*
    cons0(1,2) -> 7*
    cons0(2,1) -> 7*
    cons0(2,3) -> 7*
    cons0(3,2) -> 7*
    cons0(1,1) -> 7*
    cons0(1,3) -> 7*
    cons0(2,2) -> 7*
    00() -> 3*
    incr0(2) -> 8*
    incr0(1) -> 8*
    incr0(3) -> 8*
    s0(2) -> 9*
    s0(1) -> 9*
    s0(3) -> 9*
    hd0(2) -> 10*
    hd0(1) -> 10*
    hd0(3) -> 10*
    tl0(2) -> 11*
    tl0(1) -> 11*
    tl0(3) -> 11*
    active1(17) -> 5*
    active1(12) -> 5*
    active1(18) -> 5*
    01() -> 17*
    zeros1() -> 12*
    nats1() -> 18*
    mark1(13) -> 4*
    cons1(17,12) -> 13*
    adx1(12) -> 13*
    active2(22) -> 28*
    active2(29) -> 4*
    cons2(17,12) -> 29*
    cons2(24,22) -> 23*
    adx2(22) -> 23*
    adx2(28) -> 29*
    mark2(12) -> 28*
    mark2(23) -> 5*
    02() -> 24*
    zeros2() -> 22*
    adx3(37) -> 51*
    adx3(32) -> 33*
    adx3(22) -> 29*
    adx3(12) -> 29*
    adx3(39) -> 29*
    adx3(46) -> 29*
    active3(37) -> 32*
    active3(33) -> 5*
    cons3(38,37) -> 39*
    cons3(24,22) -> 33*
    cons3(38,51) -> 52*
    mark3(22) -> 32*
    mark3(39) -> 28*
    mark3(53) -> 4*
    adx4(45) -> 33*
    adx4(37) -> 33*
    adx4(22) -> 33*
    adx4(54) -> 33*
    adx4(43) -> 59*
    zeros3() -> 37*
    03() -> 38*
    active4(66) -> 62*
    active4(46) -> 28*
    active4(63) -> 4*
    cons4(76,75) -> 77*
    cons4(38,37) -> 46*
    cons4(38,51) -> 66*
    cons4(44,43) -> 45*
    cons4(44,59) -> 60*
    mark4(45) -> 32*
    mark4(77) -> 4*
    mark4(52) -> 62*
    mark4(61) -> 5*
  problem:
   
  Qed