Problem:
 active(nats()) -> mark(cons(0(),incr(nats())))
 active(pairs()) -> mark(cons(0(),incr(odds())))
 active(odds()) -> mark(incr(pairs()))
 active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
 active(head(cons(X,XS))) -> mark(X)
 active(tail(cons(X,XS))) -> mark(XS)
 active(cons(X1,X2)) -> cons(active(X1),X2)
 active(incr(X)) -> incr(active(X))
 active(s(X)) -> s(active(X))
 active(head(X)) -> head(active(X))
 active(tail(X)) -> tail(active(X))
 cons(mark(X1),X2) -> mark(cons(X1,X2))
 incr(mark(X)) -> mark(incr(X))
 s(mark(X)) -> mark(s(X))
 head(mark(X)) -> mark(head(X))
 tail(mark(X)) -> mark(tail(X))
 proper(nats()) -> ok(nats())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(incr(X)) -> incr(proper(X))
 proper(pairs()) -> ok(pairs())
 proper(odds()) -> ok(odds())
 proper(s(X)) -> s(proper(X))
 proper(head(X)) -> head(proper(X))
 proper(tail(X)) -> tail(proper(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 incr(ok(X)) -> ok(incr(X))
 s(ok(X)) -> ok(s(X))
 head(ok(X)) -> ok(head(X))
 tail(ok(X)) -> ok(tail(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Bounds Processor:
  bound: 9
  enrichment: match
  automaton:
   final states: {14,13,12,11,10,9,8,7}
   transitions:
    cons3(45,74) -> 66*
    cons3(62,61) -> 58*
    cons3(67,81) -> 82*
    active3(66) -> 58*
    pairs3() -> 71*
    03() -> 67*
    ok4(80) -> 58*
    ok4(87) -> 61*
    ok4(99) -> 114*
    ok4(101) -> 108*
    ok4(118) -> 114*
    incr4(82) -> 94*
    incr4(77) -> 87*
    incr4(114) -> 107*
    incr4(99) -> 100*
    incr4(76) -> 58*
    incr4(71) -> 80*
    odds3() -> 77*
    nats3() -> 77*
    active4(80) -> 90*
    active4(45) -> 86*
    active4(48) -> 76*
    top4(90) -> 14*
    cons4(108,107) -> 91*
    cons4(86,74) -> 58*
    cons4(101,100) -> 102*
    cons4(67,87) -> 80*
    mark3(82) -> 76*
    mark4(102) -> 91*
    mark4(94) -> 58*
    incr5(102) -> 105*
    incr5(99) -> 127*
    incr5(126) -> 119*
    incr5(91) -> 90*
    incr5(118) -> 127*
    active5(67) -> 103*
    active5(71) -> 91*
    active5(133) -> 112*
    active0(5) -> 7*
    active0(2) -> 7*
    active0(4) -> 7*
    active0(6) -> 7*
    active0(1) -> 7*
    active0(3) -> 7*
    proper4(77) -> 114*
    proper4(67) -> 108*
    proper4(94) -> 90*
    proper4(81) -> 107*
    nats0() -> 1*
    cons5(103,87) -> 90*
    cons5(101,127) -> 132*
    cons5(120,119) -> 115*
    mark0(5) -> 2*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(6) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    04() -> 101*
    cons0(3,1) -> 8*
    cons0(3,3) -> 8*
    cons0(3,5) -> 8*
    cons0(4,2) -> 8*
    cons0(4,4) -> 8*
    cons0(4,6) -> 8*
    cons0(5,1) -> 8*
    cons0(5,3) -> 8*
    cons0(5,5) -> 8*
    cons0(6,2) -> 8*
    cons0(1,2) -> 8*
    cons0(6,4) -> 8*
    cons0(1,4) -> 8*
    cons0(6,6) -> 8*
    cons0(1,6) -> 8*
    cons0(2,1) -> 8*
    cons0(2,3) -> 8*
    cons0(2,5) -> 8*
    cons0(3,2) -> 8*
    cons0(3,4) -> 8*
    cons0(3,6) -> 8*
    cons0(4,1) -> 8*
    cons0(4,3) -> 8*
    cons0(4,5) -> 8*
    cons0(5,2) -> 8*
    cons0(5,4) -> 8*
    cons0(5,6) -> 8*
    cons0(6,1) -> 8*
    cons0(1,1) -> 8*
    cons0(6,3) -> 8*
    cons0(1,3) -> 8*
    cons0(6,5) -> 8*
    cons0(1,5) -> 8*
    cons0(2,2) -> 8*
    cons0(2,4) -> 8*
    cons0(2,6) -> 8*
    odds4() -> 99*
    00() -> 3*
    proper5(105) -> 112*
    proper5(100) -> 119*
    proper5(82) -> 91*
    proper5(99) -> 126*
    proper5(101) -> 120*
    incr0(5) -> 9*
    incr0(2) -> 9*
    incr0(4) -> 9*
    incr0(6) -> 9*
    incr0(1) -> 9*
    incr0(3) -> 9*
    mark5(105) -> 90*
    pairs0() -> 4*
    top5(112) -> 14*
    odds0() -> 5*
    incr6(115) -> 112*
    incr6(132) -> 133*
    incr6(127) -> 139*
    incr6(129) -> 136*
    incr6(176) -> 165*
    incr6(178) -> 136*
    s0(5) -> 10*
    s0(2) -> 10*
    s0(4) -> 10*
    s0(6) -> 10*
    s0(1) -> 10*
    s0(3) -> 10*
    proper6(102) -> 115*
    proper6(99) -> 176*
    proper6(141) -> 149*
    proper6(118) -> 176*
    head0(5) -> 11*
    head0(2) -> 11*
    head0(4) -> 11*
    head0(6) -> 11*
    head0(1) -> 11*
    head0(3) -> 11*
    nats4() -> 118*
    tail0(5) -> 12*
    tail0(2) -> 12*
    tail0(4) -> 12*
    tail0(6) -> 12*
    tail0(1) -> 12*
    tail0(3) -> 12*
    ok5(132) -> 91*
    ok5(127) -> 107*
    ok5(129) -> 176,126
    ok5(178) -> 176*
    ok5(123) -> 168,120
    proper0(5) -> 13*
    proper0(2) -> 13*
    proper0(4) -> 13*
    proper0(6) -> 13*
    proper0(1) -> 13*
    proper0(3) -> 13*
    05() -> 123*
    ok0(5) -> 6*
    ok0(2) -> 6*
    ok0(4) -> 6*
    ok0(6) -> 6*
    ok0(1) -> 6*
    ok0(3) -> 6*
    odds5() -> 129*
    top0(5) -> 14*
    top0(2) -> 14*
    top0(4) -> 14*
    top0(6) -> 14*
    top0(1) -> 14*
    top0(3) -> 14*
    ok6(137) -> 115*
    ok6(184) -> 160*
    ok6(136) -> 165,119
    ok6(133) -> 90*
    ok6(190) -> 188*
    ok6(185) -> 181*
    top1(36) -> 14*
    cons6(140,139) -> 141*
    cons6(123,136) -> 137*
    cons6(148,127) -> 115*
    active1(5) -> 36*
    active1(2) -> 36*
    active1(4) -> 36*
    active1(6) -> 36*
    active1(1) -> 36*
    active1(3) -> 36*
    ok7(145) -> 112*
    ok7(192) -> 174*
    ok7(194) -> 149*
    ok7(151) -> 159*
    ok7(195) -> 179*
    proper1(5) -> 36*
    proper1(2) -> 36*
    proper1(4) -> 36*
    proper1(6) -> 36*
    proper1(1) -> 36*
    proper1(3) -> 36*
    incr7(137) -> 145*
    incr7(136) -> 151*
    incr7(188) -> 179*
    incr7(158) -> 149*
    incr7(190) -> 195*
    incr7(165) -> 159*
    ok1(30) -> 30,10
    ok1(15) -> 36,13
    ok1(32) -> 32,11
    ok1(17) -> 36,13
    ok1(34) -> 34,12
    ok1(26) -> 26,8
    ok1(28) -> 28,9
    ok1(23) -> 36,13
    active6(145) -> 149*
    active6(132) -> 115*
    active6(101) -> 148*
    tail1(5) -> 34*
    tail1(2) -> 34*
    tail1(4) -> 34*
    tail1(6) -> 34*
    tail1(1) -> 34*
    tail1(3) -> 34*
    mark6(141) -> 112*
    head1(5) -> 32*
    head1(2) -> 32*
    head1(4) -> 32*
    head1(6) -> 32*
    head1(1) -> 32*
    head1(3) -> 32*
    s6(101) -> 140*
    s6(123) -> 184*
    s1(5) -> 30*
    s1(2) -> 30*
    s1(4) -> 30*
    s1(6) -> 30*
    s1(1) -> 30*
    s1(3) -> 30*
    top6(149) -> 14*
    incr1(15) -> 16*
    incr1(5) -> 28*
    incr1(2) -> 28*
    incr1(4) -> 28*
    incr1(6) -> 28*
    incr1(1) -> 28*
    incr1(23) -> 18*
    incr1(3) -> 28*
    cons7(160,159) -> 149*
    cons7(152,151) -> 153*
    cons7(184,151) -> 194*
    cons7(164,136) -> 158*
    cons1(2,6) -> 26*
    cons1(17,16) -> 18*
    cons1(3,1) -> 26*
    cons1(3,3) -> 26*
    cons1(3,5) -> 26*
    cons1(4,2) -> 26*
    cons1(4,4) -> 26*
    cons1(4,6) -> 26*
    cons1(5,1) -> 26*
    cons1(5,3) -> 26*
    cons1(5,5) -> 26*
    cons1(6,2) -> 26*
    cons1(1,2) -> 26*
    cons1(6,4) -> 26*
    cons1(1,4) -> 26*
    cons1(6,6) -> 26*
    cons1(1,6) -> 26*
    cons1(2,1) -> 26*
    cons1(2,3) -> 26*
    cons1(2,5) -> 26*
    cons1(3,2) -> 26*
    cons1(3,4) -> 26*
    cons1(3,6) -> 26*
    cons1(4,1) -> 26*
    cons1(4,3) -> 26*
    cons1(4,5) -> 26*
    cons1(5,2) -> 26*
    cons1(5,4) -> 26*
    cons1(5,6) -> 26*
    cons1(6,1) -> 26*
    cons1(1,1) -> 26*
    cons1(6,3) -> 26*
    cons1(1,3) -> 26*
    cons1(6,5) -> 26*
    cons1(1,5) -> 26*
    cons1(2,2) -> 26*
    cons1(2,4) -> 26*
    proper7(140) -> 160*
    proper7(127) -> 165*
    proper7(139) -> 159*
    proper7(129) -> 188*
    proper7(101) -> 168*
    proper7(178) -> 188*
    proper7(153) -> 169*
    odds1() -> 15*
    active7(137) -> 158*
    active7(194) -> 169*
    active7(123) -> 164*
    pairs1() -> 23*
    mark7(153) -> 149*
    01() -> 17*
    s7(164) -> 200*
    s7(168) -> 160*
    s7(123) -> 152*
    s7(185) -> 192*
    nats1() -> 15*
    top7(169) -> 14*
    mark1(30) -> 30,10
    mark1(32) -> 32,11
    mark1(34) -> 34,12
    mark1(26) -> 26,8
    mark1(28) -> 28,9
    mark1(18) -> 36,7
    cons8(192,198) -> 201*
    cons8(200,151) -> 169*
    cons8(174,173) -> 169*
    top2(38) -> 14*
    proper8(152) -> 174*
    proper8(151) -> 173*
    proper8(136) -> 179*
    proper8(123) -> 181*
    active2(15) -> 38*
    active2(17) -> 38*
    active2(23) -> 38*
    s8(207) -> 206*
    s8(181) -> 174*
    proper2(15) -> 56*
    proper2(17) -> 50*
    proper2(16) -> 49*
    proper2(23) -> 54*
    proper2(18) -> 38*
    incr8(179) -> 173*
    incr8(195) -> 198*
    incr2(54) -> 38*
    incr2(56) -> 49*
    incr2(48) -> 46*
    incr2(43) -> 44*
    nats5() -> 178*
    cons2(50,49) -> 38*
    cons2(45,44) -> 46*
    06() -> 185*
    mark2(46) -> 38*
    odds6() -> 190*
    pairs2() -> 48*
    nats6() -> 190*
    02() -> 45*
    ok8(201) -> 169*
    ok8(198) -> 173*
    odds2() -> 43*
    active8(184) -> 200*
    active8(201) -> 203*
    active8(185) -> 207*
    nats2() -> 43*
    top8(203) -> 14*
    top3(58) -> 14*
    cons9(206,198) -> 203*
    proper3(45) -> 62*
    proper3(44) -> 61*
    proper3(46) -> 58*
    proper3(48) -> 63*
    proper3(43) -> 70*
    active9(192) -> 206*
    ok2(45) -> 50*
    ok2(48) -> 54*
    ok2(43) -> 56*
    ok3(77) -> 70*
    ok3(67) -> 62*
    ok3(74) -> 49*
    ok3(71) -> 63*
    ok3(66) -> 38*
    incr3(70) -> 61*
    incr3(77) -> 81*
    incr3(63) -> 58*
    incr3(48) -> 66*
    incr3(43) -> 74*
  problem:
   
  Qed