YES(?,O(n^1))
739.39/297.10	YES(?,O(n^1))
739.39/297.10	
739.39/297.10	We are left with following problem, upon which TcT provides the
739.39/297.10	certificate YES(?,O(n^1)).
739.39/297.10	
739.39/297.10	Strict Trs:
739.39/297.10	  { active(nats()) -> mark(adx(zeros()))
739.39/297.10	  , active(adx(X)) -> adx(active(X))
739.39/297.10	  , active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
739.39/297.10	  , active(zeros()) -> mark(cons(0(), zeros()))
739.39/297.10	  , active(incr(X)) -> incr(active(X))
739.39/297.10	  , active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
739.39/297.10	  , active(hd(X)) -> hd(active(X))
739.39/297.10	  , active(hd(cons(X, Y))) -> mark(X)
739.39/297.10	  , active(tl(X)) -> tl(active(X))
739.39/297.10	  , active(tl(cons(X, Y))) -> mark(Y)
739.39/297.10	  , adx(mark(X)) -> mark(adx(X))
739.39/297.10	  , adx(ok(X)) -> ok(adx(X))
739.39/297.10	  , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
739.39/297.10	  , incr(mark(X)) -> mark(incr(X))
739.39/297.10	  , incr(ok(X)) -> ok(incr(X))
739.39/297.10	  , s(ok(X)) -> ok(s(X))
739.39/297.10	  , hd(mark(X)) -> mark(hd(X))
739.39/297.10	  , hd(ok(X)) -> ok(hd(X))
739.39/297.10	  , tl(mark(X)) -> mark(tl(X))
739.39/297.10	  , tl(ok(X)) -> ok(tl(X))
739.39/297.10	  , proper(nats()) -> ok(nats())
739.39/297.10	  , proper(adx(X)) -> adx(proper(X))
739.39/297.10	  , proper(zeros()) -> ok(zeros())
739.39/297.10	  , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
739.39/297.10	  , proper(0()) -> ok(0())
739.39/297.10	  , proper(incr(X)) -> incr(proper(X))
739.39/297.10	  , proper(s(X)) -> s(proper(X))
739.39/297.10	  , proper(hd(X)) -> hd(proper(X))
739.39/297.10	  , proper(tl(X)) -> tl(proper(X))
739.39/297.10	  , top(mark(X)) -> top(proper(X))
739.39/297.10	  , top(ok(X)) -> top(active(X)) }
739.39/297.10	Obligation:
739.39/297.10	  runtime complexity
739.39/297.10	Answer:
739.39/297.10	  YES(?,O(n^1))
739.39/297.10	
739.39/297.10	The problem is match-bounded by 10. The enriched problem is
739.39/297.10	compatible with the following automaton.
739.39/297.10	{ active_0(2) -> 1
739.39/297.10	, active_0(3) -> 1
739.39/297.10	, active_0(5) -> 1
739.39/297.10	, active_0(7) -> 1
739.39/297.10	, active_0(13) -> 1
739.39/297.10	, active_1(2) -> 25
739.39/297.10	, active_1(3) -> 25
739.39/297.10	, active_1(5) -> 25
739.39/297.10	, active_1(7) -> 25
739.39/297.10	, active_1(13) -> 25
739.39/297.10	, active_2(16) -> 26
739.39/297.10	, active_2(17) -> 26
739.39/297.10	, active_2(24) -> 26
739.39/297.10	, active_3(33) -> 32
739.39/297.10	, active_4(28) -> 38
739.39/297.10	, active_4(41) -> 42
739.39/297.10	, active_5(35) -> 43
739.39/297.10	, active_5(57) -> 50
739.39/297.10	, active_6(55) -> 51
739.39/297.10	, active_6(62) -> 63
739.39/297.10	, active_7(58) -> 64
739.39/297.10	, active_7(79) -> 69
739.39/297.10	, active_8(78) -> 72
739.39/297.10	, active_8(87) -> 88
739.39/297.10	, active_9(86) -> 89
739.39/297.10	, active_9(107) -> 96
739.39/297.10	, active_10(110) -> 111
739.39/297.10	, nats_0() -> 2
739.39/297.10	, nats_1() -> 24
739.39/297.10	, mark_0(2) -> 3
739.39/297.10	, mark_0(3) -> 3
739.39/297.10	, mark_0(5) -> 3
739.39/297.10	, mark_0(7) -> 3
739.39/297.10	, mark_0(13) -> 3
739.39/297.10	, mark_1(15) -> 1
739.39/297.10	, mark_1(15) -> 25
739.39/297.10	, mark_1(18) -> 4
739.39/297.10	, mark_1(18) -> 18
739.39/297.10	, mark_1(20) -> 8
739.39/297.10	, mark_1(20) -> 20
739.39/297.10	, mark_1(22) -> 10
739.39/297.10	, mark_1(22) -> 22
739.39/297.10	, mark_1(23) -> 11
739.39/297.10	, mark_1(23) -> 23
739.39/297.10	, mark_2(27) -> 26
739.39/297.10	, mark_3(39) -> 38
739.39/297.10	, mark_4(40) -> 32
739.39/297.10	, mark_4(44) -> 43
739.39/297.10	, mark_5(47) -> 42
739.39/297.10	, mark_6(59) -> 50
739.39/297.10	, mark_7(65) -> 63
739.39/297.10	, mark_7(82) -> 69
739.39/297.10	, mark_8(90) -> 88
739.39/297.10	, adx_0(2) -> 4
739.39/297.10	, adx_0(3) -> 4
739.39/297.10	, adx_0(5) -> 4
739.39/297.10	, adx_0(7) -> 4
739.39/297.10	, adx_0(13) -> 4
739.39/297.10	, adx_1(2) -> 18
739.39/297.10	, adx_1(3) -> 18
739.39/297.10	, adx_1(5) -> 18
739.39/297.10	, adx_1(7) -> 18
739.39/297.10	, adx_1(13) -> 18
739.39/297.10	, adx_1(16) -> 15
739.39/297.10	, adx_2(28) -> 27
739.39/297.10	, adx_2(30) -> 26
739.39/297.10	, adx_3(28) -> 33
739.39/297.10	, adx_3(34) -> 32
739.39/297.10	, adx_4(35) -> 41
739.39/297.10	, adx_4(38) -> 32
739.39/297.10	, adx_4(39) -> 40
739.39/297.10	, adx_5(43) -> 42
739.39/297.10	, adx_5(44) -> 47
739.39/297.10	, adx_6(46) -> 61
739.39/297.10	, adx_6(51) -> 50
739.39/297.10	, adx_6(55) -> 57
739.39/297.10	, adx_6(56) -> 77
739.39/297.10	, adx_7(56) -> 67
739.39/297.10	, adx_7(58) -> 62
739.39/297.10	, adx_7(64) -> 63
739.39/297.10	, adx_7(73) -> 71
739.39/297.10	, adx_7(81) -> 85
739.39/297.10	, adx_7(98) -> 95
739.39/297.10	, adx_8(80) -> 75
739.39/297.10	, adx_8(103) -> 101
739.39/297.10	, adx_8(104) -> 106
739.39/297.10	, zeros_0() -> 5
739.39/297.10	, zeros_1() -> 16
739.39/297.10	, zeros_2() -> 28
739.39/297.10	, zeros_3() -> 35
739.39/297.10	, zeros_4() -> 46
739.39/297.10	, zeros_5() -> 56
739.39/297.10	, zeros_6() -> 81
739.39/297.10	, zeros_7() -> 104
739.39/297.10	, cons_0(2, 2) -> 6
739.39/297.10	, cons_0(2, 3) -> 6
739.39/297.10	, cons_0(2, 5) -> 6
739.39/297.10	, cons_0(2, 7) -> 6
739.39/297.10	, cons_0(2, 13) -> 6
739.39/297.10	, cons_0(3, 2) -> 6
739.39/297.10	, cons_0(3, 3) -> 6
739.39/297.10	, cons_0(3, 5) -> 6
739.39/297.10	, cons_0(3, 7) -> 6
739.39/297.10	, cons_0(3, 13) -> 6
739.39/297.10	, cons_0(5, 2) -> 6
739.39/297.10	, cons_0(5, 3) -> 6
739.39/297.10	, cons_0(5, 5) -> 6
739.39/297.10	, cons_0(5, 7) -> 6
739.39/297.10	, cons_0(5, 13) -> 6
739.39/297.10	, cons_0(7, 2) -> 6
739.39/297.10	, cons_0(7, 3) -> 6
739.39/297.10	, cons_0(7, 5) -> 6
739.39/297.10	, cons_0(7, 7) -> 6
739.39/297.10	, cons_0(7, 13) -> 6
739.39/297.10	, cons_0(13, 2) -> 6
739.39/297.10	, cons_0(13, 3) -> 6
739.39/297.10	, cons_0(13, 5) -> 6
739.39/297.10	, cons_0(13, 7) -> 6
739.39/297.10	, cons_0(13, 13) -> 6
739.39/297.10	, cons_1(2, 2) -> 19
739.39/297.10	, cons_1(2, 3) -> 19
739.39/297.10	, cons_1(2, 5) -> 19
739.39/297.10	, cons_1(2, 7) -> 19
739.39/297.10	, cons_1(2, 13) -> 19
739.39/297.10	, cons_1(3, 2) -> 19
739.39/297.10	, cons_1(3, 3) -> 19
739.39/297.10	, cons_1(3, 5) -> 19
739.39/297.10	, cons_1(3, 7) -> 19
739.39/297.10	, cons_1(3, 13) -> 19
739.39/297.10	, cons_1(5, 2) -> 19
739.39/297.10	, cons_1(5, 3) -> 19
739.39/297.10	, cons_1(5, 5) -> 19
739.39/297.10	, cons_1(5, 7) -> 19
739.39/297.10	, cons_1(5, 13) -> 19
739.39/297.10	, cons_1(7, 2) -> 19
739.39/297.10	, cons_1(7, 3) -> 19
739.39/297.10	, cons_1(7, 5) -> 19
739.39/297.10	, cons_1(7, 7) -> 19
739.39/297.10	, cons_1(7, 13) -> 19
739.39/297.10	, cons_1(13, 2) -> 19
739.39/297.10	, cons_1(13, 3) -> 19
739.39/297.10	, cons_1(13, 5) -> 19
739.39/297.10	, cons_1(13, 7) -> 19
739.39/297.10	, cons_1(13, 13) -> 19
739.39/297.10	, cons_1(17, 16) -> 15
739.39/297.10	, cons_2(29, 28) -> 27
739.39/297.10	, cons_2(31, 30) -> 26
739.39/297.10	, cons_3(29, 28) -> 33
739.39/297.10	, cons_3(36, 34) -> 32
739.39/297.10	, cons_3(37, 35) -> 39
739.39/297.10	, cons_4(37, 35) -> 41
739.39/297.10	, cons_4(45, 46) -> 44
739.39/297.10	, cons_4(48, 49) -> 43
739.39/297.10	, cons_5(45, 46) -> 55
739.39/297.10	, cons_5(52, 53) -> 51
739.39/297.10	, cons_6(45, 61) -> 60
739.39/297.10	, cons_6(54, 56) -> 58
739.39/297.10	, cons_6(54, 77) -> 78
739.39/297.10	, cons_7(54, 67) -> 66
739.39/297.10	, cons_7(70, 71) -> 68
739.39/297.10	, cons_7(76, 85) -> 86
739.39/297.10	, cons_7(83, 84) -> 82
739.39/297.10	, cons_8(74, 75) -> 72
739.39/297.10	, cons_8(91, 92) -> 90
739.39/297.10	, cons_8(93, 94) -> 88
739.39/297.10	, cons_8(97, 92) -> 107
739.39/297.10	, cons_9(99, 100) -> 96
739.39/297.10	, cons_9(109, 108) -> 110
739.39/297.10	, 0_0() -> 7
739.39/297.10	, 0_1() -> 17
739.39/297.10	, 0_2() -> 29
739.39/297.10	, 0_3() -> 37
739.39/297.10	, 0_4() -> 45
739.39/297.10	, 0_5() -> 54
739.39/297.10	, 0_6() -> 76
739.39/297.10	, 0_7() -> 105
739.39/297.10	, incr_0(2) -> 8
739.39/297.10	, incr_0(3) -> 8
739.39/297.10	, incr_0(5) -> 8
739.39/297.10	, incr_0(7) -> 8
739.39/297.10	, incr_0(13) -> 8
739.39/297.10	, incr_1(2) -> 20
739.39/297.10	, incr_1(3) -> 20
739.39/297.10	, incr_1(5) -> 20
739.39/297.10	, incr_1(7) -> 20
739.39/297.10	, incr_1(13) -> 20
739.39/297.10	, incr_6(60) -> 59
739.39/297.10	, incr_7(66) -> 65
739.39/297.10	, incr_7(68) -> 63
739.39/297.10	, incr_7(77) -> 84
739.39/297.10	, incr_7(78) -> 79
739.39/297.10	, incr_8(72) -> 69
739.39/297.10	, incr_8(85) -> 92
739.39/297.10	, incr_8(86) -> 87
739.39/297.10	, incr_8(95) -> 94
739.39/297.10	, incr_9(89) -> 88
739.39/297.10	, incr_9(101) -> 100
739.39/297.10	, incr_9(106) -> 108
739.39/297.10	, s_0(2) -> 9
739.39/297.10	, s_0(3) -> 9
739.39/297.10	, s_0(5) -> 9
739.39/297.10	, s_0(7) -> 9
739.39/297.10	, s_0(13) -> 9
739.39/297.10	, s_1(2) -> 21
739.39/297.10	, s_1(3) -> 21
739.39/297.10	, s_1(5) -> 21
739.39/297.10	, s_1(7) -> 21
739.39/297.10	, s_1(13) -> 21
739.39/297.10	, s_7(54) -> 83
739.39/297.10	, s_7(76) -> 97
739.39/297.10	, s_8(74) -> 93
739.39/297.10	, s_8(76) -> 91
739.39/297.10	, s_8(105) -> 109
739.39/297.10	, s_9(102) -> 99
739.39/297.10	, hd_0(2) -> 10
739.39/297.10	, hd_0(3) -> 10
739.39/297.10	, hd_0(5) -> 10
739.39/297.10	, hd_0(7) -> 10
739.39/297.10	, hd_0(13) -> 10
739.39/297.10	, hd_1(2) -> 22
739.39/297.10	, hd_1(3) -> 22
739.39/297.10	, hd_1(5) -> 22
739.39/297.10	, hd_1(7) -> 22
739.39/297.10	, hd_1(13) -> 22
739.39/297.10	, tl_0(2) -> 11
739.39/297.10	, tl_0(3) -> 11
739.39/297.10	, tl_0(5) -> 11
739.39/297.10	, tl_0(7) -> 11
739.39/297.10	, tl_0(13) -> 11
739.39/297.10	, tl_1(2) -> 23
739.39/297.10	, tl_1(3) -> 23
739.39/297.10	, tl_1(5) -> 23
739.39/297.10	, tl_1(7) -> 23
739.39/297.10	, tl_1(13) -> 23
739.39/297.10	, proper_0(2) -> 12
739.39/297.10	, proper_0(3) -> 12
739.39/297.10	, proper_0(5) -> 12
739.39/297.10	, proper_0(7) -> 12
739.39/297.10	, proper_0(13) -> 12
739.39/297.10	, proper_1(2) -> 25
739.39/297.10	, proper_1(3) -> 25
739.39/297.10	, proper_1(5) -> 25
739.39/297.10	, proper_1(7) -> 25
739.39/297.10	, proper_1(13) -> 25
739.39/297.10	, proper_2(15) -> 26
739.39/297.10	, proper_2(16) -> 30
739.39/297.10	, proper_2(17) -> 31
739.39/297.10	, proper_3(27) -> 32
739.39/297.10	, proper_3(28) -> 34
739.39/297.10	, proper_3(29) -> 36
739.39/297.10	, proper_4(35) -> 49
739.39/297.10	, proper_4(37) -> 48
739.39/297.10	, proper_4(40) -> 42
739.39/297.10	, proper_5(39) -> 43
739.39/297.10	, proper_5(45) -> 52
739.39/297.10	, proper_5(46) -> 53
739.39/297.10	, proper_5(47) -> 50
739.39/297.10	, proper_6(44) -> 51
739.39/297.10	, proper_6(59) -> 63
739.39/297.10	, proper_7(45) -> 70
739.39/297.10	, proper_7(46) -> 73
739.39/297.10	, proper_7(56) -> 98
739.39/297.10	, proper_7(60) -> 68
739.39/297.10	, proper_7(61) -> 71
739.39/297.10	, proper_7(65) -> 69
739.39/297.10	, proper_8(54) -> 74
739.39/297.10	, proper_8(56) -> 80
739.39/297.10	, proper_8(66) -> 72
739.39/297.10	, proper_8(67) -> 75
739.39/297.10	, proper_8(77) -> 95
739.39/297.10	, proper_8(81) -> 103
739.39/297.10	, proper_8(82) -> 88
739.39/297.10	, proper_8(83) -> 93
739.39/297.10	, proper_8(84) -> 94
739.39/297.10	, proper_9(76) -> 102
739.39/297.10	, proper_9(85) -> 101
739.39/297.10	, proper_9(90) -> 96
739.39/297.10	, proper_9(91) -> 99
739.39/297.10	, proper_9(92) -> 100
739.39/297.10	, ok_0(2) -> 13
739.39/297.10	, ok_0(3) -> 13
739.39/297.10	, ok_0(5) -> 13
739.39/297.10	, ok_0(7) -> 13
739.39/297.10	, ok_0(13) -> 13
739.39/297.10	, ok_1(16) -> 12
739.39/297.10	, ok_1(16) -> 25
739.39/297.10	, ok_1(17) -> 12
739.39/297.10	, ok_1(17) -> 25
739.39/297.10	, ok_1(18) -> 4
739.39/297.10	, ok_1(18) -> 18
739.39/297.10	, ok_1(19) -> 6
739.39/297.10	, ok_1(19) -> 19
739.39/297.10	, ok_1(20) -> 8
739.39/297.10	, ok_1(20) -> 20
739.39/297.10	, ok_1(21) -> 9
739.39/297.10	, ok_1(21) -> 21
739.39/297.10	, ok_1(22) -> 10
739.39/297.10	, ok_1(22) -> 22
739.39/297.10	, ok_1(23) -> 11
739.39/297.10	, ok_1(23) -> 23
739.39/297.10	, ok_1(24) -> 12
739.39/297.10	, ok_1(24) -> 25
739.39/297.10	, ok_2(28) -> 30
739.39/297.10	, ok_2(29) -> 31
739.39/297.10	, ok_3(33) -> 26
739.39/297.10	, ok_3(35) -> 34
739.39/297.10	, ok_3(37) -> 36
739.39/297.10	, ok_4(41) -> 32
739.39/297.10	, ok_4(45) -> 48
739.39/297.10	, ok_4(46) -> 49
739.39/297.10	, ok_5(54) -> 52
739.39/297.10	, ok_5(54) -> 70
739.39/297.10	, ok_5(55) -> 43
739.39/297.10	, ok_5(56) -> 53
739.39/297.10	, ok_5(56) -> 73
739.39/297.10	, ok_6(57) -> 42
739.39/297.10	, ok_6(58) -> 51
739.39/297.10	, ok_6(76) -> 74
739.39/297.10	, ok_6(77) -> 71
739.39/297.10	, ok_6(78) -> 68
739.39/297.10	, ok_6(81) -> 80
739.39/297.10	, ok_6(81) -> 98
739.39/297.10	, ok_7(62) -> 50
739.39/297.10	, ok_7(79) -> 63
739.39/297.10	, ok_7(85) -> 75
739.39/297.10	, ok_7(85) -> 95
739.39/297.10	, ok_7(86) -> 72
739.39/297.10	, ok_7(97) -> 93
739.39/297.10	, ok_7(104) -> 103
739.39/297.10	, ok_7(105) -> 102
739.39/297.10	, ok_8(87) -> 69
739.39/297.10	, ok_8(92) -> 94
739.39/297.10	, ok_8(106) -> 101
739.39/297.10	, ok_8(107) -> 88
739.39/297.10	, ok_8(109) -> 99
739.39/297.10	, ok_9(108) -> 100
739.39/297.10	, ok_9(110) -> 96
739.39/297.10	, top_0(2) -> 14
739.39/297.10	, top_0(3) -> 14
739.39/297.10	, top_0(5) -> 14
739.39/297.10	, top_0(7) -> 14
739.39/297.10	, top_0(13) -> 14
739.39/297.10	, top_1(25) -> 14
739.39/297.10	, top_2(26) -> 14
739.39/297.10	, top_3(32) -> 14
739.39/297.10	, top_4(42) -> 14
739.39/297.10	, top_5(50) -> 14
739.39/297.10	, top_6(63) -> 14
739.39/297.10	, top_7(69) -> 14
739.39/297.10	, top_8(88) -> 14
739.39/297.10	, top_9(96) -> 14
739.39/297.10	, top_10(111) -> 14 }
739.39/297.10	
739.39/297.10	Hurray, we answered YES(?,O(n^1))
739.39/297.10	EOF