WORST_CASE(Omega(n^1),O(n^2))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^2))
    + Considered Problem:
        - Strict TRS:
            gcd(0(),Y) -> 0()
            gcd(s(X),0()) -> s(X)
            gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
            if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
            if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd,if,le,minus,pred} and constructors {0,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            gcd(0(),Y) -> 0()
            gcd(s(X),0()) -> s(X)
            gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
            if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
            if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd,if,le,minus,pred} and constructors {0,false,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          le(x,y){x -> s(x),y -> s(y)} =
            le(s(x),s(y)) ->^+ le(x,y)
              = C[le(x,y) = le(x,y){}]

** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            gcd(0(),Y) -> 0()
            gcd(s(X),0()) -> s(X)
            gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
            if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
            if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd,if,le,minus,pred} and constructors {0,false,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          gcd#(0(),Y) -> c_1()
          gcd#(s(X),0()) -> c_2()
          gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
          if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
          if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
          le#(0(),Y) -> c_6()
          le#(s(X),0()) -> c_7()
          le#(s(X),s(Y)) -> c_8(le#(X,Y))
          minus#(X,0()) -> c_9()
          minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y))
          pred#(s(X)) -> c_11()
        Weak DPs
          
        
        and mark the set of starting terms.
** Step 1.b:2: PredecessorEstimation WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            gcd#(0(),Y) -> c_1()
            gcd#(s(X),0()) -> c_2()
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
            le#(0(),Y) -> c_6()
            le#(s(X),0()) -> c_7()
            le#(s(X),s(Y)) -> c_8(le#(X,Y))
            minus#(X,0()) -> c_9()
            minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y))
            pred#(s(X)) -> c_11()
        - Weak TRS:
            gcd(0(),Y) -> 0()
            gcd(s(X),0()) -> s(X)
            gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
            if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
            if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,s
            ,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,6,7,9,11}
        by application of
          Pre({1,2,6,7,9,11}) = {3,4,5,8,10}.
        Here rules are labelled as follows:
          1: gcd#(0(),Y) -> c_1()
          2: gcd#(s(X),0()) -> c_2()
          3: gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
          4: if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
          5: if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
          6: le#(0(),Y) -> c_6()
          7: le#(s(X),0()) -> c_7()
          8: le#(s(X),s(Y)) -> c_8(le#(X,Y))
          9: minus#(X,0()) -> c_9()
          10: minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y))
          11: pred#(s(X)) -> c_11()
** Step 1.b:3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
            le#(s(X),s(Y)) -> c_8(le#(X,Y))
            minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y))
        - Weak DPs:
            gcd#(0(),Y) -> c_1()
            gcd#(s(X),0()) -> c_2()
            le#(0(),Y) -> c_6()
            le#(s(X),0()) -> c_7()
            minus#(X,0()) -> c_9()
            pred#(s(X)) -> c_11()
        - Weak TRS:
            gcd(0(),Y) -> 0()
            gcd(s(X),0()) -> s(X)
            gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
            if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
            if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,s
            ,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
             -->_2 le#(s(X),s(Y)) -> c_8(le#(X,Y)):4
             -->_1 if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y)):3
             -->_1 if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X)):2
             -->_2 le#(s(X),0()) -> c_7():9
             -->_2 le#(0(),Y) -> c_6():8
          
          2:S:if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
             -->_2 minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y)):5
             -->_2 minus#(X,0()) -> c_9():10
             -->_1 gcd#(0(),Y) -> c_1():6
             -->_1 gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X)):1
          
          3:S:if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
             -->_2 minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y)):5
             -->_2 minus#(X,0()) -> c_9():10
             -->_1 gcd#(0(),Y) -> c_1():6
             -->_1 gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X)):1
          
          4:S:le#(s(X),s(Y)) -> c_8(le#(X,Y))
             -->_1 le#(s(X),0()) -> c_7():9
             -->_1 le#(0(),Y) -> c_6():8
             -->_1 le#(s(X),s(Y)) -> c_8(le#(X,Y)):4
          
          5:S:minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y))
             -->_1 pred#(s(X)) -> c_11():11
             -->_2 minus#(X,0()) -> c_9():10
             -->_2 minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y)):5
          
          6:W:gcd#(0(),Y) -> c_1()
             
          
          7:W:gcd#(s(X),0()) -> c_2()
             
          
          8:W:le#(0(),Y) -> c_6()
             
          
          9:W:le#(s(X),0()) -> c_7()
             
          
          10:W:minus#(X,0()) -> c_9()
             
          
          11:W:pred#(s(X)) -> c_11()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: gcd#(s(X),0()) -> c_2()
          6: gcd#(0(),Y) -> c_1()
          10: minus#(X,0()) -> c_9()
          11: pred#(s(X)) -> c_11()
          8: le#(0(),Y) -> c_6()
          9: le#(s(X),0()) -> c_7()
