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