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)
 mark(nats()) -> active(nats())
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(0()) -> active(0())
 mark(incr(X)) -> active(incr(mark(X)))
 mark(pairs()) -> active(pairs())
 mark(odds()) -> active(odds())
 mark(s(X)) -> active(s(mark(X)))
 mark(head(X)) -> active(head(mark(X)))
 mark(tail(X)) -> active(tail(mark(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)
 head(mark(X)) -> head(X)
 head(active(X)) -> head(X)
 tail(mark(X)) -> tail(X)
 tail(active(X)) -> tail(X)

Proof:
 Bounds Processor:
  bound: 7
  enrichment: match
  automaton:
   final states: {11,10,9,8,7,6,5}
   transitions:
    03() -> 46*
    odds3() -> 44*
    active4(60) -> 62*
    active4(93) -> 82*
    active4(83) -> 5*
    active4(63) -> 37*
    mark4(60) -> 62*
    mark4(67) -> 82*
    mark4(62) -> 92*
    mark4(81) -> 6*
    mark4(61) -> 42*
    mark4(46) -> 62*
    04() -> 60*
    odds4() -> 58*
    cons5(46,45) -> 63*
    cons5(97,66) -> 83*
    cons5(67,66) -> 83*
    cons5(60,45) -> 63*
    cons5(90,79) -> 91*
    cons5(87,45) -> 63*
    cons5(93,66) -> 83*
    cons5(74,59) -> 75*
    active5(75) -> 42*
    active5(97) -> 90,82
    active5(87) -> 100,62,74
    active5(91) -> 6*
    mark5(80) -> 90*
    mark5(60) -> 74*
    mark5(87) -> 74*
    mark5(74) -> 74*
    mark5(46) -> 74*
    s3(60) -> 67*
    s3(62) -> 67*
    s3(46) -> 67*
    cons6(46,59) -> 75*
    cons6(101,79) -> 91*
    cons6(60,59) -> 75*
    cons6(80,79) -> 91*
    cons6(87,59) -> 75*
    cons6(97,79) -> 91*
    cons6(104,59) -> 75*
    cons6(74,59) -> 75*
    05() -> 87*
    active0(2) -> 5*
    active0(4) -> 5*
    active0(1) -> 5*
    active0(3) -> 5*
    s4(60) -> 67,80
    s4(92) -> 93*
    s4(87) -> 67,80
    s4(62) -> 93*
    s4(74) -> 80*
    s4(46) -> 67*
    nats0() -> 1*
    s5(60) -> 93,80
    s5(87) -> 93,80
    s5(62) -> 93*
    s5(104) -> 80*
    s5(74) -> 80,97
    s5(46) -> 80,93
    mark0(2) -> 6*
    mark0(4) -> 6*
    mark0(1) -> 6*
    mark0(3) -> 6*
    s6(100) -> 101*
    s6(60) -> 80,97
    s6(87) -> 93,80,97
    s6(104) -> 80,97
    s6(74) -> 80,97
    s6(46) -> 80,97
    cons0(3,1) -> 7*
    cons0(3,3) -> 7*
    cons0(4,2) -> 7*
    cons0(4,4) -> 7*
    cons0(1,2) -> 7*
    cons0(1,4) -> 7*
    cons0(2,1) -> 7*
    cons0(2,3) -> 7*
    cons0(3,2) -> 7*
    cons0(3,4) -> 7*
    cons0(4,1) -> 7*
    cons0(4,3) -> 7*
    cons0(1,1) -> 7*
    cons0(1,3) -> 7*
    cons0(2,2) -> 7*
    cons0(2,4) -> 7*
    active6(104) -> 100,74
    active6(101) -> 90*
    00() -> 2*
    mark6(60) -> 100*
    mark6(87) -> 100*
    mark6(104) -> 100*
    mark6(74) -> 100*
    mark6(46) -> 100*
    incr0(2) -> 8*
    incr0(4) -> 8*
    incr0(1) -> 8*
    incr0(3) -> 8*
    s7(60) -> 101*
    s7(87) -> 101*
    s7(104) -> 101,80,97
    s7(74) -> 101*
    s7(106) -> 101*
    s7(46) -> 101*
    pairs0() -> 3*
    06() -> 104*
    odds0() -> 4*
    cons7(104,59) -> 75*
    s0(2) -> 9*
    s0(4) -> 9*
    s0(1) -> 9*
    s0(3) -> 9*
    active7(106) -> 100*
    head0(2) -> 10*
    head0(4) -> 10*
    head0(1) -> 10*
    head0(3) -> 10*
    07() -> 106*
    tail0(2) -> 11*
    tail0(4) -> 11*
    tail0(1) -> 11*
    tail0(3) -> 11*
    active1(21) -> 6*
    active1(16) -> 6*
    active1(18) -> 6*
    odds1() -> 16*
    pairs1() -> 21*
    01() -> 18*
    nats1() -> 16*
    mark1(19) -> 5*
    incr1(21) -> 19*
    incr1(16) -> 17*
    cons1(18,17) -> 19*
    active2(31) -> 37*
    active2(33) -> 5*
    active2(28) -> 32*
    incr2(37) -> 33*
    incr2(31) -> 29*
    incr2(26) -> 27*
    mark2(29) -> 6*
    mark2(21) -> 37*
    mark2(18) -> 32*
    cons2(28,27) -> 29*
    cons2(32,17) -> 33*
    pairs2() -> 31*
    02() -> 28*
    odds2() -> 26*
    nats2() -> 26*
    incr3(45) -> 66*
    incr3(47) -> 33*
    incr3(42) -> 39*
    incr3(44) -> 45*
    incr3(31) -> 33*
    incr3(21) -> 33*
    incr3(63) -> 33*
    cons3(46,45) -> 47*
    cons3(28,17) -> 33*
    cons3(18,17) -> 33*
    cons3(38,27) -> 39*
    cons3(67,66) -> 68*
    active3(52) -> 42*
    active3(39) -> 6*
    active3(46) -> 38*
    mark3(47) -> 37*
    mark3(31) -> 42*
    mark3(68) -> 5*
    mark3(28) -> 38*
    incr4(75) -> 39*
    incr4(52) -> 39*
    incr4(59) -> 79*
    incr4(61) -> 39*
    incr4(31) -> 39*
    incr4(58) -> 59*
    cons4(28,27) -> 39*
    cons4(82,66) -> 83*
    cons4(60,59) -> 61*
    cons4(80,79) -> 81*
    cons4(62,45) -> 63*
    cons4(46,27) -> 39*
    pairs3() -> 52*
  problem:
   
  Qed