** Step 1.b:4: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
            le#(s(X),s(Y)) -> c_8(le#(X,Y))
            minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y))
        - Weak TRS:
            gcd(0(),Y) -> 0()
            gcd(s(X),0()) -> s(X)
            gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
            if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
            if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,s
            ,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
             -->_2 le#(s(X),s(Y)) -> c_8(le#(X,Y)):4
             -->_1 if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y)):3
             -->_1 if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X)):2
          
          2:S:if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
             -->_2 minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y)):5
             -->_1 gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X)):1
          
          3:S:if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
             -->_2 minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y)):5
             -->_1 gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X)):1
          
          4:S:le#(s(X),s(Y)) -> c_8(le#(X,Y))
             -->_1 le#(s(X),s(Y)) -> c_8(le#(X,Y)):4
          
          5:S:minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y))
             -->_2 minus#(X,s(Y)) -> c_10(pred#(minus(X,Y)),minus#(X,Y)):5
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          minus#(X,s(Y)) -> c_10(minus#(X,Y))
** Step 1.b:5: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
            le#(s(X),s(Y)) -> c_8(le#(X,Y))
            minus#(X,s(Y)) -> c_10(minus#(X,Y))
        - Weak TRS:
            gcd(0(),Y) -> 0()
            gcd(s(X),0()) -> s(X)
            gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
            if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
            if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,s
            ,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          le(0(),Y) -> true()
          le(s(X),0()) -> false()
          le(s(X),s(Y)) -> le(X,Y)
          minus(X,0()) -> X
          minus(X,s(Y)) -> pred(minus(X,Y))
          pred(s(X)) -> X
          gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
          if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
          if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
          le#(s(X),s(Y)) -> c_8(le#(X,Y))
          minus#(X,s(Y)) -> c_10(minus#(X,Y))
** Step 1.b:6: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
            le#(s(X),s(Y)) -> c_8(le#(X,Y))
            minus#(X,s(Y)) -> c_10(minus#(X,Y))
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,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
          gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
          if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
          if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
        and a lower component
          le#(s(X),s(Y)) -> c_8(le#(X,Y))
          minus#(X,s(Y)) -> c_10(minus#(X,Y))
        Further, following extension rules are added to the lower component.
          gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
          gcd#(s(X),s(Y)) -> le#(Y,X)
          if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
          if#(false(),s(X),s(Y)) -> minus#(Y,X)
          if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
          if#(true(),s(X),s(Y)) -> minus#(X,Y)
*** Step 1.b:6.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,s
            ,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X))
             -->_1 if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y)):3
             -->_1 if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X)):2
          
          2:S:if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)),minus#(Y,X))
             -->_1 gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X)):1
          
          3:S:if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)),minus#(X,Y))
             -->_1 gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)),le#(Y,X)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)))
          if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)))
          if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)))
