WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1
            ,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark
            ,minus_active} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          div_active#(x,y) -> c_1()
          div_active#(0(),s(y)) -> c_2()
          div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
          ge_active#(x,y) -> c_4()
          ge_active#(x,0()) -> c_5()
          ge_active#(0(),s(y)) -> c_6()
          ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
          if_active#(x,y,z) -> c_8()
          if_active#(false(),x,y) -> c_9(mark#(y))
          if_active#(true(),x,y) -> c_10(mark#(x))
          mark#(0()) -> c_11()
          mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
          mark#(ge(x,y)) -> c_13(ge_active#(x,y))
          mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
          mark#(minus(x,y)) -> c_15(minus_active#(x,y))
          mark#(s(x)) -> c_16(mark#(x))
          minus_active#(x,y) -> c_17()
          minus_active#(0(),y) -> c_18()
          minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            div_active#(x,y) -> c_1()
            div_active#(0(),s(y)) -> c_2()
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
            ge_active#(x,y) -> c_4()
            ge_active#(x,0()) -> c_5()
            ge_active#(0(),s(y)) -> c_6()
            ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
            if_active#(x,y,z) -> c_8()
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
            mark#(0()) -> c_11()
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(ge(x,y)) -> c_13(ge_active#(x,y))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
            mark#(minus(x,y)) -> c_15(minus_active#(x,y))
            mark#(s(x)) -> c_16(mark#(x))
            minus_active#(x,y) -> c_17()
            minus_active#(0(),y) -> c_18()
            minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,4,5,6,8,11,17,18}
        by application of
          Pre({1,2,4,5,6,8,11,17,18}) = {3,7,9,10,12,13,14,15,16,19}.
        Here rules are labelled as follows:
          1: div_active#(x,y) -> c_1()
          2: div_active#(0(),s(y)) -> c_2()
          3: div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
          4: ge_active#(x,y) -> c_4()
          5: ge_active#(x,0()) -> c_5()
          6: ge_active#(0(),s(y)) -> c_6()
          7: ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
          8: if_active#(x,y,z) -> c_8()
          9: if_active#(false(),x,y) -> c_9(mark#(y))
          10: if_active#(true(),x,y) -> c_10(mark#(x))
          11: mark#(0()) -> c_11()
          12: mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
          13: mark#(ge(x,y)) -> c_13(ge_active#(x,y))
          14: mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
          15: mark#(minus(x,y)) -> c_15(minus_active#(x,y))
          16: mark#(s(x)) -> c_16(mark#(x))
          17: minus_active#(x,y) -> c_17()
          18: minus_active#(0(),y) -> c_18()
          19: minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
            ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(ge(x,y)) -> c_13(ge_active#(x,y))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
            mark#(minus(x,y)) -> c_15(minus_active#(x,y))
            mark#(s(x)) -> c_16(mark#(x))
            minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        - Weak DPs:
            div_active#(x,y) -> c_1()
            div_active#(0(),s(y)) -> c_2()
            ge_active#(x,y) -> c_4()
            ge_active#(x,0()) -> c_5()
            ge_active#(0(),s(y)) -> c_6()
            if_active#(x,y,z) -> c_8()
            mark#(0()) -> c_11()
            minus_active#(x,y) -> c_17()
            minus_active#(0(),y) -> c_18()
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
             -->_1 if_active#(true(),x,y) -> c_10(mark#(x)):4
             -->_1 if_active#(false(),x,y) -> c_9(mark#(y)):3
             -->_2 ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y)):2
             -->_1 if_active#(x,y,z) -> c_8():16
             -->_2 ge_active#(0(),s(y)) -> c_6():15
             -->_2 ge_active#(x,0()) -> c_5():14
             -->_2 ge_active#(x,y) -> c_4():13
          
          2:S:ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
             -->_1 ge_active#(0(),s(y)) -> c_6():15
             -->_1 ge_active#(x,0()) -> c_5():14
             -->_1 ge_active#(x,y) -> c_4():13
             -->_1 ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y)):2
          
          3:S:if_active#(false(),x,y) -> c_9(mark#(y))
             -->_1 mark#(s(x)) -> c_16(mark#(x)):9
             -->_1 mark#(minus(x,y)) -> c_15(minus_active#(x,y)):8
             -->_1 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):7
             -->_1 mark#(ge(x,y)) -> c_13(ge_active#(x,y)):6
             -->_1 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):5
             -->_1 mark#(0()) -> c_11():17
          
          4:S:if_active#(true(),x,y) -> c_10(mark#(x))
             -->_1 mark#(s(x)) -> c_16(mark#(x)):9
             -->_1 mark#(minus(x,y)) -> c_15(minus_active#(x,y)):8
             -->_1 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):7
             -->_1 mark#(ge(x,y)) -> c_13(ge_active#(x,y)):6
             -->_1 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):5
             -->_1 mark#(0()) -> c_11():17
          
          5:S:mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
             -->_2 mark#(s(x)) -> c_16(mark#(x)):9
             -->_2 mark#(minus(x,y)) -> c_15(minus_active#(x,y)):8
             -->_2 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):7
             -->_2 mark#(ge(x,y)) -> c_13(ge_active#(x,y)):6
             -->_2 mark#(0()) -> c_11():17
             -->_1 div_active#(0(),s(y)) -> c_2():12
             -->_1 div_active#(x,y) -> c_1():11
             -->_2 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):5
             -->_1 div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
                                                ,ge_active#(x,y)):1
          
          6:S:mark#(ge(x,y)) -> c_13(ge_active#(x,y))
             -->_1 ge_active#(0(),s(y)) -> c_6():15
             -->_1 ge_active#(x,0()) -> c_5():14
             -->_1 ge_active#(x,y) -> c_4():13
             -->_1 ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y)):2
          
          7:S:mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
             -->_2 mark#(s(x)) -> c_16(mark#(x)):9
             -->_2 mark#(minus(x,y)) -> c_15(minus_active#(x,y)):8
             -->_2 mark#(0()) -> c_11():17
             -->_1 if_active#(x,y,z) -> c_8():16
             -->_2 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):7
             -->_2 mark#(ge(x,y)) -> c_13(ge_active#(x,y)):6
             -->_2 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):5
             -->_1 if_active#(true(),x,y) -> c_10(mark#(x)):4
             -->_1 if_active#(false(),x,y) -> c_9(mark#(y)):3
          
          8:S:mark#(minus(x,y)) -> c_15(minus_active#(x,y))
             -->_1 minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y)):10
             -->_1 minus_active#(0(),y) -> c_18():19
             -->_1 minus_active#(x,y) -> c_17():18
          
          9:S:mark#(s(x)) -> c_16(mark#(x))
             -->_1 mark#(0()) -> c_11():17
             -->_1 mark#(s(x)) -> c_16(mark#(x)):9
             -->_1 mark#(minus(x,y)) -> c_15(minus_active#(x,y)):8
             -->_1 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):7
             -->_1 mark#(ge(x,y)) -> c_13(ge_active#(x,y)):6
             -->_1 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):5
          
          10:S:minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
             -->_1 minus_active#(0(),y) -> c_18():19
             -->_1 minus_active#(x,y) -> c_17():18
             -->_1 minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y)):10
          
          11:W:div_active#(x,y) -> c_1()
             
          
          12:W:div_active#(0(),s(y)) -> c_2()
             
          
          13:W:ge_active#(x,y) -> c_4()
             
          
          14:W:ge_active#(x,0()) -> c_5()
             
          
          15:W:ge_active#(0(),s(y)) -> c_6()
             
          
          16:W:if_active#(x,y,z) -> c_8()
             
          
          17:W:mark#(0()) -> c_11()
             
          
          18:W:minus_active#(x,y) -> c_17()
             
          
          19:W:minus_active#(0(),y) -> c_18()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          11: div_active#(x,y) -> c_1()
          12: div_active#(0(),s(y)) -> c_2()
          13: ge_active#(x,y) -> c_4()
          14: ge_active#(x,0()) -> c_5()
          15: ge_active#(0(),s(y)) -> c_6()
          16: if_active#(x,y,z) -> c_8()
          18: minus_active#(x,y) -> c_17()
          19: minus_active#(0(),y) -> c_18()
          17: mark#(0()) -> c_11()
