*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        0() -> n__0()
        activate(X) -> X
        activate(n__0()) -> 0()
        activate(n__s(X)) -> s(X)
        div(0(),n__s(Y)) -> 0()
        div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0())
        geq(X,n__0()) -> true()
        geq(n__0(),n__s(Y)) -> false()
        geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
        if(false(),X,Y) -> activate(Y)
        if(true(),X,Y) -> activate(X)
        minus(n__0(),Y) -> 0()
        minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
        s(X) -> n__s(X)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__s/1,true/0}
      Obligation:
        Innermost
        basic terms: {0,activate,div,geq,if,minus,s}/{false,n__0,n__s,true}
    Applied Processor:
      InnermostRuleRemoval
    Proof:
      Arguments of following rules are not normal-forms.
        div(0(),n__s(Y)) -> 0()
        div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0())
      All above mentioned rules can be savely removed.
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        0() -> n__0()
        activate(X) -> X
        activate(n__0()) -> 0()
        activate(n__s(X)) -> s(X)
        geq(X,n__0()) -> true()
        geq(n__0(),n__s(Y)) -> false()
        geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
        if(false(),X,Y) -> activate(Y)
        if(true(),X,Y) -> activate(X)
        minus(n__0(),Y) -> 0()
        minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
        s(X) -> n__s(X)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__s/1,true/0}
      Obligation:
        Innermost
        basic terms: {0,activate,div,geq,if,minus,s}/{false,n__0,n__s,true}
    Applied Processor:
      Bounds {initialAutomaton = minimal, enrichment = match}
    Proof:
      The problem is match-bounded by 4.
      The enriched problem is compatible with follwoing automaton.
        0_0() -> 1
        0_1() -> 1
        0_1() -> 3
        0_1() -> 4
        0_1() -> 5
        0_1() -> 6
        0_1() -> 7
        0_1() -> 8
        0_2() -> 1
        0_3() -> 1
        activate_0(2) -> 1
        activate_1(2) -> 1
        activate_1(2) -> 3
        activate_1(2) -> 4
        activate_2(2) -> 5
        activate_2(2) -> 6
        activate_3(2) -> 7
        activate_3(2) -> 8
        div_0(2,2) -> 1
        false_0() -> 1
        false_0() -> 2
        false_0() -> 3
        false_0() -> 4
        false_0() -> 5
        false_0() -> 6
        false_0() -> 7
        false_0() -> 8
        false_1() -> 1
        false_2() -> 1
        false_3() -> 1
        geq_0(2,2) -> 1
        geq_1(3,4) -> 1
        geq_2(5,6) -> 1
        geq_3(7,8) -> 1
        if_0(2,2,2) -> 1
        minus_0(2,2) -> 1
        minus_1(4,4) -> 1
        minus_2(6,6) -> 1
        minus_3(8,8) -> 1
        n__0_0() -> 1
        n__0_0() -> 2
        n__0_0() -> 3
        n__0_0() -> 4
        n__0_0() -> 5
        n__0_0() -> 6
        n__0_0() -> 7
        n__0_0() -> 8
        n__0_1() -> 1
        n__0_2() -> 1
        n__0_2() -> 3
        n__0_2() -> 4
        n__0_2() -> 5
        n__0_2() -> 6
        n__0_2() -> 7
        n__0_2() -> 8
        n__0_3() -> 1
        n__0_4() -> 1
        n__s_0(2) -> 1
        n__s_0(2) -> 2
        n__s_0(2) -> 3
        n__s_0(2) -> 4
        n__s_0(2) -> 5
        n__s_0(2) -> 6
        n__s_0(2) -> 7
        n__s_0(2) -> 8
        n__s_1(2) -> 1
        n__s_2(2) -> 1
        n__s_2(2) -> 3
        n__s_2(2) -> 4
        n__s_2(2) -> 5
        n__s_2(2) -> 6
        n__s_2(2) -> 7
        n__s_2(2) -> 8
        s_0(2) -> 1
        s_1(2) -> 1
        s_1(2) -> 3
        s_1(2) -> 4
        s_1(2) -> 5
        s_1(2) -> 6
        s_1(2) -> 7
        s_1(2) -> 8
        true_0() -> 1
        true_0() -> 2
        true_0() -> 3
        true_0() -> 4
        true_0() -> 5
        true_0() -> 6
        true_0() -> 7
        true_0() -> 8
        true_1() -> 1
        true_2() -> 1
        true_3() -> 1
        2 -> 1
        2 -> 3
        2 -> 4
        2 -> 5
        2 -> 6
        2 -> 7
        2 -> 8
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        0() -> n__0()
        activate(X) -> X
        activate(n__0()) -> 0()
        activate(n__s(X)) -> s(X)
        geq(X,n__0()) -> true()
        geq(n__0(),n__s(Y)) -> false()
        geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
        if(false(),X,Y) -> activate(Y)
        if(true(),X,Y) -> activate(X)
        minus(n__0(),Y) -> 0()
        minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
        s(X) -> n__s(X)
      Signature:
        {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__s/1,true/0}
      Obligation:
        Innermost
        basic terms: {0,activate,div,geq,if,minus,s}/{false,n__0,n__s,true}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).