*** Step 1.b:6.a:2: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)))
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,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_4) = {1},
          uargs(c_5) = {1}
        
        Following symbols are considered usable:
          {minus,pred,gcd#,if#,le#,minus#,pred#}
        TcT has computed the following interpretation:
               p(0) = [0]                    
           p(false) = [0]                    
             p(gcd) = [2]                    
              p(if) = [1] x1 + [1] x2 + [8]  
              p(le) = [0]                    
           p(minus) = [1] x1 + [0]           
            p(pred) = [1] x1 + [0]           
               p(s) = [1] x1 + [1]           
            p(true) = [0]                    
            p(gcd#) = [14] x1 + [14] x2 + [2]
             p(if#) = [14] x2 + [14] x3 + [0]
             p(le#) = [1]                    
          p(minus#) = [2] x2 + [4]           
           p(pred#) = [1]                    
             p(c_1) = [1]                    
             p(c_2) = [0]                    
             p(c_3) = [1] x1 + [2]           
             p(c_4) = [1] x1 + [12]          
             p(c_5) = [1] x1 + [8]           
             p(c_6) = [0]                    
             p(c_7) = [0]                    
             p(c_8) = [1] x1 + [1]           
             p(c_9) = [1]                    
            p(c_10) = [2] x1 + [0]           
            p(c_11) = [0]                    
        
        Following rules are strictly oriented:
        if#(true(),s(X),s(Y)) = [14] X + [14] Y + [28]    
                              > [14] X + [14] Y + [24]    
                              = c_5(gcd#(minus(X,Y),s(Y)))
        
        
        Following rules are (at-least) weakly oriented:
               gcd#(s(X),s(Y)) =  [14] X + [14] Y + [30]     
                               >= [14] X + [14] Y + [30]     
                               =  c_3(if#(le(Y,X),s(X),s(Y)))
        
        if#(false(),s(X),s(Y)) =  [14] X + [14] Y + [28]     
                               >= [14] X + [14] Y + [28]     
                               =  c_4(gcd#(minus(Y,X),s(X))) 
        
                  minus(X,0()) =  [1] X + [0]                
                               >= [1] X + [0]                
                               =  X                          
        
                 minus(X,s(Y)) =  [1] X + [0]                
                               >= [1] X + [0]                
                               =  pred(minus(X,Y))           
        
                    pred(s(X)) =  [1] X + [1]                
                               >= [1] X + [0]                
                               =  X                          
        
*** Step 1.b:6.a:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)))
        - Weak DPs:
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)))
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,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(pred) = {1},
            uargs(gcd#) = {1},
            uargs(if#) = {1},
            uargs(c_3) = {1},
            uargs(c_4) = {1},
            uargs(c_5) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(0) = [0]                           
             p(false) = [0]                           
               p(gcd) = [0]                           
                p(if) = [0]                           
                p(le) = [0]                           
             p(minus) = [1] x1 + [3]                  
              p(pred) = [1] x1 + [0]                  
                 p(s) = [1] x1 + [6]                  
              p(true) = [0]                           
              p(gcd#) = [1] x1 + [1] x2 + [3]         
               p(if#) = [1] x1 + [1] x2 + [1] x3 + [0]
               p(le#) = [0]                           
            p(minus#) = [0]                           
             p(pred#) = [0]                           
               p(c_1) = [0]                           
               p(c_2) = [0]                           
               p(c_3) = [1] x1 + [0]                  
               p(c_4) = [1] x1 + [0]                  
               p(c_5) = [1] x1 + [0]                  
               p(c_6) = [0]                           
               p(c_7) = [0]                           
               p(c_8) = [0]                           
               p(c_9) = [0]                           
              p(c_10) = [0]                           
              p(c_11) = [0]                           
          
          Following rules are strictly oriented:
          gcd#(s(X),s(Y)) = [1] X + [1] Y + [15]       
                          > [1] X + [1] Y + [12]       
                          = c_3(if#(le(Y,X),s(X),s(Y)))
          
          
          Following rules are (at-least) weakly oriented:
          if#(false(),s(X),s(Y)) =  [1] X + [1] Y + [12]      
                                 >= [1] X + [1] Y + [12]      
                                 =  c_4(gcd#(minus(Y,X),s(X)))
          
           if#(true(),s(X),s(Y)) =  [1] X + [1] Y + [12]      
                                 >= [1] X + [1] Y + [12]      
                                 =  c_5(gcd#(minus(X,Y),s(Y)))
          
                       le(0(),Y) =  [0]                       
                                 >= [0]                       
                                 =  true()                    
          
                    le(s(X),0()) =  [0]                       
                                 >= [0]                       
                                 =  false()                   
          
                   le(s(X),s(Y)) =  [0]                       
                                 >= [0]                       
                                 =  le(X,Y)                   
          
                    minus(X,0()) =  [1] X + [3]               
                                 >= [1] X + [0]               
                                 =  X                         
          
                   minus(X,s(Y)) =  [1] X + [3]               
                                 >= [1] X + [3]               
                                 =  pred(minus(X,Y))          
          
                      pred(s(X)) =  [1] X + [6]               
                                 >= [1] X + [0]               
                                 =  X                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:6.a:4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)))
        - Weak DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)))
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,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(pred) = {1},
            uargs(gcd#) = {1},
            uargs(if#) = {1},
            uargs(c_3) = {1},
            uargs(c_4) = {1},
            uargs(c_5) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(0) = [0]                           
             p(false) = [0]                           
               p(gcd) = [1] x1 + [4]                  
                p(if) = [1] x2 + [1] x3 + [0]         
                p(le) = [1]                           
             p(minus) = [1] x1 + [0]                  
              p(pred) = [1] x1 + [0]                  
                 p(s) = [1] x1 + [2]                  
              p(true) = [1]                           
              p(gcd#) = [1] x1 + [1] x2 + [2]         
               p(if#) = [1] x1 + [1] x2 + [1] x3 + [1]
               p(le#) = [0]                           
            p(minus#) = [1] x1 + [1] x2 + [4]         
             p(pred#) = [1] x1 + [1]                  
               p(c_1) = [2]                           
               p(c_2) = [0]                           
               p(c_3) = [1] x1 + [0]                  
               p(c_4) = [1] x1 + [0]                  
               p(c_5) = [1] x1 + [2]                  
               p(c_6) = [0]                           
               p(c_7) = [0]                           
               p(c_8) = [2] x1 + [2]                  
               p(c_9) = [0]                           
              p(c_10) = [1] x1 + [4]                  
              p(c_11) = [0]                           
          
          Following rules are strictly oriented:
          if#(false(),s(X),s(Y)) = [1] X + [1] Y + [5]       
                                 > [1] X + [1] Y + [4]       
                                 = c_4(gcd#(minus(Y,X),s(X)))
          
          
          Following rules are (at-least) weakly oriented:
                gcd#(s(X),s(Y)) =  [1] X + [1] Y + [6]        
                                >= [1] X + [1] Y + [6]        
                                =  c_3(if#(le(Y,X),s(X),s(Y)))
          
          if#(true(),s(X),s(Y)) =  [1] X + [1] Y + [6]        
                                >= [1] X + [1] Y + [6]        
                                =  c_5(gcd#(minus(X,Y),s(Y))) 
          
                      le(0(),Y) =  [1]                        
                                >= [1]                        
                                =  true()                     
          
                   le(s(X),0()) =  [1]                        
                                >= [0]                        
                                =  false()                    
          
                  le(s(X),s(Y)) =  [1]                        
                                >= [1]                        
                                =  le(X,Y)                    
          
                   minus(X,0()) =  [1] X + [0]                
                                >= [1] X + [0]                
                                =  X                          
          
                  minus(X,s(Y)) =  [1] X + [0]                
                                >= [1] X + [0]                
                                =  pred(minus(X,Y))           
          
                     pred(s(X)) =  [1] X + [2]                
                                >= [1] X + [0]                
                                =  X                          
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:6.a:5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            gcd#(s(X),s(Y)) -> c_3(if#(le(Y,X),s(X),s(Y)))
            if#(false(),s(X),s(Y)) -> c_4(gcd#(minus(Y,X),s(X)))
            if#(true(),s(X),s(Y)) -> c_5(gcd#(minus(X,Y),s(Y)))
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,s
            ,true}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

*** Step 1.b:6.b:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            le#(s(X),s(Y)) -> c_8(le#(X,Y))
            minus#(X,s(Y)) -> c_10(minus#(X,Y))
        - Weak DPs:
            gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
            gcd#(s(X),s(Y)) -> le#(Y,X)
            if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
            if#(false(),s(X),s(Y)) -> minus#(Y,X)
            if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
            if#(true(),s(X),s(Y)) -> minus#(X,Y)
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,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_8) = {1},
          uargs(c_10) = {1}
        
        Following symbols are considered usable:
          {minus,pred,gcd#,if#,le#,minus#,pred#}
        TcT has computed the following interpretation:
               p(0) = [0]                           
           p(false) = [2]                           
             p(gcd) = [1] x1 + [2] x2 + [2]         
              p(if) = [1] x1 + [1] x2 + [1] x3 + [1]
              p(le) = [8] x1 + [0]                  
           p(minus) = [1] x1 + [1]                  
            p(pred) = [1] x1 + [0]                  
               p(s) = [1] x1 + [2]                  
            p(true) = [0]                           
            p(gcd#) = [1] x1 + [1] x2 + [1]         
             p(if#) = [1] x2 + [1] x3 + [0]         
             p(le#) = [1] x1 + [0]                  
          p(minus#) = [0]                           
           p(pred#) = [1]                           
             p(c_1) = [0]                           
             p(c_2) = [2]                           
             p(c_3) = [4] x1 + [1] x2 + [0]         
             p(c_4) = [2]                           
             p(c_5) = [2] x1 + [1]                  
             p(c_6) = [0]                           
             p(c_7) = [1]                           
             p(c_8) = [1] x1 + [0]                  
             p(c_9) = [1]                           
            p(c_10) = [4] x1 + [0]                  
            p(c_11) = [1]                           
        
        Following rules are strictly oriented:
        le#(s(X),s(Y)) = [1] X + [2]  
                       > [1] X + [0]  
                       = c_8(le#(X,Y))
        
        
        Following rules are (at-least) weakly oriented:
               gcd#(s(X),s(Y)) =  [1] X + [1] Y + [5]   
                               >= [1] X + [1] Y + [4]   
                               =  if#(le(Y,X),s(X),s(Y))
        
               gcd#(s(X),s(Y)) =  [1] X + [1] Y + [5]   
                               >= [1] Y + [0]           
                               =  le#(Y,X)              
        
        if#(false(),s(X),s(Y)) =  [1] X + [1] Y + [4]   
                               >= [1] X + [1] Y + [4]   
                               =  gcd#(minus(Y,X),s(X)) 
        
        if#(false(),s(X),s(Y)) =  [1] X + [1] Y + [4]   
                               >= [0]                   
                               =  minus#(Y,X)           
        
         if#(true(),s(X),s(Y)) =  [1] X + [1] Y + [4]   
                               >= [1] X + [1] Y + [4]   
                               =  gcd#(minus(X,Y),s(Y)) 
        
         if#(true(),s(X),s(Y)) =  [1] X + [1] Y + [4]   
                               >= [0]                   
                               =  minus#(X,Y)           
        
                minus#(X,s(Y)) =  [0]                   
                               >= [0]                   
                               =  c_10(minus#(X,Y))     
        
                  minus(X,0()) =  [1] X + [1]           
                               >= [1] X + [0]           
                               =  X                     
        
                 minus(X,s(Y)) =  [1] X + [1]           
                               >= [1] X + [1]           
                               =  pred(minus(X,Y))      
        
                    pred(s(X)) =  [1] X + [2]           
                               >= [1] X + [0]           
                               =  X                     
        
*** Step 1.b:6.b:2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            minus#(X,s(Y)) -> c_10(minus#(X,Y))
        - Weak DPs:
            gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
            gcd#(s(X),s(Y)) -> le#(Y,X)
            if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
            if#(false(),s(X),s(Y)) -> minus#(Y,X)
            if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
            if#(true(),s(X),s(Y)) -> minus#(X,Y)
            le#(s(X),s(Y)) -> c_8(le#(X,Y))
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,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(pred) = {1},
            uargs(gcd#) = {1},
            uargs(if#) = {1},
            uargs(c_8) = {1},
            uargs(c_10) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(0) = [0]                           
             p(false) = [0]                           
               p(gcd) = [0]                           
                p(if) = [0]                           
                p(le) = [3]                           
             p(minus) = [1] x1 + [0]                  
              p(pred) = [1] x1 + [0]                  
                 p(s) = [1] x1 + [4]                  
              p(true) = [0]                           
              p(gcd#) = [1] x1 + [1] x2 + [3]         
               p(if#) = [1] x1 + [1] x2 + [1] x3 + [0]
               p(le#) = [0]                           
            p(minus#) = [1] x1 + [1] x2 + [3]         
             p(pred#) = [0]                           
               p(c_1) = [0]                           
               p(c_2) = [0]                           
               p(c_3) = [0]                           
               p(c_4) = [0]                           
               p(c_5) = [0]                           
               p(c_6) = [0]                           
               p(c_7) = [0]                           
               p(c_8) = [1] x1 + [0]                  
               p(c_9) = [0]                           
              p(c_10) = [1] x1 + [1]                  
              p(c_11) = [0]                           
          
          Following rules are strictly oriented:
          minus#(X,s(Y)) = [1] X + [1] Y + [7]
                         > [1] X + [1] Y + [4]
                         = c_10(minus#(X,Y))  
          
          
          Following rules are (at-least) weakly oriented:
                 gcd#(s(X),s(Y)) =  [1] X + [1] Y + [11]  
                                 >= [1] X + [1] Y + [11]  
                                 =  if#(le(Y,X),s(X),s(Y))
          
                 gcd#(s(X),s(Y)) =  [1] X + [1] Y + [11]  
                                 >= [0]                   
                                 =  le#(Y,X)              
          
          if#(false(),s(X),s(Y)) =  [1] X + [1] Y + [8]   
                                 >= [1] X + [1] Y + [7]   
                                 =  gcd#(minus(Y,X),s(X)) 
          
          if#(false(),s(X),s(Y)) =  [1] X + [1] Y + [8]   
                                 >= [1] X + [1] Y + [3]   
                                 =  minus#(Y,X)           
          
           if#(true(),s(X),s(Y)) =  [1] X + [1] Y + [8]   
                                 >= [1] X + [1] Y + [7]   
                                 =  gcd#(minus(X,Y),s(Y)) 
          
           if#(true(),s(X),s(Y)) =  [1] X + [1] Y + [8]   
                                 >= [1] X + [1] Y + [3]   
                                 =  minus#(X,Y)           
          
                  le#(s(X),s(Y)) =  [0]                   
                                 >= [0]                   
                                 =  c_8(le#(X,Y))         
          
                       le(0(),Y) =  [3]                   
                                 >= [0]                   
                                 =  true()                
          
                    le(s(X),0()) =  [3]                   
                                 >= [0]                   
                                 =  false()               
          
                   le(s(X),s(Y)) =  [3]                   
                                 >= [3]                   
                                 =  le(X,Y)               
          
                    minus(X,0()) =  [1] X + [0]           
                                 >= [1] X + [0]           
                                 =  X                     
          
                   minus(X,s(Y)) =  [1] X + [0]           
                                 >= [1] X + [0]           
                                 =  pred(minus(X,Y))      
          
                      pred(s(X)) =  [1] X + [4]           
                                 >= [1] X + [0]           
                                 =  X                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:6.b:3: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
            gcd#(s(X),s(Y)) -> le#(Y,X)
            if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
            if#(false(),s(X),s(Y)) -> minus#(Y,X)
            if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
            if#(true(),s(X),s(Y)) -> minus#(X,Y)
            le#(s(X),s(Y)) -> c_8(le#(X,Y))
            minus#(X,s(Y)) -> c_10(minus#(X,Y))
        - Weak TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(X,0()) -> X
            minus(X,s(Y)) -> pred(minus(X,Y))
            pred(s(X)) -> X
        - Signature:
            {gcd/2,if/3,le/2,minus/2,pred/1,gcd#/2,if#/3,le#/2,minus#/2,pred#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0
            ,c_3/2,c_4/2,c_5/2,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {gcd#,if#,le#,minus#,pred#} and constructors {0,false,s
            ,true}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^2))