YES(?,O(n^1))
1183.58/297.12	YES(?,O(n^1))
1183.58/297.12	
1183.58/297.12	We are left with following problem, upon which TcT provides the
1183.58/297.12	certificate YES(?,O(n^1)).
1183.58/297.12	
1183.58/297.12	Strict Trs:
1183.58/297.12	  { active(nats()) -> mark(cons(0(), incr(nats())))
1183.58/297.12	  , active(cons(X1, X2)) -> cons(active(X1), X2)
1183.58/297.12	  , active(incr(X)) -> incr(active(X))
1183.58/297.12	  , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
1183.58/297.12	  , active(pairs()) -> mark(cons(0(), incr(odds())))
1183.58/297.12	  , active(odds()) -> mark(incr(pairs()))
1183.58/297.12	  , active(s(X)) -> s(active(X))
1183.58/297.12	  , active(head(X)) -> head(active(X))
1183.58/297.12	  , active(head(cons(X, XS))) -> mark(X)
1183.58/297.12	  , active(tail(X)) -> tail(active(X))
1183.58/297.12	  , active(tail(cons(X, XS))) -> mark(XS)
1183.58/297.12	  , cons(mark(X1), X2) -> mark(cons(X1, X2))
1183.58/297.12	  , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
1183.58/297.12	  , incr(mark(X)) -> mark(incr(X))
1183.58/297.12	  , incr(ok(X)) -> ok(incr(X))
1183.58/297.12	  , s(mark(X)) -> mark(s(X))
1183.58/297.12	  , s(ok(X)) -> ok(s(X))
1183.58/297.12	  , head(mark(X)) -> mark(head(X))
1183.58/297.12	  , head(ok(X)) -> ok(head(X))
1183.58/297.12	  , tail(mark(X)) -> mark(tail(X))
1183.58/297.12	  , tail(ok(X)) -> ok(tail(X))
1183.58/297.12	  , proper(nats()) -> ok(nats())
1183.58/297.12	  , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
1183.58/297.12	  , proper(0()) -> ok(0())
1183.58/297.12	  , proper(incr(X)) -> incr(proper(X))
1183.58/297.12	  , proper(pairs()) -> ok(pairs())
1183.58/297.12	  , proper(odds()) -> ok(odds())
1183.58/297.12	  , proper(s(X)) -> s(proper(X))
1183.58/297.12	  , proper(head(X)) -> head(proper(X))
1183.58/297.12	  , proper(tail(X)) -> tail(proper(X))
1183.58/297.12	  , top(mark(X)) -> top(proper(X))
1183.58/297.12	  , top(ok(X)) -> top(active(X)) }
1183.58/297.12	Obligation:
1183.58/297.12	  innermost runtime complexity
1183.58/297.12	Answer:
1183.58/297.12	  YES(?,O(n^1))
1183.58/297.12	
1183.58/297.12	The problem is match-bounded by 9. The enriched problem is
1183.58/297.12	compatible with the following automaton.
1183.58/297.12	{ active_0(2) -> 1
1183.58/297.12	, active_0(3) -> 1
1183.58/297.12	, active_0(5) -> 1
1183.58/297.12	, active_0(7) -> 1
1183.58/297.12	, active_0(8) -> 1
1183.58/297.12	, active_0(13) -> 1
1183.58/297.12	, active_1(2) -> 25
1183.58/297.12	, active_1(3) -> 25
1183.58/297.12	, active_1(5) -> 25
1183.58/297.12	, active_1(7) -> 25
1183.58/297.12	, active_1(8) -> 25
1183.58/297.12	, active_1(13) -> 25
1183.58/297.12	, active_2(16) -> 26
1183.58/297.12	, active_2(18) -> 26
1183.58/297.12	, active_2(19) -> 26
1183.58/297.12	, active_3(38) -> 36
1183.58/297.12	, active_4(28) -> 53
1183.58/297.12	, active_4(31) -> 46
1183.58/297.12	, active_4(50) -> 52
1183.58/297.12	, active_5(41) -> 61
1183.58/297.12	, active_5(44) -> 54
1183.58/297.12	, active_5(74) -> 60
1183.58/297.12	, active_6(56) -> 81
1183.58/297.12	, active_6(72) -> 65
1183.58/297.12	, active_6(79) -> 80
1183.58/297.12	, active_7(69) -> 91
1183.58/297.12	, active_7(78) -> 82
1183.58/297.12	, active_7(103) -> 90
1183.58/297.12	, active_8(97) -> 105
1183.58/297.12	, active_8(98) -> 109
1183.58/297.12	, active_8(106) -> 107
1183.58/297.12	, active_9(102) -> 108
1183.58/297.12	, nats_0() -> 2
1183.58/297.12	, nats_1() -> 18
1183.58/297.12	, nats_2() -> 30
1183.58/297.12	, nats_3() -> 45
1183.58/297.12	, nats_4() -> 58
1183.58/297.12	, nats_5() -> 71
1183.58/297.12	, nats_6() -> 100
1183.58/297.12	, mark_0(2) -> 3
1183.58/297.12	, mark_0(3) -> 3
1183.58/297.12	, mark_0(5) -> 3
1183.58/297.12	, mark_0(7) -> 3
1183.58/297.12	, mark_0(8) -> 3
1183.58/297.12	, mark_0(13) -> 3
1183.58/297.12	, mark_1(15) -> 1
1183.58/297.12	, mark_1(15) -> 25
1183.58/297.12	, mark_1(20) -> 4
1183.58/297.12	, mark_1(20) -> 20
1183.58/297.12	, mark_1(21) -> 6
1183.58/297.12	, mark_1(21) -> 21
1183.58/297.12	, mark_1(22) -> 9
1183.58/297.12	, mark_1(22) -> 22
1183.58/297.12	, mark_1(23) -> 10
1183.58/297.12	, mark_1(23) -> 23
1183.58/297.12	, mark_1(24) -> 11
1183.58/297.12	, mark_1(24) -> 24
1183.58/297.12	, mark_2(27) -> 26
1183.58/297.12	, mark_3(47) -> 46
1183.58/297.12	, mark_4(49) -> 36
1183.58/297.12	, mark_4(55) -> 54
1183.58/297.12	, mark_5(59) -> 52
1183.58/297.12	, mark_6(75) -> 60
1183.58/297.12	, mark_7(83) -> 80
1183.58/297.12	, cons_0(2, 2) -> 4
1183.58/297.12	, cons_0(2, 3) -> 4
1183.58/297.12	, cons_0(2, 5) -> 4
1183.58/297.12	, cons_0(2, 7) -> 4
1183.58/297.12	, cons_0(2, 8) -> 4
1183.58/297.12	, cons_0(2, 13) -> 4
1183.58/297.12	, cons_0(3, 2) -> 4
1183.58/297.12	, cons_0(3, 3) -> 4
1183.58/297.12	, cons_0(3, 5) -> 4
1183.58/297.12	, cons_0(3, 7) -> 4
1183.58/297.12	, cons_0(3, 8) -> 4
1183.58/297.12	, cons_0(3, 13) -> 4
1183.58/297.12	, cons_0(5, 2) -> 4
1183.58/297.12	, cons_0(5, 3) -> 4
1183.58/297.12	, cons_0(5, 5) -> 4
1183.58/297.12	, cons_0(5, 7) -> 4
1183.58/297.12	, cons_0(5, 8) -> 4
1183.58/297.12	, cons_0(5, 13) -> 4
1183.58/297.12	, cons_0(7, 2) -> 4
1183.58/297.12	, cons_0(7, 3) -> 4
1183.58/297.12	, cons_0(7, 5) -> 4
1183.58/297.12	, cons_0(7, 7) -> 4
1183.58/297.12	, cons_0(7, 8) -> 4
1183.58/297.12	, cons_0(7, 13) -> 4
1183.58/297.12	, cons_0(8, 2) -> 4
1183.58/297.12	, cons_0(8, 3) -> 4
1183.58/297.12	, cons_0(8, 5) -> 4
1183.58/297.12	, cons_0(8, 7) -> 4
1183.58/297.12	, cons_0(8, 8) -> 4
1183.58/297.12	, cons_0(8, 13) -> 4
1183.58/297.12	, cons_0(13, 2) -> 4
1183.58/297.12	, cons_0(13, 3) -> 4
1183.58/297.12	, cons_0(13, 5) -> 4
1183.58/297.12	, cons_0(13, 7) -> 4
1183.58/297.12	, cons_0(13, 8) -> 4
1183.58/297.12	, cons_0(13, 13) -> 4
1183.58/297.12	, cons_1(2, 2) -> 20
1183.58/297.12	, cons_1(2, 3) -> 20
1183.58/297.12	, cons_1(2, 5) -> 20
1183.58/297.12	, cons_1(2, 7) -> 20
1183.58/297.12	, cons_1(2, 8) -> 20
1183.58/297.12	, cons_1(2, 13) -> 20
1183.58/297.12	, cons_1(3, 2) -> 20
1183.58/297.12	, cons_1(3, 3) -> 20
1183.58/297.12	, cons_1(3, 5) -> 20
1183.58/297.12	, cons_1(3, 7) -> 20
1183.58/297.12	, cons_1(3, 8) -> 20
1183.58/297.12	, cons_1(3, 13) -> 20
1183.58/297.12	, cons_1(5, 2) -> 20
1183.58/297.12	, cons_1(5, 3) -> 20
1183.58/297.12	, cons_1(5, 5) -> 20
1183.58/297.12	, cons_1(5, 7) -> 20
1183.58/297.12	, cons_1(5, 8) -> 20
1183.58/297.12	, cons_1(5, 13) -> 20
1183.58/297.12	, cons_1(7, 2) -> 20
1183.58/297.12	, cons_1(7, 3) -> 20
1183.58/297.12	, cons_1(7, 5) -> 20
1183.58/297.12	, cons_1(7, 7) -> 20
1183.58/297.12	, cons_1(7, 8) -> 20
1183.58/297.12	, cons_1(7, 13) -> 20
1183.58/297.12	, cons_1(8, 2) -> 20
1183.58/297.12	, cons_1(8, 3) -> 20
1183.58/297.12	, cons_1(8, 5) -> 20
1183.58/297.12	, cons_1(8, 7) -> 20
1183.58/297.12	, cons_1(8, 8) -> 20
1183.58/297.12	, cons_1(8, 13) -> 20
1183.58/297.12	, cons_1(13, 2) -> 20
1183.58/297.12	, cons_1(13, 3) -> 20
1183.58/297.12	, cons_1(13, 5) -> 20
1183.58/297.12	, cons_1(13, 7) -> 20
1183.58/297.12	, cons_1(13, 8) -> 20
1183.58/297.12	, cons_1(13, 13) -> 20
1183.58/297.12	, cons_1(16, 17) -> 15
1183.58/297.12	, cons_2(28, 29) -> 27
1183.58/297.12	, cons_2(32, 33) -> 26
1183.58/297.12	, cons_3(28, 37) -> 38
1183.58/297.12	, cons_3(39, 40) -> 36
1183.58/297.12	, cons_3(41, 48) -> 47
1183.58/297.12	, cons_4(41, 51) -> 50
1183.58/297.12	, cons_4(53, 37) -> 36
1183.58/297.12	, cons_4(56, 57) -> 55
1183.58/297.12	, cons_4(62, 63) -> 54
1183.58/297.12	, cons_5(56, 66) -> 72
1183.58/297.12	, cons_5(61, 51) -> 52
1183.58/297.12	, cons_5(67, 68) -> 65
1183.58/297.12	, cons_6(69, 73) -> 78
1183.58/297.12	, cons_6(76, 77) -> 75
1183.58/297.12	, cons_6(81, 66) -> 65
1183.58/297.12	, cons_7(84, 85) -> 83
1183.58/297.12	, cons_7(86, 87) -> 80
1183.58/297.12	, cons_7(91, 73) -> 82
1183.58/297.12	, cons_7(97, 85) -> 103
1183.58/297.12	, cons_8(92, 93) -> 90
1183.58/297.12	, cons_8(102, 104) -> 106
1183.58/297.12	, cons_8(105, 85) -> 90
1183.58/297.12	, cons_9(108, 104) -> 107
1183.58/297.12	, 0_0() -> 5
1183.58/297.12	, 0_1() -> 16
1183.58/297.12	, 0_2() -> 28
1183.58/297.12	, 0_3() -> 41
1183.58/297.12	, 0_4() -> 56
1183.58/297.12	, 0_5() -> 69
1183.58/297.12	, 0_6() -> 98
1183.58/297.12	, incr_0(2) -> 6
1183.58/297.12	, incr_0(3) -> 6
1183.58/297.12	, incr_0(5) -> 6
1183.58/297.12	, incr_0(7) -> 6
1183.58/297.12	, incr_0(8) -> 6
1183.58/297.12	, incr_0(13) -> 6
1183.58/297.12	, incr_1(2) -> 21
1183.58/297.12	, incr_1(3) -> 21
1183.58/297.12	, incr_1(5) -> 21
1183.58/297.12	, incr_1(7) -> 21
1183.58/297.12	, incr_1(8) -> 21
1183.58/297.12	, incr_1(13) -> 21
1183.58/297.12	, incr_1(18) -> 17
1183.58/297.12	, incr_1(19) -> 15
1183.58/297.12	, incr_2(30) -> 29
1183.58/297.12	, incr_2(31) -> 27
1183.58/297.12	, incr_2(34) -> 33
1183.58/297.12	, incr_2(35) -> 26
1183.58/297.12	, incr_3(30) -> 37
1183.58/297.12	, incr_3(31) -> 38
1183.58/297.12	, incr_3(42) -> 40
1183.58/297.12	, incr_3(43) -> 36
1183.58/297.12	, incr_3(45) -> 48
1183.58/297.12	, incr_4(44) -> 50
1183.58/297.12	, incr_4(45) -> 51
1183.58/297.12	, incr_4(46) -> 36
1183.58/297.12	, incr_4(47) -> 49
1183.58/297.12	, incr_4(58) -> 57
1183.58/297.12	, incr_4(64) -> 63
1183.58/297.12	, incr_5(54) -> 52
1183.58/297.12	, incr_5(55) -> 59
1183.58/297.12	, incr_5(58) -> 66
1183.58/297.12	, incr_5(70) -> 68
1183.58/297.12	, incr_6(65) -> 60
1183.58/297.12	, incr_6(66) -> 77
1183.58/297.12	, incr_6(71) -> 73
1183.58/297.12	, incr_6(72) -> 74
1183.58/297.12	, incr_6(94) -> 88
1183.58/297.12	, incr_7(73) -> 85
1183.58/297.12	, incr_7(78) -> 79
1183.58/297.12	, incr_7(82) -> 80
1183.58/297.12	, incr_7(88) -> 87
1183.58/297.12	, incr_7(99) -> 95
1183.58/297.12	, incr_7(100) -> 101
1183.58/297.12	, incr_8(95) -> 93
1183.58/297.12	, incr_8(101) -> 104
1183.58/297.12	, pairs_0() -> 7
1183.58/297.12	, pairs_1() -> 19
1183.58/297.12	, pairs_2() -> 31
1183.58/297.12	, pairs_3() -> 44
1183.58/297.12	, odds_0() -> 8
1183.58/297.12	, odds_1() -> 18
1183.58/297.12	, odds_2() -> 30
1183.58/297.12	, odds_3() -> 45
1183.58/297.12	, odds_4() -> 58
1183.58/297.12	, odds_5() -> 71
1183.58/297.12	, odds_6() -> 100
1183.58/297.12	, s_0(2) -> 9
1183.58/297.12	, s_0(3) -> 9
1183.58/297.12	, s_0(5) -> 9
1183.58/297.12	, s_0(7) -> 9
1183.58/297.12	, s_0(8) -> 9
1183.58/297.12	, s_0(13) -> 9
1183.58/297.12	, s_1(2) -> 22
1183.58/297.12	, s_1(3) -> 22
1183.58/297.12	, s_1(5) -> 22
1183.58/297.12	, s_1(7) -> 22
1183.58/297.12	, s_1(8) -> 22
1183.58/297.12	, s_1(13) -> 22
1183.58/297.12	, s_6(56) -> 76
1183.58/297.12	, s_6(69) -> 97
1183.58/297.12	, s_7(69) -> 84
1183.58/297.12	, s_7(89) -> 86
1183.58/297.12	, s_7(91) -> 105
1183.58/297.12	, s_7(98) -> 102
1183.58/297.12	, s_8(96) -> 92
1183.58/297.12	, s_8(109) -> 108
1183.58/297.12	, head_0(2) -> 10
1183.58/297.12	, head_0(3) -> 10
1183.58/297.12	, head_0(5) -> 10
1183.58/297.12	, head_0(7) -> 10
1183.58/297.12	, head_0(8) -> 10
1183.58/297.12	, head_0(13) -> 10
1183.58/297.12	, head_1(2) -> 23
1183.58/297.12	, head_1(3) -> 23
1183.58/297.12	, head_1(5) -> 23
1183.58/297.12	, head_1(7) -> 23
1183.58/297.12	, head_1(8) -> 23
1183.58/297.12	, head_1(13) -> 23
1183.58/297.12	, tail_0(2) -> 11
1183.58/297.12	, tail_0(3) -> 11
1183.58/297.12	, tail_0(5) -> 11
1183.58/297.12	, tail_0(7) -> 11
1183.58/297.12	, tail_0(8) -> 11
1183.58/297.12	, tail_0(13) -> 11
1183.58/297.12	, tail_1(2) -> 24
1183.58/297.12	, tail_1(3) -> 24
1183.58/297.12	, tail_1(5) -> 24
1183.58/297.12	, tail_1(7) -> 24
1183.58/297.12	, tail_1(8) -> 24
1183.58/297.12	, tail_1(13) -> 24
1183.58/297.12	, proper_0(2) -> 12
1183.58/297.12	, proper_0(3) -> 12
1183.58/297.12	, proper_0(5) -> 12
1183.58/297.12	, proper_0(7) -> 12
1183.58/297.12	, proper_0(8) -> 12
1183.58/297.12	, proper_0(13) -> 12
1183.58/297.12	, proper_1(2) -> 25
1183.58/297.12	, proper_1(3) -> 25
1183.58/297.12	, proper_1(5) -> 25
1183.58/297.12	, proper_1(7) -> 25
1183.58/297.12	, proper_1(8) -> 25
1183.58/297.12	, proper_1(13) -> 25
1183.58/297.12	, proper_2(15) -> 26
1183.58/297.12	, proper_2(16) -> 32
1183.58/297.12	, proper_2(17) -> 33
1183.58/297.12	, proper_2(18) -> 34
1183.58/297.12	, proper_2(19) -> 35
1183.58/297.12	, proper_3(27) -> 36
1183.58/297.12	, proper_3(28) -> 39
1183.58/297.12	, proper_3(29) -> 40
1183.58/297.12	, proper_3(30) -> 42
1183.58/297.12	, proper_3(31) -> 43
1183.58/297.12	, proper_4(41) -> 62
1183.58/297.12	, proper_4(45) -> 64
1183.58/297.12	, proper_4(48) -> 63
1183.58/297.12	, proper_4(49) -> 52
1183.58/297.12	, proper_5(47) -> 54
1183.58/297.12	, proper_5(56) -> 67
1183.58/297.12	, proper_5(57) -> 68
1183.58/297.12	, proper_5(58) -> 70
1183.58/297.12	, proper_5(59) -> 60
1183.58/297.12	, proper_6(55) -> 65
1183.58/297.12	, proper_6(58) -> 94
1183.58/297.12	, proper_6(75) -> 80
1183.58/297.12	, proper_7(56) -> 89
1183.58/297.12	, proper_7(66) -> 88
1183.58/297.12	, proper_7(71) -> 99
1183.58/297.12	, proper_7(76) -> 86
1183.58/297.12	, proper_7(77) -> 87
1183.58/297.12	, proper_7(83) -> 90
1183.58/297.12	, proper_8(69) -> 96
1183.58/297.12	, proper_8(73) -> 95
1183.58/297.12	, proper_8(84) -> 92
1183.58/297.12	, proper_8(85) -> 93
1183.58/297.12	, ok_0(2) -> 13
1183.58/297.12	, ok_0(3) -> 13
1183.58/297.12	, ok_0(5) -> 13
1183.58/297.12	, ok_0(7) -> 13
1183.58/297.12	, ok_0(8) -> 13
1183.58/297.12	, ok_0(13) -> 13
1183.58/297.12	, ok_1(16) -> 12
1183.58/297.12	, ok_1(16) -> 25
1183.58/297.12	, ok_1(18) -> 12
1183.58/297.12	, ok_1(18) -> 25
1183.58/297.12	, ok_1(19) -> 12
1183.58/297.12	, ok_1(19) -> 25
1183.58/297.12	, ok_1(20) -> 4
1183.58/297.12	, ok_1(20) -> 20
1183.58/297.12	, ok_1(21) -> 6
1183.58/297.12	, ok_1(21) -> 21
1183.58/297.12	, ok_1(22) -> 9
1183.58/297.12	, ok_1(22) -> 22
1183.58/297.12	, ok_1(23) -> 10
1183.58/297.12	, ok_1(23) -> 23
1183.58/297.12	, ok_1(24) -> 11
1183.58/297.12	, ok_1(24) -> 24
1183.58/297.12	, ok_2(28) -> 32
1183.58/297.12	, ok_2(30) -> 34
1183.58/297.12	, ok_2(31) -> 35
1183.58/297.12	, ok_3(37) -> 33
1183.58/297.12	, ok_3(38) -> 26
1183.58/297.12	, ok_3(41) -> 39
1183.58/297.12	, ok_3(44) -> 43
1183.58/297.12	, ok_3(45) -> 42
1183.58/297.12	, ok_4(50) -> 36
1183.58/297.12	, ok_4(51) -> 40
1183.58/297.12	, ok_4(56) -> 62
1183.58/297.12	, ok_4(58) -> 64
1183.58/297.12	, ok_5(66) -> 63
1183.58/297.12	, ok_5(69) -> 67
1183.58/297.12	, ok_5(69) -> 89
1183.58/297.12	, ok_5(71) -> 70
1183.58/297.12	, ok_5(71) -> 94
1183.58/297.12	, ok_5(72) -> 54
1183.58/297.12	, ok_6(73) -> 68
1183.58/297.12	, ok_6(73) -> 88
1183.58/297.12	, ok_6(74) -> 52
1183.58/297.12	, ok_6(78) -> 65
1183.58/297.12	, ok_6(97) -> 86
1183.58/297.12	, ok_6(98) -> 96
1183.58/297.12	, ok_6(100) -> 99
1183.58/297.12	, ok_7(79) -> 60
1183.58/297.12	, ok_7(85) -> 87
1183.58/297.12	, ok_7(101) -> 95
1183.58/297.12	, ok_7(102) -> 92
1183.58/297.12	, ok_7(103) -> 80
1183.58/297.12	, ok_8(104) -> 93
1183.58/297.12	, ok_8(106) -> 90
1183.58/297.12	, top_0(2) -> 14
1183.58/297.12	, top_0(3) -> 14
1183.58/297.12	, top_0(5) -> 14
1183.58/297.12	, top_0(7) -> 14
1183.58/297.12	, top_0(8) -> 14
1183.58/297.12	, top_0(13) -> 14
1183.58/297.12	, top_1(25) -> 14
1183.58/297.12	, top_2(26) -> 14
1183.58/297.12	, top_3(36) -> 14
1183.58/297.12	, top_4(52) -> 14
1183.58/297.12	, top_5(60) -> 14
1183.58/297.12	, top_6(80) -> 14
1183.58/297.12	, top_7(90) -> 14
1183.58/297.12	, top_8(107) -> 14 }
1183.58/297.12	
1183.58/297.12	Hurray, we answered YES(?,O(n^1))
1183.90/297.21	EOF