YES(?,O(n^1))
13.96/3.75	YES(?,O(n^1))
13.96/3.76	
13.96/3.76	Problem:
13.96/3.76	 active(incr(nil())) -> mark(nil())
13.96/3.76	 active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
13.96/3.76	 active(adx(nil())) -> mark(nil())
13.96/3.76	 active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
13.96/3.76	 active(nats()) -> mark(adx(zeros()))
13.96/3.76	 active(zeros()) -> mark(cons(0(),zeros()))
13.96/3.76	 active(head(cons(X,L))) -> mark(X)
13.96/3.76	 active(tail(cons(X,L))) -> mark(L)
13.96/3.76	 active(incr(X)) -> incr(active(X))
13.96/3.76	 active(cons(X1,X2)) -> cons(active(X1),X2)
13.96/3.76	 active(s(X)) -> s(active(X))
13.96/3.76	 active(adx(X)) -> adx(active(X))
13.96/3.76	 active(head(X)) -> head(active(X))
13.96/3.76	 active(tail(X)) -> tail(active(X))
13.96/3.76	 incr(mark(X)) -> mark(incr(X))
13.96/3.76	 cons(mark(X1),X2) -> mark(cons(X1,X2))
13.96/3.76	 s(mark(X)) -> mark(s(X))
13.96/3.76	 adx(mark(X)) -> mark(adx(X))
13.96/3.76	 head(mark(X)) -> mark(head(X))
13.96/3.76	 tail(mark(X)) -> mark(tail(X))
13.96/3.76	 proper(incr(X)) -> incr(proper(X))
13.96/3.76	 proper(nil()) -> ok(nil())
13.96/3.76	 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
13.96/3.76	 proper(s(X)) -> s(proper(X))
13.96/3.76	 proper(adx(X)) -> adx(proper(X))
13.96/3.76	 proper(nats()) -> ok(nats())
13.96/3.76	 proper(zeros()) -> ok(zeros())
13.96/3.76	 proper(0()) -> ok(0())
13.96/3.76	 proper(head(X)) -> head(proper(X))
13.96/3.76	 proper(tail(X)) -> tail(proper(X))
13.96/3.76	 incr(ok(X)) -> ok(incr(X))
13.96/3.76	 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
13.96/3.76	 s(ok(X)) -> ok(s(X))
13.96/3.76	 adx(ok(X)) -> ok(adx(X))
13.96/3.76	 head(ok(X)) -> ok(head(X))
13.96/3.76	 tail(ok(X)) -> ok(tail(X))
13.96/3.76	 top(mark(X)) -> top(proper(X))
13.96/3.76	 top(ok(X)) -> top(active(X))
13.96/3.76	
13.96/3.76	Proof:
13.96/3.76	 Bounds Processor:
13.96/3.76	  bound: 10
13.96/3.76	  enrichment: match
13.96/3.76	  automaton:
13.96/3.76	   final states: {15,14,13,12,11,10,9,8,7}
13.96/3.76	   transitions:
13.96/3.76	    zeros3() -> 58*
13.96/3.76	    ok4(67) -> 51*
13.96/3.76	    ok4(79) -> 87*
13.96/3.76	    ok4(78) -> 86*
13.96/3.76	    adx4(69) -> 77*
13.96/3.76	    adx4(64) -> 51*
13.96/3.76	    adx4(58) -> 67*
13.96/3.76	    cons4(87,86) -> 74*
13.96/3.76	    cons4(79,78) -> 80*
13.96/3.76	    cons4(61,58) -> 67*
13.96/3.76	    cons4(63,42) -> 51*
13.96/3.76	    active4(67) -> 70*
13.96/3.76	    active4(42) -> 64*
13.96/3.76	    active4(44) -> 63*
13.96/3.76	    top4(70) -> 15*
13.96/3.76	    mark3(69) -> 64*
13.96/3.76	    mark4(80) -> 74*
13.96/3.76	    mark4(77) -> 51*
13.96/3.76	    adx5(80) -> 84*
13.96/3.76	    adx5(74) -> 70*
13.96/3.76	    active5(105) -> 91*
13.96/3.76	    active5(61) -> 73*
13.96/3.76	    active5(58) -> 74*
13.96/3.76	    cons5(97,96) -> 92*
13.96/3.76	    cons5(79,78) -> 98*
13.96/3.76	    cons5(73,58) -> 70*
13.96/3.76	    proper4(77) -> 70*
13.96/3.76	    proper4(61) -> 87*
13.96/3.76	    proper4(58) -> 86*
13.96/3.76	    04() -> 79*
13.96/3.76	    zeros4() -> 78*
13.96/3.76	    proper5(84) -> 91*
13.96/3.76	    proper5(79) -> 97*
13.96/3.76	    proper5(69) -> 74*
13.96/3.76	    proper5(78) -> 96*
13.96/3.76	    mark5(84) -> 70*
13.96/3.76	    active0(5) -> 7*
13.96/3.76	    active0(2) -> 7*
13.96/3.76	    active0(4) -> 7*
13.96/3.76	    active0(6) -> 7*
13.96/3.76	    active0(1) -> 7*
13.96/3.76	    active0(3) -> 7*
13.96/3.76	    top5(91) -> 15*
13.96/3.76	    incr0(5) -> 8*
13.96/3.76	    incr0(2) -> 8*
13.96/3.76	    incr0(4) -> 8*
13.96/3.76	    incr0(6) -> 8*
13.96/3.76	    incr0(1) -> 8*
13.96/3.76	    incr0(3) -> 8*
13.96/3.76	    adx6(92) -> 91*
13.96/3.76	    adx6(101) -> 151*
13.96/3.76	    adx6(98) -> 105*
13.96/3.76	    adx6(78) -> 108*
13.96/3.76	    nil0() -> 1*
13.96/3.76	    proper6(110) -> 118*
13.96/3.76	    proper6(80) -> 92*
13.96/3.76	    mark0(5) -> 2*
13.96/3.76	    mark0(2) -> 2*
13.96/3.76	    mark0(4) -> 2*
13.96/3.76	    mark0(6) -> 2*
13.96/3.76	    mark0(1) -> 2*
13.96/3.76	    mark0(3) -> 2*
13.96/3.76	    ok5(102) -> 133,97
13.96/3.76	    ok5(101) -> 141,96
13.96/3.76	    ok5(98) -> 74*
13.96/3.76	    cons0(3,1) -> 9*
13.96/3.76	    cons0(3,3) -> 9*
13.96/3.76	    cons0(3,5) -> 9*
13.96/3.76	    cons0(4,2) -> 9*
13.96/3.76	    cons0(4,4) -> 9*
13.96/3.76	    cons0(4,6) -> 9*
13.96/3.76	    cons0(5,1) -> 9*
13.96/3.76	    cons0(5,3) -> 9*
13.96/3.76	    cons0(5,5) -> 9*
13.96/3.76	    cons0(6,2) -> 9*
13.96/3.76	    cons0(1,2) -> 9*
13.96/3.76	    cons0(6,4) -> 9*
13.96/3.76	    cons0(1,4) -> 9*
13.96/3.76	    cons0(6,6) -> 9*
13.96/3.76	    cons0(1,6) -> 9*
13.96/3.76	    cons0(2,1) -> 9*
13.96/3.76	    cons0(2,3) -> 9*
13.96/3.76	    cons0(2,5) -> 9*
13.96/3.76	    cons0(3,2) -> 9*
13.96/3.76	    cons0(3,4) -> 9*
13.96/3.76	    cons0(3,6) -> 9*
13.96/3.76	    cons0(4,1) -> 9*
13.96/3.76	    cons0(4,3) -> 9*
13.96/3.76	    cons0(4,5) -> 9*
13.96/3.76	    cons0(5,2) -> 9*
13.96/3.76	    cons0(5,4) -> 9*
13.96/3.76	    cons0(5,6) -> 9*
13.96/3.76	    cons0(6,1) -> 9*
13.96/3.76	    cons0(1,1) -> 9*
13.96/3.76	    cons0(6,3) -> 9*
13.96/3.76	    cons0(1,3) -> 9*
13.96/3.76	    cons0(6,5) -> 9*
13.96/3.76	    cons0(1,5) -> 9*
13.96/3.76	    cons0(2,2) -> 9*
13.96/3.76	    cons0(2,4) -> 9*
13.96/3.76	    cons0(2,6) -> 9*
13.96/3.76	    ok6(105) -> 70*
13.96/3.76	    ok6(152) -> 194,147
13.96/3.76	    ok6(151) -> 132*
13.96/3.76	    ok6(106) -> 92*
13.96/3.76	    ok6(148) -> 145*
13.96/3.76	    ok6(155) -> 128*
13.96/3.76	    s0(5) -> 10*
13.96/3.76	    s0(2) -> 10*
13.96/3.76	    s0(4) -> 10*
13.96/3.76	    s0(6) -> 10*
13.96/3.76	    s0(1) -> 10*
13.96/3.76	    s0(3) -> 10*
13.96/3.76	    05() -> 102*
13.96/3.76	    adx0(5) -> 11*
13.96/3.76	    adx0(2) -> 11*
13.96/3.76	    adx0(4) -> 11*
13.96/3.76	    adx0(6) -> 11*
13.96/3.76	    adx0(1) -> 11*
13.96/3.76	    adx0(3) -> 11*
13.96/3.76	    zeros5() -> 101*
13.96/3.76	    nats0() -> 3*
13.96/3.76	    cons6(117,78) -> 92*
13.96/3.76	    cons6(102,151) -> 155*
13.96/3.76	    cons6(79,108) -> 109*
13.96/3.76	    cons6(102,101) -> 106*
13.96/3.76	    zeros0() -> 4*
13.96/3.77	    ok7(197) -> 181*
13.96/3.77	    ok7(204) -> 201*
13.96/3.77	    ok7(159) -> 186,144
13.96/3.77	    ok7(114) -> 91*
13.96/3.77	    ok7(206) -> 203*
13.96/3.77	    ok7(156) -> 118*
13.96/3.77	    ok7(160) -> 138*
13.96/3.77	    00() -> 5*
13.96/3.77	    adx7(152) -> 159*
13.96/3.77	    adx7(127) -> 118*
13.96/3.77	    adx7(194) -> 186*
13.96/3.77	    adx7(141) -> 132*
13.96/3.77	    adx7(106) -> 114*
13.96/3.77	    adx7(101) -> 120*
13.96/3.77	    head0(5) -> 12*
13.96/3.77	    head0(2) -> 12*
13.96/3.77	    head0(4) -> 12*
13.96/3.77	    head0(6) -> 12*
13.96/3.77	    head0(1) -> 12*
13.96/3.77	    head0(3) -> 12*
13.96/3.77	    active6(114) -> 118*
13.96/3.77	    active6(79) -> 117*
13.96/3.77	    active6(98) -> 92*
13.96/3.77	    tail0(5) -> 13*
13.96/3.77	    tail0(2) -> 13*
13.96/3.77	    tail0(4) -> 13*
13.96/3.77	    tail0(6) -> 13*
13.96/3.77	    tail0(1) -> 13*
13.96/3.77	    tail0(3) -> 13*
13.96/3.77	    mark6(110) -> 91*
13.96/3.77	    proper0(5) -> 14*
13.96/3.77	    proper0(2) -> 14*
13.96/3.77	    proper0(4) -> 14*
13.96/3.77	    proper0(6) -> 14*
13.96/3.77	    proper0(1) -> 14*
13.96/3.77	    proper0(3) -> 14*
13.96/3.77	    incr6(109) -> 110*
13.96/3.77	    ok0(5) -> 6*
13.96/3.77	    ok0(2) -> 6*
13.96/3.77	    ok0(4) -> 6*
13.96/3.77	    ok0(6) -> 6*
13.96/3.77	    ok0(1) -> 6*
13.96/3.77	    ok0(3) -> 6*
13.96/3.77	    top6(118) -> 15*
13.96/3.77	    top0(5) -> 15*
13.96/3.77	    top0(2) -> 15*
13.96/3.77	    top0(4) -> 15*
13.96/3.77	    top0(6) -> 15*
13.96/3.77	    top0(1) -> 15*
13.96/3.77	    top0(3) -> 15*
13.96/3.77	    incr7(155) -> 156*
13.96/3.77	    incr7(151) -> 162*
13.96/3.77	    incr7(121) -> 122*
13.96/3.77	    incr7(128) -> 118*
13.96/3.77	    top1(37) -> 15*
13.96/3.77	    proper7(122) -> 137*
13.96/3.77	    proper7(109) -> 128*
13.96/3.77	    proper7(79) -> 133*
13.96/3.77	    proper7(101) -> 194*
13.96/3.77	    proper7(108) -> 132*
13.96/3.77	    proper7(78) -> 141*
13.96/3.77	    active1(5) -> 37*
13.96/3.77	    active1(2) -> 37*
13.96/3.77	    active1(4) -> 37*
13.96/3.77	    active1(6) -> 37*
13.96/3.77	    active1(1) -> 37*
13.96/3.77	    active1(3) -> 37*
13.96/3.77	    active7(102) -> 131*
13.96/3.77	    active7(156) -> 137*
13.96/3.77	    active7(106) -> 127*
13.96/3.77	    proper1(5) -> 37*
13.96/3.77	    proper1(2) -> 37*
13.96/3.77	    proper1(4) -> 37*
13.96/3.77	    proper1(6) -> 37*
13.96/3.77	    proper1(1) -> 37*
13.96/3.77	    proper1(3) -> 37*
13.96/3.77	    mark7(122) -> 118*
13.96/3.77	    mark7(164) -> 137*
13.96/3.77	    ok1(35) -> 37,14
13.96/3.77	    ok1(25) -> 25,9
13.96/3.77	    ok1(20) -> 37,14
13.96/3.77	    ok1(27) -> 27,10
13.96/3.77	    ok1(29) -> 29,11
13.96/3.77	    ok1(31) -> 31,12
13.96/3.77	    ok1(33) -> 33,13
13.96/3.77	    ok1(23) -> 23,8
13.96/3.77	    ok1(18) -> 37,14
13.96/3.77	    cons7(131,101) -> 127*
13.96/3.77	    cons7(133,132) -> 128*
13.96/3.77	    cons7(163,162) -> 164*
13.96/3.77	    cons7(102,120) -> 121*
13.96/3.77	    cons7(131,151) -> 138*
13.96/3.77	    cons7(148,159) -> 160*
13.96/3.77	    tail1(5) -> 33*
13.96/3.77	    tail1(2) -> 33*
13.96/3.77	    tail1(4) -> 33*
13.96/3.77	    tail1(6) -> 33*
13.96/3.77	    tail1(1) -> 33*
13.96/3.77	    tail1(3) -> 33*
13.96/3.77	    top7(137) -> 15*
13.96/3.77	    head1(5) -> 31*
13.96/3.77	    head1(2) -> 31*
13.96/3.77	    head1(4) -> 31*
13.96/3.77	    head1(6) -> 31*
13.96/3.77	    head1(1) -> 31*
13.96/3.77	    head1(3) -> 31*
13.96/3.77	    incr8(160) -> 168*
13.96/3.77	    incr8(159) -> 172*
13.96/3.77	    incr8(186) -> 180*
13.96/3.77	    incr8(138) -> 137*
13.96/3.77	    adx1(5) -> 29*
13.96/3.77	    adx1(2) -> 29*
13.96/3.77	    adx1(4) -> 29*
13.96/3.77	    adx1(6) -> 29*
13.96/3.77	    adx1(1) -> 29*
13.96/3.77	    adx1(18) -> 19*
13.96/3.77	    adx1(3) -> 29*
13.96/3.77	    proper8(120) -> 144*
13.96/3.77	    proper8(162) -> 180*
13.96/3.77	    proper8(152) -> 203*
13.96/3.77	    proper8(102) -> 145*
13.96/3.77	    proper8(164) -> 170*
13.96/3.77	    proper8(151) -> 186*
13.96/3.77	    proper8(121) -> 138*
13.96/3.77	    proper8(101) -> 147*
13.96/3.77	    proper8(163) -> 181*
13.96/3.77	    s1(5) -> 27*
13.96/3.77	    s1(2) -> 27*
13.96/3.77	    s1(4) -> 27*
13.96/3.77	    s1(6) -> 27*
13.96/3.77	    s1(1) -> 27*
13.96/3.77	    s1(3) -> 27*
13.96/3.77	    cons8(185,159) -> 179*
13.96/3.77	    cons8(181,180) -> 170*
13.96/3.77	    cons8(173,172) -> 174*
13.96/3.77	    cons8(145,144) -> 138*
13.96/3.77	    cons8(197,172) -> 211*
13.96/3.77	    cons1(2,6) -> 25*
13.96/3.77	    cons1(3,1) -> 25*
13.96/3.77	    cons1(3,3) -> 25*
13.96/3.77	    cons1(3,5) -> 25*
13.96/3.77	    cons1(4,2) -> 25*
13.96/3.77	    cons1(4,4) -> 25*
13.96/3.77	    cons1(4,6) -> 25*
13.96/3.77	    cons1(5,1) -> 25*
13.96/3.77	    cons1(5,3) -> 25*
13.96/3.77	    cons1(5,5) -> 25*
13.96/3.77	    cons1(6,2) -> 25*
13.96/3.77	    cons1(1,2) -> 25*
13.96/3.77	    cons1(6,4) -> 25*
13.96/3.77	    cons1(1,4) -> 25*
13.96/3.77	    cons1(6,6) -> 25*
13.96/3.77	    cons1(1,6) -> 25*
13.96/3.77	    cons1(2,1) -> 25*
13.96/3.77	    cons1(2,3) -> 25*
13.96/3.77	    cons1(2,5) -> 25*
13.96/3.77	    cons1(3,2) -> 25*
13.96/3.77	    cons1(3,4) -> 25*
13.96/3.77	    cons1(3,6) -> 25*
13.96/3.77	    cons1(4,1) -> 25*
13.96/3.77	    cons1(4,3) -> 25*
13.96/3.77	    cons1(4,5) -> 25*
13.96/3.77	    cons1(5,2) -> 25*
13.96/3.77	    cons1(5,4) -> 25*
13.96/3.77	    cons1(5,6) -> 25*
13.96/3.77	    cons1(20,18) -> 19*
13.96/3.77	    cons1(6,1) -> 25*
13.96/3.77	    cons1(1,1) -> 25*
13.96/3.77	    cons1(6,3) -> 25*
13.96/3.77	    cons1(1,3) -> 25*
13.96/3.77	    cons1(6,5) -> 25*
13.96/3.77	    cons1(1,5) -> 25*
13.96/3.77	    cons1(2,2) -> 25*
13.96/3.77	    cons1(2,4) -> 25*
13.96/3.77	    06() -> 148*
13.96/3.77	    incr1(5) -> 23*
13.96/3.77	    incr1(2) -> 23*
13.96/3.77	    incr1(4) -> 23*
13.96/3.77	    incr1(6) -> 23*
13.96/3.77	    incr1(1) -> 23*
13.96/3.77	    incr1(3) -> 23*
13.96/3.77	    adx8(147) -> 144*
13.96/3.77	    adx8(206) -> 212*
13.96/3.77	    adx8(203) -> 198*
13.96/3.77	    01() -> 20*
13.96/3.77	    zeros6() -> 152*
13.96/3.77	    zeros1() -> 18*
13.96/3.77	    ok8(212) -> 198*
13.96/3.77	    ok8(172) -> 180*
13.96/3.77	    ok8(211) -> 170*
13.96/3.77	    ok8(208) -> 193*
13.96/3.77	    ok8(168) -> 137*
13.96/3.77	    nats1() -> 35*
13.96/3.77	    active8(155) -> 138*
13.96/3.77	    active8(168) -> 170*
13.96/3.77	    active8(148) -> 185*
13.96/3.77	    nil1() -> 35*
13.96/3.77	    s7(102) -> 163*
13.96/3.77	    s7(148) -> 197*
13.96/3.77	    mark1(25) -> 25,9
13.96/3.77	    mark1(27) -> 27,10
13.96/3.77	    mark1(29) -> 29,11
13.96/3.77	    mark1(19) -> 37,7
13.96/3.77	    mark1(31) -> 31,12
13.96/3.77	    mark1(33) -> 33,13
13.96/3.77	    mark1(23) -> 23,8
13.96/3.77	    top8(170) -> 15*
13.96/3.77	    top2(39) -> 15*
13.96/3.77	    incr9(212) -> 215*
13.96/3.77	    incr9(179) -> 170*
13.96/3.77	    incr9(198) -> 192*
13.96/3.77	    active2(35) -> 39*
13.96/3.77	    active2(20) -> 39*
13.96/3.77	    active2(18) -> 39*
13.96/3.77	    active9(160) -> 179*
13.96/3.77	    active9(197) -> 217*
13.96/3.77	    active9(204) -> 224*
13.96/3.77	    active9(211) -> 188*
13.96/3.77	    proper2(20) -> 49*
13.96/3.77	    proper2(19) -> 39*
13.96/3.77	    proper2(18) -> 48*
13.96/3.77	    mark8(174) -> 170*
13.96/3.77	    adx2(42) -> 43*
13.96/3.77	    adx2(48) -> 39*
13.96/3.77	    s8(145) -> 181*
13.96/3.77	    s8(204) -> 208*
13.96/3.77	    s8(148) -> 173*
13.96/3.77	    s8(185) -> 217*
13.96/3.77	    cons2(44,42) -> 43*
13.96/3.77	    cons2(49,48) -> 39*
13.96/3.77	    top9(188) -> 15*
13.96/3.77	    mark2(43) -> 39*
13.96/3.77	    proper9(172) -> 192*
13.96/3.77	    proper9(174) -> 188*
13.96/3.77	    proper9(159) -> 198*
13.96/3.77	    proper9(173) -> 193*
13.96/3.77	    proper9(148) -> 201*
13.96/3.77	    02() -> 44*
13.96/3.77	    cons9(208,215) -> 218*
13.96/3.77	    cons9(193,192) -> 188*
13.96/3.77	    cons9(217,172) -> 188*
13.96/3.77	    zeros2() -> 42*
13.96/3.77	    s9(224) -> 223*
13.96/3.77	    s9(201) -> 193*
13.96/3.77	    top3(51) -> 15*
13.96/3.77	    07() -> 204*
13.96/3.77	    proper3(42) -> 52*
13.96/3.77	    proper3(44) -> 53*
13.96/3.77	    proper3(43) -> 51*
13.96/3.77	    zeros7() -> 206*
13.96/3.77	    ok2(42) -> 48*
13.96/3.77	    ok2(44) -> 49*
13.96/3.77	    ok9(218) -> 188*
13.96/3.77	    ok9(215) -> 192*
13.96/3.77	    ok3(61) -> 53*
13.96/3.77	    ok3(56) -> 39*
13.96/3.77	    ok3(58) -> 52*
13.96/3.77	    top10(220) -> 15*
13.96/3.77	    adx3(52) -> 51*
13.96/3.77	    adx3(42) -> 56*
13.96/3.77	    active10(218) -> 220*
13.96/3.77	    active10(208) -> 223*
13.96/3.77	    cons3(44,42) -> 56*
13.96/3.77	    cons3(61,58) -> 69*
13.96/3.77	    cons3(53,52) -> 51*
13.96/3.77	    cons10(223,215) -> 220*
13.96/3.77	    active3(56) -> 51*
13.96/3.77	    03() -> 61*
13.96/3.77	  problem:
13.96/3.77	   
13.96/3.77	  Qed
13.96/3.77	EOF