YES(?,O(n^1))
9.59/2.62	YES(?,O(n^1))
9.59/2.63	
9.59/2.63	Problem:
9.59/2.63	 active(nats()) -> mark(adx(zeros()))
9.59/2.63	 active(zeros()) -> mark(cons(0(),zeros()))
9.59/2.63	 active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
9.59/2.63	 active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
9.59/2.63	 active(hd(cons(X,Y))) -> mark(X)
9.59/2.63	 active(tl(cons(X,Y))) -> mark(Y)
9.59/2.63	 active(adx(X)) -> adx(active(X))
9.59/2.63	 active(incr(X)) -> incr(active(X))
9.59/2.63	 active(hd(X)) -> hd(active(X))
9.59/2.63	 active(tl(X)) -> tl(active(X))
9.59/2.63	 adx(mark(X)) -> mark(adx(X))
9.59/2.63	 incr(mark(X)) -> mark(incr(X))
9.59/2.63	 hd(mark(X)) -> mark(hd(X))
9.59/2.63	 tl(mark(X)) -> mark(tl(X))
9.59/2.63	 proper(nats()) -> ok(nats())
9.59/2.63	 proper(adx(X)) -> adx(proper(X))
9.59/2.63	 proper(zeros()) -> ok(zeros())
9.59/2.63	 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
9.59/2.63	 proper(0()) -> ok(0())
9.59/2.63	 proper(incr(X)) -> incr(proper(X))
9.59/2.63	 proper(s(X)) -> s(proper(X))
9.59/2.63	 proper(hd(X)) -> hd(proper(X))
9.59/2.63	 proper(tl(X)) -> tl(proper(X))
9.59/2.63	 adx(ok(X)) -> ok(adx(X))
9.59/2.63	 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
9.59/2.63	 incr(ok(X)) -> ok(incr(X))
9.59/2.63	 s(ok(X)) -> ok(s(X))
9.59/2.63	 hd(ok(X)) -> ok(hd(X))
9.59/2.63	 tl(ok(X)) -> ok(tl(X))
9.59/2.63	 top(mark(X)) -> top(proper(X))
9.59/2.63	 top(ok(X)) -> top(active(X))
9.59/2.63	
9.59/2.63	Proof:
9.59/2.63	 Bounds Processor:
9.59/2.63	  bound: 10
9.59/2.63	  enrichment: match
9.59/2.63	  automaton:
9.59/2.63	   final states: {14,13,12,11,10,9,8,7,6}
9.59/2.63	   transitions:
9.59/2.63	    ok9(204) -> 181*
9.59/2.63	    ok9(206) -> 177*
9.59/2.63	    03() -> 60*
9.59/2.63	    top10(207) -> 14*
9.59/2.63	    zeros3() -> 57*
9.59/2.63	    active10(206) -> 207*
9.59/2.63	    ok4(74) -> 82*
9.59/2.63	    ok4(73) -> 81*
9.59/2.63	    ok4(63) -> 50*
9.59/2.63	    cons4(60,57) -> 63*
9.59/2.63	    cons4(82,81) -> 69*
9.59/2.63	    cons4(74,73) -> 75*
9.59/2.63	    adx4(65) -> 72*
9.59/2.63	    adx4(62) -> 50*
9.59/2.63	    adx4(57) -> 63*
9.59/2.63	    active4(41) -> 62*
9.59/2.63	    active4(63) -> 68*
9.59/2.63	    top4(68) -> 14*
9.59/2.63	    mark3(65) -> 62*
9.59/2.63	    mark4(75) -> 69*
9.59/2.63	    mark4(72) -> 50*
9.59/2.63	    adx5(75) -> 79*
9.59/2.63	    adx5(69) -> 68*
9.59/2.63	    active5(100) -> 86*
9.59/2.63	    active5(57) -> 69*
9.59/2.63	    proper4(60) -> 82*
9.59/2.63	    proper4(72) -> 68*
9.59/2.63	    proper4(57) -> 81*
9.59/2.63	    04() -> 74*
9.59/2.63	    zeros4() -> 73*
9.59/2.63	    proper5(65) -> 69*
9.59/2.63	    proper5(79) -> 86*
9.59/2.63	    proper5(74) -> 92*
9.59/2.63	    proper5(73) -> 91*
9.59/2.63	    active0(5) -> 6*
9.59/2.63	    active0(2) -> 6*
9.59/2.63	    active0(4) -> 6*
9.59/2.63	    active0(1) -> 6*
9.59/2.63	    active0(3) -> 6*
9.59/2.63	    mark5(79) -> 68*
9.59/2.63	    nats0() -> 1*
9.59/2.64	    top5(86) -> 14*
9.59/2.64	    mark0(5) -> 2*
9.59/2.64	    mark0(2) -> 2*
9.59/2.64	    mark0(4) -> 2*
9.59/2.64	    mark0(1) -> 2*
9.59/2.64	    mark0(3) -> 2*
9.59/2.64	    adx6(87) -> 86*
9.59/2.64	    adx6(96) -> 142*
9.59/2.64	    adx6(93) -> 100*
9.59/2.64	    adx6(73) -> 103*
9.59/2.64	    adx0(5) -> 7*
9.59/2.64	    adx0(2) -> 7*
9.59/2.64	    adx0(4) -> 7*
9.59/2.64	    adx0(1) -> 7*
9.59/2.64	    adx0(3) -> 7*
9.59/2.64	    proper6(105) -> 112*
9.59/2.64	    proper6(75) -> 87*
9.59/2.64	    zeros0() -> 3*
9.59/2.64	    ok5(97) -> 124,92
9.59/2.64	    ok5(96) -> 129,91
9.59/2.64	    ok5(93) -> 69*
9.59/2.64	    cons0(3,1) -> 12*
9.59/2.64	    cons0(3,3) -> 12*
9.59/2.64	    cons0(3,5) -> 12*
9.59/2.64	    cons0(4,2) -> 12*
9.59/2.64	    cons0(4,4) -> 12*
9.59/2.64	    cons0(5,1) -> 12*
9.59/2.64	    cons0(5,3) -> 12*
9.59/2.64	    cons0(5,5) -> 12*
9.59/2.64	    cons0(1,2) -> 12*
9.59/2.64	    cons0(1,4) -> 12*
9.59/2.64	    cons0(2,1) -> 12*
9.59/2.64	    cons0(2,3) -> 12*
9.59/2.64	    cons0(2,5) -> 12*
9.59/2.64	    cons0(3,2) -> 12*
9.59/2.64	    cons0(3,4) -> 12*
9.59/2.64	    cons0(4,1) -> 12*
9.59/2.64	    cons0(4,3) -> 12*
9.59/2.64	    cons0(4,5) -> 12*
9.59/2.64	    cons0(5,2) -> 12*
9.59/2.64	    cons0(5,4) -> 12*
9.59/2.64	    cons0(1,1) -> 12*
9.59/2.64	    cons0(1,3) -> 12*
9.59/2.64	    cons0(1,5) -> 12*
9.59/2.64	    cons0(2,2) -> 12*
9.59/2.64	    cons0(2,4) -> 12*
9.59/2.64	    cons5(74,73) -> 93*
9.59/2.64	    cons5(92,91) -> 87*
9.59/2.64	    00() -> 4*
9.59/2.64	    ok6(100) -> 68*
9.59/2.64	    ok6(142) -> 123*
9.59/2.64	    ok6(139) -> 134*
9.59/2.64	    ok6(146) -> 122*
9.59/2.64	    ok6(101) -> 87*
9.59/2.64	    ok6(143) -> 180,138
9.59/2.64	    incr0(5) -> 8*
9.59/2.64	    incr0(2) -> 8*
9.59/2.64	    incr0(4) -> 8*
9.59/2.64	    incr0(1) -> 8*
9.59/2.64	    incr0(3) -> 8*
9.59/2.64	    05() -> 97*
9.59/2.64	    s0(5) -> 13*
9.59/2.64	    s0(2) -> 13*
9.59/2.64	    s0(4) -> 13*
9.59/2.64	    s0(1) -> 13*
9.59/2.64	    s0(3) -> 13*
9.59/2.64	    zeros5() -> 96*
9.59/2.64	    hd0(5) -> 9*
9.59/2.64	    hd0(2) -> 9*
9.59/2.64	    hd0(4) -> 9*
9.59/2.64	    hd0(1) -> 9*
9.59/2.64	    hd0(3) -> 9*
9.59/2.64	    cons6(74,103) -> 104*
9.59/2.64	    cons6(97,96) -> 101*
9.59/2.64	    cons6(97,142) -> 146*
9.59/2.64	    tl0(5) -> 10*
9.59/2.64	    tl0(2) -> 10*
9.59/2.64	    tl0(4) -> 10*
9.59/2.64	    tl0(1) -> 10*
9.59/2.64	    tl0(3) -> 10*
9.59/2.64	    ok7(150) -> 112*
9.59/2.64	    ok7(147) -> 175,133
9.59/2.64	    ok7(109) -> 86*
9.59/2.64	    ok7(186) -> 174*
9.59/2.64	    ok7(151) -> 131*
9.59/2.64	    ok7(193) -> 189*
9.59/2.64	    ok7(195) -> 192*
9.59/2.64	    proper0(5) -> 11*
9.59/2.64	    proper0(2) -> 11*
9.59/2.64	    proper0(4) -> 11*
9.59/2.64	    proper0(1) -> 11*
9.59/2.64	    proper0(3) -> 11*
9.59/2.64	    adx7(129) -> 123*
9.59/2.64	    adx7(119) -> 112*
9.59/2.64	    adx7(101) -> 109*
9.59/2.64	    adx7(96) -> 116*
9.59/2.64	    adx7(143) -> 147*
9.59/2.64	    adx7(180) -> 175*
9.59/2.64	    ok0(5) -> 5*
9.59/2.64	    ok0(2) -> 5*
9.59/2.64	    ok0(4) -> 5*
9.59/2.64	    ok0(1) -> 5*
9.59/2.64	    ok0(3) -> 5*
9.59/2.64	    active6(109) -> 112*
9.59/2.64	    active6(93) -> 87*
9.59/2.64	    top0(5) -> 14*
9.59/2.64	    top0(2) -> 14*
9.59/2.64	    top0(4) -> 14*
9.59/2.64	    top0(1) -> 14*
9.59/2.64	    top0(3) -> 14*
9.59/2.64	    mark6(105) -> 86*
9.59/2.64	    top1(36) -> 14*
9.59/2.64	    incr6(104) -> 105*
9.59/2.64	    active1(5) -> 36*
9.59/2.64	    active1(2) -> 36*
9.59/2.64	    active1(4) -> 36*
9.59/2.64	    active1(1) -> 36*
9.59/2.64	    active1(3) -> 36*
9.59/2.64	    top6(112) -> 14*
9.59/2.64	    proper1(5) -> 36*
9.59/2.64	    proper1(2) -> 36*
9.59/2.64	    proper1(4) -> 36*
9.59/2.64	    proper1(1) -> 36*
9.59/2.64	    proper1(3) -> 36*
9.59/2.64	    incr7(142) -> 153*
9.59/2.64	    incr7(122) -> 112*
9.59/2.64	    incr7(117) -> 118*
9.59/2.64	    incr7(146) -> 150*
9.59/2.64	    ok1(25) -> 25,9
9.59/2.64	    ok1(20) -> 36,11
9.59/2.64	    ok1(15) -> 36,11
9.59/2.64	    ok1(29) -> 36,11
9.59/2.64	    ok1(24) -> 24,8
9.59/2.64	    ok1(31) -> 31,12
9.59/2.64	    ok1(21) -> 21,7
9.59/2.64	    ok1(33) -> 33,13
9.59/2.64	    ok1(28) -> 28,10
9.59/2.64	    proper7(104) -> 122*
9.59/2.64	    proper7(74) -> 124*
9.59/2.64	    proper7(96) -> 180*
9.59/2.64	    proper7(118) -> 128*
9.59/2.64	    proper7(103) -> 123*
9.59/2.64	    proper7(73) -> 129*
9.59/2.64	    tl1(5) -> 28*
9.59/2.64	    tl1(2) -> 28*
9.59/2.64	    tl1(4) -> 28*
9.59/2.64	    tl1(1) -> 28*
9.59/2.64	    tl1(3) -> 28*
9.59/2.64	    active7(150) -> 128*
9.59/2.64	    active7(101) -> 119*
9.59/2.64	    hd1(5) -> 25*
9.59/2.64	    hd1(2) -> 25*
9.59/2.64	    hd1(4) -> 25*
9.59/2.64	    hd1(1) -> 25*
9.59/2.64	    hd1(3) -> 25*
9.59/2.64	    mark7(155) -> 128*
9.59/2.64	    mark7(118) -> 112*
9.59/2.64	    s1(5) -> 33*
9.59/2.64	    s1(2) -> 33*
9.59/2.64	    s1(4) -> 33*
9.59/2.64	    s1(1) -> 33*
9.59/2.64	    s1(3) -> 33*
9.59/2.64	    cons7(124,123) -> 122*
9.59/2.64	    cons7(139,147) -> 151*
9.59/2.64	    cons7(154,153) -> 155*
9.59/2.64	    cons7(97,116) -> 117*
9.59/2.64	    incr1(5) -> 24*
9.59/2.64	    incr1(2) -> 24*
9.59/2.64	    incr1(4) -> 24*
9.59/2.64	    incr1(1) -> 24*
9.59/2.64	    incr1(3) -> 24*
9.59/2.64	    top7(128) -> 14*
9.59/2.64	    cons1(3,1) -> 31*
9.59/2.64	    cons1(3,3) -> 31*
9.59/2.64	    cons1(3,5) -> 31*
9.59/2.64	    cons1(4,2) -> 31*
9.59/2.64	    cons1(4,4) -> 31*
9.59/2.64	    cons1(5,1) -> 31*
9.59/2.64	    cons1(5,3) -> 31*
9.59/2.64	    cons1(5,5) -> 31*
9.59/2.64	    cons1(20,15) -> 16*
9.59/2.64	    cons1(1,2) -> 31*
9.59/2.64	    cons1(1,4) -> 31*
9.59/2.64	    cons1(2,1) -> 31*
9.59/2.64	    cons1(2,3) -> 31*
9.59/2.64	    cons1(2,5) -> 31*
9.59/2.64	    cons1(3,2) -> 31*
9.59/2.64	    cons1(3,4) -> 31*
9.59/2.64	    cons1(4,1) -> 31*
9.59/2.64	    cons1(4,3) -> 31*
9.59/2.64	    cons1(4,5) -> 31*
9.59/2.64	    cons1(5,2) -> 31*
9.59/2.64	    cons1(5,4) -> 31*
9.59/2.64	    cons1(1,1) -> 31*
9.59/2.64	    cons1(1,3) -> 31*
9.59/2.64	    cons1(1,5) -> 31*
9.59/2.64	    cons1(2,2) -> 31*
9.59/2.64	    cons1(2,4) -> 31*
9.59/2.64	    incr8(147) -> 166*
9.59/2.64	    incr8(151) -> 159*
9.59/2.64	    incr8(131) -> 128*
9.59/2.64	    incr8(175) -> 173*
9.59/2.64	    adx1(15) -> 16*
9.59/2.64	    adx1(5) -> 21*
9.59/2.64	    adx1(2) -> 21*
9.59/2.64	    adx1(4) -> 21*
9.59/2.64	    adx1(1) -> 21*
9.59/2.64	    adx1(3) -> 21*
9.59/2.64	    proper8(155) -> 162*
9.59/2.64	    proper8(142) -> 175*
9.59/2.64	    proper8(117) -> 131*
9.59/2.64	    proper8(97) -> 134*
9.59/2.64	    proper8(154) -> 174*
9.59/2.64	    proper8(116) -> 133*
9.59/2.64	    proper8(96) -> 138*
9.59/2.64	    proper8(153) -> 173*
9.59/2.64	    proper8(143) -> 192*
9.59/2.64	    01() -> 20*
9.59/2.64	    cons8(186,166) -> 201*
9.59/2.64	    cons8(134,133) -> 131*
9.59/2.64	    cons8(174,173) -> 162*
9.59/2.64	    cons8(167,166) -> 168*
9.59/2.64	    zeros1() -> 15*
9.59/2.64	    06() -> 139*
9.59/2.64	    nats1() -> 29*
9.59/2.64	    adx8(192) -> 188*
9.59/2.64	    adx8(138) -> 133*
9.59/2.64	    adx8(195) -> 200*
9.59/2.64	    mark1(25) -> 25,9
9.59/2.64	    mark1(24) -> 24,8
9.59/2.64	    mark1(21) -> 21,7
9.59/2.64	    mark1(16) -> 36,6
9.59/2.64	    mark1(28) -> 28,10
9.59/2.64	    zeros6() -> 143*
9.59/2.64	    top2(38) -> 14*
9.59/2.64	    ok8(197) -> 182*
9.59/2.64	    ok8(159) -> 128*
9.59/2.64	    ok8(201) -> 162*
9.59/2.64	    ok8(166) -> 173*
9.59/2.64	    ok8(200) -> 188*
9.59/2.64	    active2(20) -> 38*
9.59/2.64	    active2(15) -> 38*
9.59/2.64	    active2(29) -> 38*
9.59/2.64	    active8(159) -> 162*
9.59/2.64	    active8(146) -> 131*
9.59/2.64	    proper2(20) -> 47*
9.59/2.64	    proper2(15) -> 46*
9.59/2.64	    proper2(16) -> 38*
9.59/2.64	    s7(97) -> 154*
9.59/2.64	    s7(139) -> 186*
9.59/2.64	    cons2(47,46) -> 38*
9.59/2.64	    cons2(43,41) -> 42*
9.59/2.64	    top8(162) -> 14*
9.59/2.64	    adx2(46) -> 38*
9.59/2.64	    adx2(41) -> 42*
9.59/2.64	    incr9(169) -> 162*
9.59/2.64	    incr9(188) -> 181*
9.59/2.64	    incr9(200) -> 204*
9.59/2.64	    mark2(42) -> 38*
9.59/2.64	    active9(201) -> 177*
9.59/2.64	    active9(151) -> 169*
9.59/2.64	    02() -> 43*
9.59/2.64	    mark8(168) -> 162*
9.59/2.64	    zeros2() -> 41*
9.59/2.64	    s8(139) -> 167*
9.59/2.64	    s8(134) -> 174*
9.59/2.64	    s8(193) -> 197*
9.59/2.64	    top3(50) -> 14*
9.59/2.64	    top9(177) -> 14*
9.59/2.64	    proper3(42) -> 50*
9.59/2.64	    proper3(41) -> 51*
9.59/2.64	    proper3(43) -> 54*
9.59/2.64	    proper9(167) -> 182*
9.59/2.64	    proper9(147) -> 188*
9.59/2.64	    proper9(139) -> 189*
9.59/2.64	    proper9(166) -> 181*
9.59/2.64	    proper9(168) -> 177*
9.59/2.64	    ok2(41) -> 46*
9.59/2.64	    ok2(43) -> 47*
9.59/2.64	    cons9(197,204) -> 206*
9.59/2.64	    cons9(182,181) -> 177*
9.59/2.64	    ok3(60) -> 54*
9.59/2.64	    ok3(55) -> 38*
9.59/2.64	    ok3(57) -> 51*
9.59/2.64	    s9(189) -> 182*
9.59/2.64	    cons3(43,41) -> 55*
9.59/2.64	    cons3(60,57) -> 65*
9.59/2.64	    cons3(54,51) -> 50*
9.59/2.64	    07() -> 193*
9.59/2.64	    adx3(51) -> 50*
9.59/2.64	    adx3(41) -> 55*
9.59/2.64	    zeros7() -> 195*
9.59/2.64	    active3(55) -> 50*
9.59/2.64	  problem:
9.59/2.64	   
9.59/2.64	  Qed
9.59/2.64	EOF