* Step 4: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
            ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(ge(x,y)) -> c_13(ge_active#(x,y))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
            mark#(minus(x,y)) -> c_15(minus_active#(x,y))
            mark#(s(x)) -> c_16(mark#(x))
            minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
          if_active#(false(),x,y) -> c_9(mark#(y))
          if_active#(true(),x,y) -> c_10(mark#(x))
          mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
          mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
          mark#(s(x)) -> c_16(mark#(x))
        and a lower component
          ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
          mark#(ge(x,y)) -> c_13(ge_active#(x,y))
          mark#(minus(x,y)) -> c_15(minus_active#(x,y))
          minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        Further, following extension rules are added to the lower component.
          div_active#(s(x),s(y)) -> ge_active#(x,y)
          div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          if_active#(false(),x,y) -> mark#(y)
          if_active#(true(),x,y) -> mark#(x)
          mark#(div(x,y)) -> div_active#(mark(x),y)
          mark#(div(x,y)) -> mark#(x)
          mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
          mark#(if(x,y,z)) -> mark#(x)
          mark#(s(x)) -> mark#(x)
** Step 4.a:1: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
            mark#(s(x)) -> c_16(mark#(x))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()),ge_active#(x,y))
             -->_1 if_active#(true(),x,y) -> c_10(mark#(x)):3
             -->_1 if_active#(false(),x,y) -> c_9(mark#(y)):2
          
          2:S:if_active#(false(),x,y) -> c_9(mark#(y))
             -->_1 mark#(s(x)) -> c_16(mark#(x)):6
             -->_1 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):5
             -->_1 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):4
          
          3:S:if_active#(true(),x,y) -> c_10(mark#(x))
             -->_1 mark#(s(x)) -> c_16(mark#(x)):6
             -->_1 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):5
             -->_1 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):4
          
          4:S:mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
             -->_2 mark#(s(x)) -> c_16(mark#(x)):6
             -->_2 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):5
             -->_2 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):4
             -->_1 div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
                                                ,ge_active#(x,y)):1
          
          5:S:mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
             -->_2 mark#(s(x)) -> c_16(mark#(x)):6
             -->_2 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):5
             -->_2 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):4
             -->_1 if_active#(true(),x,y) -> c_10(mark#(x)):3
             -->_1 if_active#(false(),x,y) -> c_9(mark#(y)):2
          
          6:S:mark#(s(x)) -> c_16(mark#(x))
             -->_1 mark#(s(x)) -> c_16(mark#(x)):6
             -->_1 mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x)):5
             -->_1 mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
