*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        dec(Cons(Cons(x,xs),Nil())) -> dec(Nil())
        dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs))
        dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs))
        dec(Cons(Nil(),Nil())) -> Nil()
        goal(x) -> nestdec(x)
        isNilNil(Cons(Cons(x,xs),Nil())) -> False()
        isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False()
        isNilNil(Cons(Nil(),Cons(x,xs))) -> False()
        isNilNil(Cons(Nil(),Nil())) -> True()
        nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs)))
        nestdec(Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))))))))))))))))
        number17(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))))))))))))))))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0}
      Obligation:
        Innermost
        basic terms: {dec,goal,isNilNil,nestdec,number17}/{Cons,False,Nil,True}
    Applied Processor:
      Bounds {initialAutomaton = perSymbol, enrichment = match}
    Proof:
      The problem is match-bounded by 2.
      The enriched problem is compatible with follwoing automaton.
        Cons_0(1,1) -> 1
        Cons_0(1,2) -> 1
        Cons_0(1,3) -> 1
        Cons_0(1,4) -> 1
        Cons_0(2,1) -> 1
        Cons_0(2,2) -> 1
        Cons_0(2,3) -> 1
        Cons_0(2,4) -> 1
        Cons_0(3,1) -> 1
        Cons_0(3,2) -> 1
        Cons_0(3,3) -> 1
        Cons_0(3,4) -> 1
        Cons_0(4,1) -> 1
        Cons_0(4,2) -> 1
        Cons_0(4,3) -> 1
        Cons_0(4,4) -> 1
        Cons_1(1,1) -> 10
        Cons_1(1,2) -> 10
        Cons_1(1,3) -> 10
        Cons_1(1,4) -> 10
        Cons_1(2,1) -> 10
        Cons_1(2,2) -> 10
        Cons_1(2,3) -> 10
        Cons_1(2,4) -> 10
        Cons_1(3,1) -> 10
        Cons_1(3,2) -> 10
        Cons_1(3,3) -> 10
        Cons_1(3,4) -> 10
        Cons_1(4,1) -> 10
        Cons_1(4,2) -> 10
        Cons_1(4,3) -> 10
        Cons_1(4,4) -> 10
        Cons_1(10,10) -> 26
        Cons_1(10,11) -> 6
        Cons_1(10,11) -> 8
        Cons_1(10,11) -> 9
        Cons_1(10,12) -> 11
        Cons_1(10,13) -> 12
        Cons_1(10,14) -> 13
        Cons_1(10,15) -> 14
        Cons_1(10,16) -> 15
        Cons_1(10,17) -> 16
        Cons_1(10,18) -> 17
        Cons_1(10,19) -> 18
        Cons_1(10,20) -> 19
        Cons_1(10,21) -> 20
        Cons_1(10,22) -> 21
        Cons_1(10,23) -> 22
        Cons_1(10,24) -> 23
        Cons_1(10,25) -> 24
        Cons_1(10,26) -> 25
        Cons_2(27,28) -> 6
        Cons_2(29,30) -> 28
        Cons_2(31,32) -> 30
        Cons_2(33,34) -> 32
        Cons_2(35,36) -> 34
        Cons_2(37,38) -> 36
        Cons_2(39,40) -> 38
        Cons_2(41,42) -> 40
        Cons_2(43,44) -> 42
        Cons_2(45,46) -> 44
        Cons_2(47,48) -> 46
        Cons_2(49,50) -> 48
        Cons_2(51,52) -> 50
        Cons_2(53,54) -> 52
        Cons_2(55,56) -> 54
        Cons_2(57,58) -> 56
        Cons_2(59,60) -> 58
        Cons_2(60,28) -> 8
        False_0() -> 2
        False_1() -> 7
        Nil_0() -> 3
        Nil_1() -> 5
        Nil_1() -> 10
        Nil_2() -> 27
        Nil_2() -> 29
        Nil_2() -> 31
        Nil_2() -> 33
        Nil_2() -> 35
        Nil_2() -> 37
        Nil_2() -> 39
        Nil_2() -> 41
        Nil_2() -> 43
        Nil_2() -> 45
        Nil_2() -> 47
        Nil_2() -> 49
        Nil_2() -> 51
        Nil_2() -> 53
        Nil_2() -> 55
        Nil_2() -> 57
        Nil_2() -> 59
        Nil_2() -> 60
        True_0() -> 4
        True_1() -> 7
        dec_0(1) -> 5
        dec_0(2) -> 5
        dec_0(3) -> 5
        dec_0(4) -> 5
        dec_1(10) -> 5
        goal_0(1) -> 6
        goal_0(2) -> 6
        goal_0(3) -> 6
        goal_0(4) -> 6
        isNilNil_0(1) -> 7
        isNilNil_0(2) -> 7
        isNilNil_0(3) -> 7
        isNilNil_0(4) -> 7
        nestdec_0(1) -> 8
        nestdec_0(2) -> 8
        nestdec_0(3) -> 8
        nestdec_0(4) -> 8
        nestdec_1(1) -> 6
        nestdec_1(2) -> 6
        nestdec_1(3) -> 6
        nestdec_1(4) -> 6
        nestdec_1(5) -> 6
        nestdec_1(5) -> 8
        number17_0(1) -> 9
        number17_0(2) -> 9
        number17_0(3) -> 9
        number17_0(4) -> 9
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        dec(Cons(Cons(x,xs),Nil())) -> dec(Nil())
        dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs))
        dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs))
        dec(Cons(Nil(),Nil())) -> Nil()
        goal(x) -> nestdec(x)
        isNilNil(Cons(Cons(x,xs),Nil())) -> False()
        isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False()
        isNilNil(Cons(Nil(),Cons(x,xs))) -> False()
        isNilNil(Cons(Nil(),Nil())) -> True()
        nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs)))
        nestdec(Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))))))))))))))))
        number17(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))))))))))))))))
      Signature:
        {dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0}
      Obligation:
        Innermost
        basic terms: {dec,goal,isNilNil,nestdec,number17}/{Cons,False,Nil,True}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).