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