** Step 4.a:2: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
            mark#(s(x)) -> c_16(mark#(x))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(div_active) = {1},
            uargs(if_active) = {1},
            uargs(s) = {1},
            uargs(div_active#) = {1},
            uargs(if_active#) = {1},
            uargs(c_3) = {1},
            uargs(c_9) = {1},
            uargs(c_10) = {1},
            uargs(c_12) = {1,2},
            uargs(c_14) = {1,2},
            uargs(c_16) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                        p(0) = [0]                  
                      p(div) = [0]                  
               p(div_active) = [1] x1 + [0]         
                    p(false) = [0]                  
                       p(ge) = [0]                  
                p(ge_active) = [0]                  
                       p(if) = [0]                  
                p(if_active) = [1] x1 + [0]         
                     p(mark) = [0]                  
                    p(minus) = [0]                  
             p(minus_active) = [0]                  
                        p(s) = [1] x1 + [0]         
                     p(true) = [0]                  
              p(div_active#) = [1] x1 + [5]         
               p(ge_active#) = [0]                  
               p(if_active#) = [1] x1 + [5]         
                    p(mark#) = [0]                  
            p(minus_active#) = [0]                  
                      p(c_1) = [0]                  
                      p(c_2) = [0]                  
                      p(c_3) = [1] x1 + [0]         
                      p(c_4) = [0]                  
                      p(c_5) = [0]                  
                      p(c_6) = [0]                  
                      p(c_7) = [0]                  
                      p(c_8) = [0]                  
                      p(c_9) = [1] x1 + [4]         
                     p(c_10) = [1] x1 + [0]         
                     p(c_11) = [0]                  
                     p(c_12) = [1] x1 + [1] x2 + [1]
                     p(c_13) = [1] x1 + [4]         
                     p(c_14) = [1] x1 + [1] x2 + [2]
                     p(c_15) = [1] x1 + [0]         
                     p(c_16) = [1] x1 + [4]         
                     p(c_17) = [0]                  
                     p(c_18) = [2]                  
                     p(c_19) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
          if_active#(false(),x,y) = [5]           
                                  > [4]           
                                  = c_9(mark#(y)) 
          
           if_active#(true(),x,y) = [5]           
                                  > [0]           
                                  = c_10(mark#(x))
          
          
          Following rules are (at-least) weakly oriented:
           div_active#(s(x),s(y)) =  [1] x + [5]                                                
                                  >= [5]                                                        
                                  =  c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
          
                  mark#(div(x,y)) =  [0]                                                        
                                  >= [6]                                                        
                                  =  c_12(div_active#(mark(x),y),mark#(x))                      
          
                 mark#(if(x,y,z)) =  [0]                                                        
                                  >= [7]                                                        
                                  =  c_14(if_active#(mark(x),y,z),mark#(x))                     
          
                      mark#(s(x)) =  [0]                                                        
                                  >= [4]                                                        
                                  =  c_16(mark#(x))                                             
          
                  div_active(x,y) =  [1] x + [0]                                                
                                  >= [0]                                                        
                                  =  div(x,y)                                                   
          
             div_active(0(),s(y)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  0()                                                        
          
            div_active(s(x),s(y)) =  [1] x + [0]                                                
                                  >= [0]                                                        
                                  =  if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())      
          
                   ge_active(x,y) =  [0]                                                        
                                  >= [0]                                                        
                                  =  ge(x,y)                                                    
          
                 ge_active(x,0()) =  [0]                                                        
                                  >= [0]                                                        
                                  =  true()                                                     
          
              ge_active(0(),s(y)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  false()                                                    
          
             ge_active(s(x),s(y)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  ge_active(x,y)                                             
          
                 if_active(x,y,z) =  [1] x + [0]                                                
                                  >= [0]                                                        
                                  =  if(x,y,z)                                                  
          
           if_active(false(),x,y) =  [0]                                                        
                                  >= [0]                                                        
                                  =  mark(y)                                                    
          
            if_active(true(),x,y) =  [0]                                                        
                                  >= [0]                                                        
                                  =  mark(x)                                                    
          
                        mark(0()) =  [0]                                                        
                                  >= [0]                                                        
                                  =  0()                                                        
          
                   mark(div(x,y)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  div_active(mark(x),y)                                      
          
                    mark(ge(x,y)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  ge_active(x,y)                                             
          
                  mark(if(x,y,z)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  if_active(mark(x),y,z)                                     
          
                 mark(minus(x,y)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  minus_active(x,y)                                          
          
                       mark(s(x)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  s(mark(x))                                                 
          
                minus_active(x,y) =  [0]                                                        
                                  >= [0]                                                        
                                  =  minus(x,y)                                                 
          
              minus_active(0(),y) =  [0]                                                        
                                  >= [0]                                                        
                                  =  0()                                                        
          
          minus_active(s(x),s(y)) =  [0]                                                        
                                  >= [0]                                                        
                                  =  minus_active(x,y)                                          
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 4.a:3: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
            mark#(s(x)) -> c_16(mark#(x))
        - Weak DPs:
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(div_active) = {1},
            uargs(if_active) = {1},
            uargs(s) = {1},
            uargs(div_active#) = {1},
            uargs(if_active#) = {1},
            uargs(c_3) = {1},
            uargs(c_9) = {1},
            uargs(c_10) = {1},
            uargs(c_12) = {1,2},
            uargs(c_14) = {1,2},
            uargs(c_16) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                        p(0) = [0]                  
                      p(div) = [0]                  
               p(div_active) = [1] x1 + [0]         
                    p(false) = [0]                  
                       p(ge) = [0]                  
                p(ge_active) = [0]                  
                       p(if) = [0]                  
                p(if_active) = [1] x1 + [0]         
                     p(mark) = [0]                  
                    p(minus) = [0]                  
             p(minus_active) = [0]                  
                        p(s) = [1] x1 + [0]         
                     p(true) = [0]                  
              p(div_active#) = [1] x1 + [4]         
               p(ge_active#) = [1] x1 + [0]         
               p(if_active#) = [1] x1 + [1]         
                    p(mark#) = [1]                  
            p(minus_active#) = [1] x1 + [1] x2 + [4]
                      p(c_1) = [1]                  
                      p(c_2) = [0]                  
                      p(c_3) = [1] x1 + [0]         
                      p(c_4) = [1]                  
                      p(c_5) = [1]                  
                      p(c_6) = [1]                  
                      p(c_7) = [1]                  
                      p(c_8) = [1]                  
                      p(c_9) = [1] x1 + [0]         
                     p(c_10) = [1] x1 + [0]         
                     p(c_11) = [0]                  
                     p(c_12) = [1] x1 + [1] x2 + [7]
                     p(c_13) = [1] x1 + [1]         
                     p(c_14) = [1] x1 + [1] x2 + [4]
                     p(c_15) = [1] x1 + [1]         
                     p(c_16) = [1] x1 + [7]         
                     p(c_17) = [1]                  
                     p(c_18) = [0]                  
                     p(c_19) = [1] x1 + [2]         
          
          Following rules are strictly oriented:
          div_active#(s(x),s(y)) = [1] x + [4]                                                
                                 > [1]                                                        
                                 = c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
          
          
          Following rules are (at-least) weakly oriented:
          if_active#(false(),x,y) =  [1]                                                  
                                  >= [1]                                                  
                                  =  c_9(mark#(y))                                        
          
           if_active#(true(),x,y) =  [1]                                                  
                                  >= [1]                                                  
                                  =  c_10(mark#(x))                                       
          
                  mark#(div(x,y)) =  [1]                                                  
                                  >= [12]                                                 
                                  =  c_12(div_active#(mark(x),y),mark#(x))                
          
                 mark#(if(x,y,z)) =  [1]                                                  
                                  >= [6]                                                  
                                  =  c_14(if_active#(mark(x),y,z),mark#(x))               
          
                      mark#(s(x)) =  [1]                                                  
                                  >= [8]                                                  
                                  =  c_16(mark#(x))                                       
          
                  div_active(x,y) =  [1] x + [0]                                          
                                  >= [0]                                                  
                                  =  div(x,y)                                             
          
             div_active(0(),s(y)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  0()                                                  
          
            div_active(s(x),s(y)) =  [1] x + [0]                                          
                                  >= [0]                                                  
                                  =  if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          
                   ge_active(x,y) =  [0]                                                  
                                  >= [0]                                                  
                                  =  ge(x,y)                                              
          
                 ge_active(x,0()) =  [0]                                                  
                                  >= [0]                                                  
                                  =  true()                                               
          
              ge_active(0(),s(y)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  false()                                              
          
             ge_active(s(x),s(y)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  ge_active(x,y)                                       
          
                 if_active(x,y,z) =  [1] x + [0]                                          
                                  >= [0]                                                  
                                  =  if(x,y,z)                                            
          
           if_active(false(),x,y) =  [0]                                                  
                                  >= [0]                                                  
                                  =  mark(y)                                              
          
            if_active(true(),x,y) =  [0]                                                  
                                  >= [0]                                                  
                                  =  mark(x)                                              
          
                        mark(0()) =  [0]                                                  
                                  >= [0]                                                  
                                  =  0()                                                  
          
                   mark(div(x,y)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  div_active(mark(x),y)                                
          
                    mark(ge(x,y)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  ge_active(x,y)                                       
          
                  mark(if(x,y,z)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  if_active(mark(x),y,z)                               
          
                 mark(minus(x,y)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  minus_active(x,y)                                    
          
                       mark(s(x)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  s(mark(x))                                           
          
                minus_active(x,y) =  [0]                                                  
                                  >= [0]                                                  
                                  =  minus(x,y)                                           
          
              minus_active(0(),y) =  [0]                                                  
                                  >= [0]                                                  
                                  =  0()                                                  
          
          minus_active(s(x),s(y)) =  [0]                                                  
                                  >= [0]                                                  
                                  =  minus_active(x,y)                                    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 4.a:4: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
            mark#(s(x)) -> c_16(mark#(x))
        - Weak DPs:
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_3) = {1},
          uargs(c_9) = {1},
          uargs(c_10) = {1},
          uargs(c_12) = {1,2},
          uargs(c_14) = {1,2},
          uargs(c_16) = {1}
        
        Following symbols are considered usable:
          {div_active#,ge_active#,if_active#,mark#,minus_active#}
        TcT has computed the following interpretation:
                      p(0) = [0]                           
                    p(div) = [1] x1 + [0]                  
             p(div_active) = [0]                           
                  p(false) = [6]                           
                     p(ge) = [2]                           
              p(ge_active) = [4] x1 + [6] x2 + [4]         
                     p(if) = [1] x1 + [1] x2 + [1] x3 + [4]
              p(if_active) = [1] x1 + [2]                  
                   p(mark) = [0]                           
                  p(minus) = [0]                           
           p(minus_active) = [4] x2 + [0]                  
                      p(s) = [1] x1 + [0]                  
                   p(true) = [4]                           
            p(div_active#) = [0]                           
             p(ge_active#) = [1] x1 + [1]                  
             p(if_active#) = [1] x2 + [1] x3 + [0]         
                  p(mark#) = [1] x1 + [0]                  
          p(minus_active#) = [2] x2 + [0]                  
                    p(c_1) = [0]                           
                    p(c_2) = [1]                           
                    p(c_3) = [4] x1 + [0]                  
                    p(c_4) = [1]                           
                    p(c_5) = [4]                           
                    p(c_6) = [4]                           
                    p(c_7) = [1] x1 + [1]                  
                    p(c_8) = [0]                           
                    p(c_9) = [1] x1 + [0]                  
                   p(c_10) = [1] x1 + [0]                  
                   p(c_11) = [1]                           
                   p(c_12) = [4] x1 + [1] x2 + [0]         
                   p(c_13) = [0]                           
                   p(c_14) = [1] x1 + [1] x2 + [3]         
                   p(c_15) = [1] x1 + [0]                  
                   p(c_16) = [1] x1 + [0]                  
                   p(c_17) = [0]                           
                   p(c_18) = [1]                           
                   p(c_19) = [4] x1 + [0]                  
        
        Following rules are strictly oriented:
        mark#(if(x,y,z)) = [1] x + [1] y + [1] z + [4]           
                         > [1] x + [1] y + [1] z + [3]           
                         = c_14(if_active#(mark(x),y,z),mark#(x))
        
        
        Following rules are (at-least) weakly oriented:
         div_active#(s(x),s(y)) =  [0]                                                        
                                >= [0]                                                        
                                =  c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
        
        if_active#(false(),x,y) =  [1] x + [1] y + [0]                                        
                                >= [1] y + [0]                                                
                                =  c_9(mark#(y))                                              
        
         if_active#(true(),x,y) =  [1] x + [1] y + [0]                                        
                                >= [1] x + [0]                                                
                                =  c_10(mark#(x))                                             
        
                mark#(div(x,y)) =  [1] x + [0]                                                
                                >= [1] x + [0]                                                
                                =  c_12(div_active#(mark(x),y),mark#(x))                      
        
                    mark#(s(x)) =  [1] x + [0]                                                
                                >= [1] x + [0]                                                
                                =  c_16(mark#(x))                                             
        
** Step 4.a:5: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(s(x)) -> c_16(mark#(x))
        - Weak DPs:
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(8, 0)
          0 :: [] -(0)-> "A"(0, 0)
          0 :: [] -(0)-> "A"(15, 7)
          0 :: [] -(0)-> "A"(13, 5)
          0 :: [] -(0)-> "A"(14, 14)
          div :: ["A"(8, 8) x "A"(0, 0)] -(8)-> "A"(0, 8)
          div :: ["A"(8, 0) x "A"(0, 0)] -(0)-> "A"(8, 0)
          div :: ["A"(10, 0) x "A"(0, 0)] -(0)-> "A"(10, 0)
          div :: ["A"(12, 8) x "A"(0, 0)] -(8)-> "A"(4, 8)
          div_active :: ["A"(8, 0) x "A"(0, 0)] -(0)-> "A"(8, 0)
          false :: [] -(0)-> "A"(8, 0)
          false :: [] -(0)-> "A"(5, 0)
          false :: [] -(0)-> "A"(15, 14)
          ge :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(8, 0)
          ge :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(14, 14)
          ge_active :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(14, 12)
          if :: ["A"(8, 0) x "A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0)
          if :: ["A"(8, 8) x "A"(8, 8) x "A"(8, 8)] -(0)-> "A"(0, 8)
          if_active :: ["A"(8, 0) x "A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0)
          mark :: ["A"(8, 0)] -(0)-> "A"(8, 0)
          minus :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(8, 0)
          minus :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(15, 11)
          minus :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(14, 6)
          minus :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(14, 13)
          minus_active :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(11, 3)
          s :: ["A"(0, 8)] -(0)-> "A"(0, 8)
          s :: ["A"(0, 0)] -(0)-> "A"(0, 0)
          s :: ["A"(8, 0)] -(8)-> "A"(8, 0)
          true :: [] -(0)-> "A"(8, 0)
          true :: [] -(0)-> "A"(5, 0)
          true :: [] -(0)-> "A"(15, 14)
          div_active# :: ["A"(8, 0) x "A"(0, 0)] -(0)-> "A"(1, 1)
          if_active# :: ["A"(5, 0) x "A"(0, 8) x "A"(8, 8)] -(0)-> "A"(3, 11)
          mark# :: ["A"(0, 8)] -(0)-> "A"(8, 1)
          c_3 :: ["A"(0, 8)] -(0)-> "A"(1, 8)
          c_9 :: ["A"(0, 0)] -(0)-> "A"(3, 15)
          c_10 :: ["A"(0, 0)] -(0)-> "A"(7, 14)
          c_12 :: ["A"(0, 0) x "A"(2, 0)] -(2)-> "A"(9, 2)
          c_14 :: ["A"(0, 8) x "A"(0, 0)] -(0)-> "A"(15, 8)
          c_16 :: ["A"(2, 0)] -(0)-> "A"(12, 2)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1, 0)
          "0_A" :: [] -(0)-> "A"(0, 1)
          "c_10_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_10_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "c_12_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
          "c_12_A" :: ["A"(0) x "A"(0)] -(1)-> "A"(0, 1)
          "c_14_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
          "c_14_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
          "c_16_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_16_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "c_9_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_9_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "div_A" :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          "div_A" :: ["A"(1, 1) x "A"(0, 0)] -(1)-> "A"(0, 1)
          "false_A" :: [] -(0)-> "A"(1, 0)
          "false_A" :: [] -(0)-> "A"(0, 1)
          "ge_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          "ge_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1)
          "if_A" :: ["A"(1, 0) x "A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
          "if_A" :: ["A"(1, 1) x "A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1)
          "minus_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          "minus_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1)
          "s_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0)
          "s_A" :: ["A"(0, 1)] -(0)-> "A"(0, 1)
          "true_A" :: [] -(0)-> "A"(1, 0)
          "true_A" :: [] -(0)-> "A"(0, 1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
        2. Weak:
          mark#(s(x)) -> c_16(mark#(x))
** Step 4.a:6: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            mark#(s(x)) -> c_16(mark#(x))
        - Weak DPs:
            div_active#(s(x),s(y)) -> c_3(if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()))
            if_active#(false(),x,y) -> c_9(mark#(y))
            if_active#(true(),x,y) -> c_10(mark#(x))
            mark#(div(x,y)) -> c_12(div_active#(mark(x),y),mark#(x))
            mark#(if(x,y,z)) -> c_14(if_active#(mark(x),y,z),mark#(x))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(1, 0)
          0 :: [] -(0)-> "A"(0, 0)
          0 :: [] -(0)-> "A"(7, 7)
          0 :: [] -(0)-> "A"(13, 13)
          0 :: [] -(0)-> "A"(6, 6)
          div :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          div :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1)
          div :: ["A"(2, 0) x "A"(0, 0)] -(0)-> "A"(2, 0)
          div_active :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          false :: [] -(0)-> "A"(1, 0)
          false :: [] -(0)-> "A"(0, 0)
          false :: [] -(0)-> "A"(15, 14)
          ge :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          ge :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(12, 13)
          ge_active :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(9, 12)
          if :: ["A"(1, 0) x "A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
          if :: ["A"(1, 1) x "A"(0, 1) x "A"(0, 1)] -(1)-> "A"(0, 1)
          if_active :: ["A"(1, 0) x "A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
          mark :: ["A"(1, 0)] -(0)-> "A"(1, 0)
          minus :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          minus :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(9, 4)
          minus :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(9, 8)
          minus :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(3, 2)
          minus_active :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(7, 7)
          s :: ["A"(0, 1)] -(1)-> "A"(0, 1)
          s :: ["A"(0, 0)] -(0)-> "A"(0, 0)
          s :: ["A"(1, 0)] -(1)-> "A"(1, 0)
          true :: [] -(0)-> "A"(1, 0)
          true :: [] -(0)-> "A"(0, 0)
          true :: [] -(0)-> "A"(15, 14)
          div_active# :: ["A"(1, 0) x "A"(0, 1)] -(1)-> "A"(1, 1)
          if_active# :: ["A"(0, 0) x "A"(0, 1) x "A"(0, 1)] -(0)-> "A"(5, 13)
          mark# :: ["A"(0, 1)] -(0)-> "A"(1, 0)
          c_3 :: ["A"(4, 3)] -(0)-> "A"(1, 3)
          c_9 :: ["A"(0, 0)] -(0)-> "A"(5, 15)
          c_10 :: ["A"(0, 0)] -(0)-> "A"(14, 13)
          c_12 :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(7, 1)
          c_14 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(3, 0)
          c_16 :: ["A"(1, 0)] -(0)-> "A"(1, 4)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1, 0)
          "0_A" :: [] -(0)-> "A"(0, 1)
          "c_10_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_10_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "c_12_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
          "c_12_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
          "c_14_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
          "c_14_A" :: ["A"(0) x "A"(0)] -(1)-> "A"(0, 1)
          "c_16_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_16_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "c_9_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_9_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "div_A" :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          "div_A" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1)
          "false_A" :: [] -(0)-> "A"(1, 0)
          "false_A" :: [] -(0)-> "A"(0, 1)
          "ge_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          "ge_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1)
          "if_A" :: ["A"(1, 0) x "A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
          "if_A" :: ["A"(1, 1) x "A"(0, 1) x "A"(0, 1)] -(1)-> "A"(0, 1)
          "minus_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          "minus_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1)
          "s_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0)
          "s_A" :: ["A"(0, 1)] -(1)-> "A"(0, 1)
          "true_A" :: [] -(0)-> "A"(1, 0)
          "true_A" :: [] -(0)-> "A"(0, 1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          mark#(s(x)) -> c_16(mark#(x))
        2. Weak:
          

** Step 4.b:1: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
            mark#(ge(x,y)) -> c_13(ge_active#(x,y))
            mark#(minus(x,y)) -> c_15(minus_active#(x,y))
            minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        - Weak DPs:
            div_active#(s(x),s(y)) -> ge_active#(x,y)
            div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            if_active#(false(),x,y) -> mark#(y)
            if_active#(true(),x,y) -> mark#(x)
            mark#(div(x,y)) -> div_active#(mark(x),y)
            mark#(div(x,y)) -> mark#(x)
            mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
            mark#(if(x,y,z)) -> mark#(x)
            mark#(s(x)) -> mark#(x)
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(div_active) = {1},
            uargs(if_active) = {1},
            uargs(s) = {1},
            uargs(div_active#) = {1},
            uargs(if_active#) = {1},
            uargs(c_7) = {1},
            uargs(c_13) = {1},
            uargs(c_15) = {1},
            uargs(c_19) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                        p(0) = [0]                  
                      p(div) = [0]                  
               p(div_active) = [1] x1 + [0]         
                    p(false) = [0]                  
                       p(ge) = [0]                  
                p(ge_active) = [0]                  
                       p(if) = [0]                  
                p(if_active) = [1] x1 + [0]         
                     p(mark) = [0]                  
                    p(minus) = [0]                  
             p(minus_active) = [0]                  
                        p(s) = [1] x1 + [0]         
                     p(true) = [0]                  
              p(div_active#) = [1] x1 + [1]         
               p(ge_active#) = [0]                  
               p(if_active#) = [1] x1 + [1]         
                    p(mark#) = [1]                  
            p(minus_active#) = [4]                  
                      p(c_1) = [2]                  
                      p(c_2) = [0]                  
                      p(c_3) = [2] x1 + [1] x2 + [0]
                      p(c_4) = [2]                  
                      p(c_5) = [2]                  
                      p(c_6) = [0]                  
                      p(c_7) = [1] x1 + [0]         
                      p(c_8) = [1]                  
                      p(c_9) = [1] x1 + [4]         
                     p(c_10) = [1] x1 + [0]         
                     p(c_11) = [1]                  
                     p(c_12) = [2] x2 + [0]         
                     p(c_13) = [1] x1 + [0]         
                     p(c_14) = [4] x1 + [2] x2 + [0]
                     p(c_15) = [1] x1 + [4]         
                     p(c_16) = [1] x1 + [4]         
                     p(c_17) = [0]                  
                     p(c_18) = [1]                  
                     p(c_19) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
          mark#(ge(x,y)) = [1]                  
                         > [0]                  
                         = c_13(ge_active#(x,y))
          
          
          Following rules are (at-least) weakly oriented:
            div_active#(s(x),s(y)) =  [1] x + [1]                                           
                                   >= [0]                                                   
                                   =  ge_active#(x,y)                                       
          
            div_active#(s(x),s(y)) =  [1] x + [1]                                           
                                   >= [1]                                                   
                                   =  if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          
             ge_active#(s(x),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  c_7(ge_active#(x,y))                                  
          
           if_active#(false(),x,y) =  [1]                                                   
                                   >= [1]                                                   
                                   =  mark#(y)                                              
          
            if_active#(true(),x,y) =  [1]                                                   
                                   >= [1]                                                   
                                   =  mark#(x)                                              
          
                   mark#(div(x,y)) =  [1]                                                   
                                   >= [1]                                                   
                                   =  div_active#(mark(x),y)                                
          
                   mark#(div(x,y)) =  [1]                                                   
                                   >= [1]                                                   
                                   =  mark#(x)                                              
          
                  mark#(if(x,y,z)) =  [1]                                                   
                                   >= [1]                                                   
                                   =  if_active#(mark(x),y,z)                               
          
                  mark#(if(x,y,z)) =  [1]                                                   
                                   >= [1]                                                   
                                   =  mark#(x)                                              
          
                 mark#(minus(x,y)) =  [1]                                                   
                                   >= [8]                                                   
                                   =  c_15(minus_active#(x,y))                              
          
                       mark#(s(x)) =  [1]                                                   
                                   >= [1]                                                   
                                   =  mark#(x)                                              
          
          minus_active#(s(x),s(y)) =  [4]                                                   
                                   >= [4]                                                   
                                   =  c_19(minus_active#(x,y))                              
          
                   div_active(x,y) =  [1] x + [0]                                           
                                   >= [0]                                                   
                                   =  div(x,y)                                              
          
              div_active(0(),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
             div_active(s(x),s(y)) =  [1] x + [0]                                           
                                   >= [0]                                                   
                                   =  if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) 
          
                    ge_active(x,y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  ge(x,y)                                               
          
                  ge_active(x,0()) =  [0]                                                   
                                   >= [0]                                                   
                                   =  true()                                                
          
               ge_active(0(),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  false()                                               
          
              ge_active(s(x),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  ge_active(x,y)                                        
          
                  if_active(x,y,z) =  [1] x + [0]                                           
                                   >= [0]                                                   
                                   =  if(x,y,z)                                             
          
            if_active(false(),x,y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  mark(y)                                               
          
             if_active(true(),x,y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  mark(x)                                               
          
                         mark(0()) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
                    mark(div(x,y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  div_active(mark(x),y)                                 
          
                     mark(ge(x,y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  ge_active(x,y)                                        
          
                   mark(if(x,y,z)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  if_active(mark(x),y,z)                                
          
                  mark(minus(x,y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus_active(x,y)                                     
          
                        mark(s(x)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  s(mark(x))                                            
          
                 minus_active(x,y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus(x,y)                                            
          
               minus_active(0(),y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
           minus_active(s(x),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus_active(x,y)                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 4.b:2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
            mark#(minus(x,y)) -> c_15(minus_active#(x,y))
            minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        - Weak DPs:
            div_active#(s(x),s(y)) -> ge_active#(x,y)
            div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            if_active#(false(),x,y) -> mark#(y)
            if_active#(true(),x,y) -> mark#(x)
            mark#(div(x,y)) -> div_active#(mark(x),y)
            mark#(div(x,y)) -> mark#(x)
            mark#(ge(x,y)) -> c_13(ge_active#(x,y))
            mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
            mark#(if(x,y,z)) -> mark#(x)
            mark#(s(x)) -> mark#(x)
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(div_active) = {1},
            uargs(if_active) = {1},
            uargs(s) = {1},
            uargs(div_active#) = {1},
            uargs(if_active#) = {1},
            uargs(c_7) = {1},
            uargs(c_13) = {1},
            uargs(c_15) = {1},
            uargs(c_19) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                        p(0) = [0]                           
                      p(div) = [1] x1 + [0]                  
               p(div_active) = [1] x1 + [0]                  
                    p(false) = [0]                           
                       p(ge) = [1] x1 + [0]                  
                p(ge_active) = [1] x1 + [0]                  
                       p(if) = [1] x1 + [1] x2 + [1] x3 + [0]
                p(if_active) = [1] x1 + [1] x2 + [1] x3 + [0]
                     p(mark) = [1] x1 + [0]                  
                    p(minus) = [0]                           
             p(minus_active) = [0]                           
                        p(s) = [1] x1 + [0]                  
                     p(true) = [0]                           
              p(div_active#) = [1] x1 + [2]                  
               p(ge_active#) = [1] x1 + [2]                  
               p(if_active#) = [1] x1 + [1] x2 + [1] x3 + [2]
                    p(mark#) = [1] x1 + [2]                  
            p(minus_active#) = [0]                           
                      p(c_1) = [1]                           
                      p(c_2) = [1]                           
                      p(c_3) = [2] x1 + [2] x2 + [0]         
                      p(c_4) = [1]                           
                      p(c_5) = [1]                           
                      p(c_6) = [1]                           
                      p(c_7) = [1] x1 + [6]                  
                      p(c_8) = [0]                           
                      p(c_9) = [4] x1 + [0]                  
                     p(c_10) = [4] x1 + [0]                  
                     p(c_11) = [0]                           
                     p(c_12) = [1] x1 + [1] x2 + [2]         
                     p(c_13) = [1] x1 + [0]                  
                     p(c_14) = [1] x1 + [2] x2 + [1]         
                     p(c_15) = [1] x1 + [0]                  
                     p(c_16) = [1] x1 + [0]                  
                     p(c_17) = [0]                           
                     p(c_18) = [0]                           
                     p(c_19) = [1] x1 + [2]                  
          
          Following rules are strictly oriented:
          mark#(minus(x,y)) = [2]                     
                            > [0]                     
                            = c_15(minus_active#(x,y))
          
          
          Following rules are (at-least) weakly oriented:
            div_active#(s(x),s(y)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  ge_active#(x,y)                                       
          
            div_active#(s(x),s(y)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          
             ge_active#(s(x),s(y)) =  [1] x + [2]                                           
                                   >= [1] x + [8]                                           
                                   =  c_7(ge_active#(x,y))                                  
          
           if_active#(false(),x,y) =  [1] x + [1] y + [2]                                   
                                   >= [1] y + [2]                                           
                                   =  mark#(y)                                              
          
            if_active#(true(),x,y) =  [1] x + [1] y + [2]                                   
                                   >= [1] x + [2]                                           
                                   =  mark#(x)                                              
          
                   mark#(div(x,y)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  div_active#(mark(x),y)                                
          
                   mark#(div(x,y)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  mark#(x)                                              
          
                    mark#(ge(x,y)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  c_13(ge_active#(x,y))                                 
          
                  mark#(if(x,y,z)) =  [1] x + [1] y + [1] z + [2]                           
                                   >= [1] x + [1] y + [1] z + [2]                           
                                   =  if_active#(mark(x),y,z)                               
          
                  mark#(if(x,y,z)) =  [1] x + [1] y + [1] z + [2]                           
                                   >= [1] x + [2]                                           
                                   =  mark#(x)                                              
          
                       mark#(s(x)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  mark#(x)                                              
          
          minus_active#(s(x),s(y)) =  [0]                                                   
                                   >= [2]                                                   
                                   =  c_19(minus_active#(x,y))                              
          
                   div_active(x,y) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  div(x,y)                                              
          
              div_active(0(),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
             div_active(s(x),s(y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) 
          
                    ge_active(x,y) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  ge(x,y)                                               
          
                  ge_active(x,0()) =  [1] x + [0]                                           
                                   >= [0]                                                   
                                   =  true()                                                
          
               ge_active(0(),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  false()                                               
          
              ge_active(s(x),s(y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  ge_active(x,y)                                        
          
                  if_active(x,y,z) =  [1] x + [1] y + [1] z + [0]                           
                                   >= [1] x + [1] y + [1] z + [0]                           
                                   =  if(x,y,z)                                             
          
            if_active(false(),x,y) =  [1] x + [1] y + [0]                                   
                                   >= [1] y + [0]                                           
                                   =  mark(y)                                               
          
             if_active(true(),x,y) =  [1] x + [1] y + [0]                                   
                                   >= [1] x + [0]                                           
                                   =  mark(x)                                               
          
                         mark(0()) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
                    mark(div(x,y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  div_active(mark(x),y)                                 
          
                     mark(ge(x,y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  ge_active(x,y)                                        
          
                   mark(if(x,y,z)) =  [1] x + [1] y + [1] z + [0]                           
                                   >= [1] x + [1] y + [1] z + [0]                           
                                   =  if_active(mark(x),y,z)                                
          
                  mark(minus(x,y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus_active(x,y)                                     
          
                        mark(s(x)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  s(mark(x))                                            
          
                 minus_active(x,y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus(x,y)                                            
          
               minus_active(0(),y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
           minus_active(s(x),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus_active(x,y)                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 4.b:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
            minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        - Weak DPs:
            div_active#(s(x),s(y)) -> ge_active#(x,y)
            div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            if_active#(false(),x,y) -> mark#(y)
            if_active#(true(),x,y) -> mark#(x)
            mark#(div(x,y)) -> div_active#(mark(x),y)
            mark#(div(x,y)) -> mark#(x)
            mark#(ge(x,y)) -> c_13(ge_active#(x,y))
            mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
            mark#(if(x,y,z)) -> mark#(x)
            mark#(minus(x,y)) -> c_15(minus_active#(x,y))
            mark#(s(x)) -> mark#(x)
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(div_active) = {1},
            uargs(if_active) = {1},
            uargs(s) = {1},
            uargs(div_active#) = {1},
            uargs(if_active#) = {1},
            uargs(c_7) = {1},
            uargs(c_13) = {1},
            uargs(c_15) = {1},
            uargs(c_19) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                        p(0) = [0]                           
                      p(div) = [1] x1 + [0]                  
               p(div_active) = [1] x1 + [0]                  
                    p(false) = [0]                           
                       p(ge) = [0]                           
                p(ge_active) = [0]                           
                       p(if) = [1] x1 + [1] x2 + [1] x3 + [0]
                p(if_active) = [1] x1 + [1] x2 + [1] x3 + [0]
                     p(mark) = [1] x1 + [0]                  
                    p(minus) = [1] x1 + [0]                  
             p(minus_active) = [1] x1 + [0]                  
                        p(s) = [1] x1 + [1]                  
                     p(true) = [0]                           
              p(div_active#) = [1] x1 + [0]                  
               p(ge_active#) = [0]                           
               p(if_active#) = [1] x1 + [1] x2 + [1] x3 + [0]
                    p(mark#) = [1] x1 + [0]                  
            p(minus_active#) = [1] x1 + [0]                  
                      p(c_1) = [0]                           
                      p(c_2) = [0]                           
                      p(c_3) = [2]                           
                      p(c_4) = [1]                           
                      p(c_5) = [0]                           
                      p(c_6) = [1]                           
                      p(c_7) = [1] x1 + [2]                  
                      p(c_8) = [1]                           
                      p(c_9) = [2] x1 + [1]                  
                     p(c_10) = [1]                           
                     p(c_11) = [1]                           
                     p(c_12) = [2] x1 + [1] x2 + [1]         
                     p(c_13) = [1] x1 + [0]                  
                     p(c_14) = [1] x2 + [1]                  
                     p(c_15) = [1] x1 + [0]                  
                     p(c_16) = [2]                           
                     p(c_17) = [0]                           
                     p(c_18) = [0]                           
                     p(c_19) = [1] x1 + [0]                  
          
          Following rules are strictly oriented:
          minus_active#(s(x),s(y)) = [1] x + [1]             
                                   > [1] x + [0]             
                                   = c_19(minus_active#(x,y))
          
          
          Following rules are (at-least) weakly oriented:
           div_active#(s(x),s(y)) =  [1] x + [1]                                           
                                  >= [0]                                                   
                                  =  ge_active#(x,y)                                       
          
           div_active#(s(x),s(y)) =  [1] x + [1]                                           
                                  >= [1] x + [1]                                           
                                  =  if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          
            ge_active#(s(x),s(y)) =  [0]                                                   
                                  >= [2]                                                   
                                  =  c_7(ge_active#(x,y))                                  
          
          if_active#(false(),x,y) =  [1] x + [1] y + [0]                                   
                                  >= [1] y + [0]                                           
                                  =  mark#(y)                                              
          
           if_active#(true(),x,y) =  [1] x + [1] y + [0]                                   
                                  >= [1] x + [0]                                           
                                  =  mark#(x)                                              
          
                  mark#(div(x,y)) =  [1] x + [0]                                           
                                  >= [1] x + [0]                                           
                                  =  div_active#(mark(x),y)                                
          
                  mark#(div(x,y)) =  [1] x + [0]                                           
                                  >= [1] x + [0]                                           
                                  =  mark#(x)                                              
          
                   mark#(ge(x,y)) =  [0]                                                   
                                  >= [0]                                                   
                                  =  c_13(ge_active#(x,y))                                 
          
                 mark#(if(x,y,z)) =  [1] x + [1] y + [1] z + [0]                           
                                  >= [1] x + [1] y + [1] z + [0]                           
                                  =  if_active#(mark(x),y,z)                               
          
                 mark#(if(x,y,z)) =  [1] x + [1] y + [1] z + [0]                           
                                  >= [1] x + [0]                                           
                                  =  mark#(x)                                              
          
                mark#(minus(x,y)) =  [1] x + [0]                                           
                                  >= [1] x + [0]                                           
                                  =  c_15(minus_active#(x,y))                              
          
                      mark#(s(x)) =  [1] x + [1]                                           
                                  >= [1] x + [0]                                           
                                  =  mark#(x)                                              
          
                  div_active(x,y) =  [1] x + [0]                                           
                                  >= [1] x + [0]                                           
                                  =  div(x,y)                                              
          
             div_active(0(),s(y)) =  [0]                                                   
                                  >= [0]                                                   
                                  =  0()                                                   
          
            div_active(s(x),s(y)) =  [1] x + [1]                                           
                                  >= [1] x + [1]                                           
                                  =  if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) 
          
                   ge_active(x,y) =  [0]                                                   
                                  >= [0]                                                   
                                  =  ge(x,y)                                               
          
                 ge_active(x,0()) =  [0]                                                   
                                  >= [0]                                                   
                                  =  true()                                                
          
              ge_active(0(),s(y)) =  [0]                                                   
                                  >= [0]                                                   
                                  =  false()                                               
          
             ge_active(s(x),s(y)) =  [0]                                                   
                                  >= [0]                                                   
                                  =  ge_active(x,y)                                        
          
                 if_active(x,y,z) =  [1] x + [1] y + [1] z + [0]                           
                                  >= [1] x + [1] y + [1] z + [0]                           
                                  =  if(x,y,z)                                             
          
           if_active(false(),x,y) =  [1] x + [1] y + [0]                                   
                                  >= [1] y + [0]                                           
                                  =  mark(y)                                               
          
            if_active(true(),x,y) =  [1] x + [1] y + [0]                                   
                                  >= [1] x + [0]                                           
                                  =  mark(x)                                               
          
                        mark(0()) =  [0]                                                   
                                  >= [0]                                                   
                                  =  0()                                                   
          
                   mark(div(x,y)) =  [1] x + [0]                                           
                                  >= [1] x + [0]                                           
                                  =  div_active(mark(x),y)                                 
          
                    mark(ge(x,y)) =  [0]                                                   
                                  >= [0]                                                   
                                  =  ge_active(x,y)                                        
          
                  mark(if(x,y,z)) =  [1] x + [1] y + [1] z + [0]                           
                                  >= [1] x + [1] y + [1] z + [0]                           
                                  =  if_active(mark(x),y,z)                                
          
                 mark(minus(x,y)) =  [1] x + [0]                                           
                                  >= [1] x + [0]                                           
                                  =  minus_active(x,y)                                     
          
                       mark(s(x)) =  [1] x + [1]                                           
                                  >= [1] x + [1]                                           
                                  =  s(mark(x))                                            
          
                minus_active(x,y) =  [1] x + [0]                                           
                                  >= [1] x + [0]                                           
                                  =  minus(x,y)                                            
          
              minus_active(0(),y) =  [0]                                                   
                                  >= [0]                                                   
                                  =  0()                                                   
          
          minus_active(s(x),s(y)) =  [1] x + [1]                                           
                                  >= [1] x + [0]                                           
                                  =  minus_active(x,y)                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 4.b:4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
        - Weak DPs:
            div_active#(s(x),s(y)) -> ge_active#(x,y)
            div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            if_active#(false(),x,y) -> mark#(y)
            if_active#(true(),x,y) -> mark#(x)
            mark#(div(x,y)) -> div_active#(mark(x),y)
            mark#(div(x,y)) -> mark#(x)
            mark#(ge(x,y)) -> c_13(ge_active#(x,y))
            mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
            mark#(if(x,y,z)) -> mark#(x)
            mark#(minus(x,y)) -> c_15(minus_active#(x,y))
            mark#(s(x)) -> mark#(x)
            minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(div_active) = {1},
            uargs(if_active) = {1},
            uargs(s) = {1},
            uargs(div_active#) = {1},
            uargs(if_active#) = {1},
            uargs(c_7) = {1},
            uargs(c_13) = {1},
            uargs(c_15) = {1},
            uargs(c_19) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                        p(0) = [0]                           
                      p(div) = [1] x1 + [0]                  
               p(div_active) = [1] x1 + [0]                  
                    p(false) = [0]                           
                       p(ge) = [1] x1 + [0]                  
                p(ge_active) = [1] x1 + [0]                  
                       p(if) = [1] x1 + [1] x2 + [1] x3 + [0]
                p(if_active) = [1] x1 + [1] x2 + [1] x3 + [0]
                     p(mark) = [1] x1 + [0]                  
                    p(minus) = [0]                           
             p(minus_active) = [0]                           
                        p(s) = [1] x1 + [2]                  
                     p(true) = [0]                           
              p(div_active#) = [1] x1 + [0]                  
               p(ge_active#) = [1] x1 + [0]                  
               p(if_active#) = [1] x1 + [1] x2 + [1] x3 + [0]
                    p(mark#) = [1] x1 + [0]                  
            p(minus_active#) = [0]                           
                      p(c_1) = [1]                           
                      p(c_2) = [0]                           
                      p(c_3) = [1] x1 + [2] x2 + [0]         
                      p(c_4) = [0]                           
                      p(c_5) = [0]                           
                      p(c_6) = [2]                           
                      p(c_7) = [1] x1 + [1]                  
                      p(c_8) = [0]                           
                      p(c_9) = [1]                           
                     p(c_10) = [0]                           
                     p(c_11) = [1]                           
                     p(c_12) = [1] x2 + [4]                  
                     p(c_13) = [1] x1 + [0]                  
                     p(c_14) = [1] x1 + [0]                  
                     p(c_15) = [1] x1 + [0]                  
                     p(c_16) = [1]                           
                     p(c_17) = [0]                           
                     p(c_18) = [2]                           
                     p(c_19) = [1] x1 + [0]                  
          
          Following rules are strictly oriented:
          ge_active#(s(x),s(y)) = [1] x + [2]         
                                > [1] x + [1]         
                                = c_7(ge_active#(x,y))
          
          
          Following rules are (at-least) weakly oriented:
            div_active#(s(x),s(y)) =  [1] x + [2]                                           
                                   >= [1] x + [0]                                           
                                   =  ge_active#(x,y)                                       
          
            div_active#(s(x),s(y)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          
           if_active#(false(),x,y) =  [1] x + [1] y + [0]                                   
                                   >= [1] y + [0]                                           
                                   =  mark#(y)                                              
          
            if_active#(true(),x,y) =  [1] x + [1] y + [0]                                   
                                   >= [1] x + [0]                                           
                                   =  mark#(x)                                              
          
                   mark#(div(x,y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  div_active#(mark(x),y)                                
          
                   mark#(div(x,y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  mark#(x)                                              
          
                    mark#(ge(x,y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  c_13(ge_active#(x,y))                                 
          
                  mark#(if(x,y,z)) =  [1] x + [1] y + [1] z + [0]                           
                                   >= [1] x + [1] y + [1] z + [0]                           
                                   =  if_active#(mark(x),y,z)                               
          
                  mark#(if(x,y,z)) =  [1] x + [1] y + [1] z + [0]                           
                                   >= [1] x + [0]                                           
                                   =  mark#(x)                                              
          
                 mark#(minus(x,y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  c_15(minus_active#(x,y))                              
          
                       mark#(s(x)) =  [1] x + [2]                                           
                                   >= [1] x + [0]                                           
                                   =  mark#(x)                                              
          
          minus_active#(s(x),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  c_19(minus_active#(x,y))                              
          
                   div_active(x,y) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  div(x,y)                                              
          
              div_active(0(),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
             div_active(s(x),s(y)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) 
          
                    ge_active(x,y) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  ge(x,y)                                               
          
                  ge_active(x,0()) =  [1] x + [0]                                           
                                   >= [0]                                                   
                                   =  true()                                                
          
               ge_active(0(),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  false()                                               
          
              ge_active(s(x),s(y)) =  [1] x + [2]                                           
                                   >= [1] x + [0]                                           
                                   =  ge_active(x,y)                                        
          
                  if_active(x,y,z) =  [1] x + [1] y + [1] z + [0]                           
                                   >= [1] x + [1] y + [1] z + [0]                           
                                   =  if(x,y,z)                                             
          
            if_active(false(),x,y) =  [1] x + [1] y + [0]                                   
                                   >= [1] y + [0]                                           
                                   =  mark(y)                                               
          
             if_active(true(),x,y) =  [1] x + [1] y + [0]                                   
                                   >= [1] x + [0]                                           
                                   =  mark(x)                                               
          
                         mark(0()) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
                    mark(div(x,y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  div_active(mark(x),y)                                 
          
                     mark(ge(x,y)) =  [1] x + [0]                                           
                                   >= [1] x + [0]                                           
                                   =  ge_active(x,y)                                        
          
                   mark(if(x,y,z)) =  [1] x + [1] y + [1] z + [0]                           
                                   >= [1] x + [1] y + [1] z + [0]                           
                                   =  if_active(mark(x),y,z)                                
          
                  mark(minus(x,y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus_active(x,y)                                     
          
                        mark(s(x)) =  [1] x + [2]                                           
                                   >= [1] x + [2]                                           
                                   =  s(mark(x))                                            
          
                 minus_active(x,y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus(x,y)                                            
          
               minus_active(0(),y) =  [0]                                                   
                                   >= [0]                                                   
                                   =  0()                                                   
          
           minus_active(s(x),s(y)) =  [0]                                                   
                                   >= [0]                                                   
                                   =  minus_active(x,y)                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 4.b:5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            div_active#(s(x),s(y)) -> ge_active#(x,y)
            div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active#(s(x),s(y)) -> c_7(ge_active#(x,y))
            if_active#(false(),x,y) -> mark#(y)
            if_active#(true(),x,y) -> mark#(x)
            mark#(div(x,y)) -> div_active#(mark(x),y)
            mark#(div(x,y)) -> mark#(x)
            mark#(ge(x,y)) -> c_13(ge_active#(x,y))
            mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
            mark#(if(x,y,z)) -> mark#(x)
            mark#(minus(x,y)) -> c_15(minus_active#(x,y))
            mark#(s(x)) -> mark#(x)
            minus_active#(s(x),s(y)) -> c_19(minus_active#(x,y))
        - Weak TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2,div_active#/2,ge_active#/2,if_active#/3,mark#/1
            ,minus_active#/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1,true/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0
            ,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/1,c_14/2,c_15/1,c_16/1,c_17/0,c_18/0,c_19/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active#,ge_active#,if_active#,mark#
            ,minus_active#} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^3))