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