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