WORST_CASE(?,O(n^1))
* Step 1: DependencyPairs WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          bool2Nat#(False()) -> c_1()
          bool2Nat#(True()) -> c_2()
          e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
          e2#(a,b,res,False()) -> c_4()
          e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
          e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
          e4#(a,b,res,False()) -> c_7()
          e4#(a,b,res,True()) -> c_8()
          e5#(a,b,res,t) -> c_9()
          e6#(a,b,res,t) -> c_10()
          e7#(a,b,res,t) -> c_11()
          e8#(a,b,res,t) -> c_12()
          equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
          gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          help1#(0()) -> c_15()
          help1#(S(0())) -> c_16()
          help1#(S(S(x))) -> c_17()
          l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
          l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
          l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
          l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
          l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
          l16#(x,y,res,tmp,mtmp,t) -> c_28()
          l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          l2#(x,y,res,tmp,mtmp,True()) -> c_30()
          l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          l5#(x,y,res,tmp,mtmp,True()) -> c_34()
          l6#(x,y,res,tmp,mtmp,t) -> c_35()
          l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
          l8#(res,y,res',True(),mtmp,t) -> c_37()
          l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          l9#(res,y,res',tmp,mtmp,t) -> c_39()
          m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          m2#(0(),b,res,True()) -> c_42()
          m2#(S(0()),b,res,True()) -> c_43()
          m2#(S(S(x)),b,res,True()) -> c_44()
          m3#(0(),b,res,t) -> c_45()
          m3#(S(0()),b,res,t) -> c_46()
          m3#(S(S(x)),b,res,t) -> c_47()
          m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
          m5#(a,b,res,t) -> c_49()
          monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        Weak DPs
          <#(x,0()) -> c_51()
          <#(0(),S(y)) -> c_52()
          <#(S(x),S(y)) -> c_53(<#(x,y))
        
        and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bool2Nat#(False()) -> c_1()
            bool2Nat#(True()) -> c_2()
            e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
            e2#(a,b,res,False()) -> c_4()
            e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
            e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
            e4#(a,b,res,False()) -> c_7()
            e4#(a,b,res,True()) -> c_8()
            e5#(a,b,res,t) -> c_9()
            e6#(a,b,res,t) -> c_10()
            e7#(a,b,res,t) -> c_11()
            e8#(a,b,res,t) -> c_12()
            equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            help1#(0()) -> c_15()
            help1#(S(0())) -> c_16()
            help1#(S(S(x))) -> c_17()
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
            l16#(x,y,res,tmp,mtmp,t) -> c_28()
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l2#(x,y,res,tmp,mtmp,True()) -> c_30()
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,True()) -> c_34()
            l6#(x,y,res,tmp,mtmp,t) -> c_35()
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
            l8#(res,y,res',True(),mtmp,t) -> c_37()
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            l9#(res,y,res',tmp,mtmp,t) -> c_39()
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m2#(0(),b,res,True()) -> c_42()
            m2#(S(0()),b,res,True()) -> c_43()
            m2#(S(S(x)),b,res,True()) -> c_44()
            m3#(0(),b,res,t) -> c_45()
            m3#(S(0()),b,res,t) -> c_46()
            m3#(S(S(x)),b,res,t) -> c_47()
            m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
            m5#(a,b,res,t) -> c_49()
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak DPs:
            <#(x,0()) -> c_51()
            <#(0(),S(y)) -> c_52()
            <#(S(x),S(y)) -> c_53(<#(x,y))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/1,c_21/1,c_22/2,c_23/2,c_24/2,c_25/2,c_26/2
            ,c_27/2,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/2,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/2,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          <(x,0()) -> False()
          <(0(),S(y)) -> True()
          <(S(x),S(y)) -> <(x,y)
          e1(a,b,res,t) -> e2(a,b,res,<(a,b))
          e2(a,b,res,False()) -> False()
          e2(a,b,res,True()) -> e3(a,b,res,True())
          e3(a,b,res,t) -> e4(a,b,res,<(b,a))
          e4(a,b,res,False()) -> False()
          e4(a,b,res,True()) -> True()
          equal0(a,b) -> e1(a,b,False(),False())
          gcd(x,y) -> l1(x,y,0(),False(),False(),False())
          l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
          l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
          l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
          l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
          l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
          l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
          l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
          l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
          l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
          l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
          l16(x,y,res,tmp,mtmp,t) -> res
          l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
          l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
          l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
          l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
          l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
          l8(res,y,res',True(),mtmp,t) -> res
          l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
          m1(a,x,res,t) -> m2(a,x,res,False())
          m2(a,b,res,False()) -> m4(a,b,res,False())
          m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
          m5(a,b,res,t) -> res
          monus(a,b) -> m1(a,b,False(),False())
          <#(x,0()) -> c_51()
          <#(0(),S(y)) -> c_52()
          <#(S(x),S(y)) -> c_53(<#(x,y))
          bool2Nat#(False()) -> c_1()
          bool2Nat#(True()) -> c_2()
          e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
          e2#(a,b,res,False()) -> c_4()
          e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
          e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
          e4#(a,b,res,False()) -> c_7()
          e4#(a,b,res,True()) -> c_8()
          e5#(a,b,res,t) -> c_9()
          e6#(a,b,res,t) -> c_10()
          e7#(a,b,res,t) -> c_11()
          e8#(a,b,res,t) -> c_12()
          equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
          gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          help1#(0()) -> c_15()
          help1#(S(0())) -> c_16()
          help1#(S(S(x))) -> c_17()
          l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
          l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
          l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
          l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
          l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
          l16#(x,y,res,tmp,mtmp,t) -> c_28()
          l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          l2#(x,y,res,tmp,mtmp,True()) -> c_30()
          l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          l5#(x,y,res,tmp,mtmp,True()) -> c_34()
          l6#(x,y,res,tmp,mtmp,t) -> c_35()
          l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
          l8#(res,y,res',True(),mtmp,t) -> c_37()
          l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          l9#(res,y,res',tmp,mtmp,t) -> c_39()
          m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          m2#(0(),b,res,True()) -> c_42()
          m2#(S(0()),b,res,True()) -> c_43()
          m2#(S(S(x)),b,res,True()) -> c_44()
          m3#(0(),b,res,t) -> c_45()
          m3#(S(0()),b,res,t) -> c_46()
          m3#(S(S(x)),b,res,t) -> c_47()
          m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
          m5#(a,b,res,t) -> c_49()
          monus#(a,b) -> c_50(m1#(a,b,False(),False()))
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bool2Nat#(False()) -> c_1()
            bool2Nat#(True()) -> c_2()
            e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
            e2#(a,b,res,False()) -> c_4()
            e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
            e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
            e4#(a,b,res,False()) -> c_7()
            e4#(a,b,res,True()) -> c_8()
            e5#(a,b,res,t) -> c_9()
            e6#(a,b,res,t) -> c_10()
            e7#(a,b,res,t) -> c_11()
            e8#(a,b,res,t) -> c_12()
            equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            help1#(0()) -> c_15()
            help1#(S(0())) -> c_16()
            help1#(S(S(x))) -> c_17()
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
            l16#(x,y,res,tmp,mtmp,t) -> c_28()
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l2#(x,y,res,tmp,mtmp,True()) -> c_30()
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,True()) -> c_34()
            l6#(x,y,res,tmp,mtmp,t) -> c_35()
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
            l8#(res,y,res',True(),mtmp,t) -> c_37()
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            l9#(res,y,res',tmp,mtmp,t) -> c_39()
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m2#(0(),b,res,True()) -> c_42()
            m2#(S(0()),b,res,True()) -> c_43()
            m2#(S(S(x)),b,res,True()) -> c_44()
            m3#(0(),b,res,t) -> c_45()
            m3#(S(0()),b,res,t) -> c_46()
            m3#(S(S(x)),b,res,t) -> c_47()
            m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
            m5#(a,b,res,t) -> c_49()
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak DPs:
            <#(x,0()) -> c_51()
            <#(0(),S(y)) -> c_52()
            <#(S(x),S(y)) -> c_53(<#(x,y))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/1,c_21/1,c_22/2,c_23/2,c_24/2,c_25/2,c_26/2
            ,c_27/2,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/2,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/2,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} 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,4,7,8,9,10,11,12,15,16,17,28,30,34,35,37,39,42,43,44,45,46,47,49}
        by application of
          Pre({1,2,4,7,8,9,10,11,12,15,16,17,28,30,34,35,37,39,42,43,44,45,46,47,49}) = {3,6,23,24,26,27,36,48}.
        Here rules are labelled as follows:
          1: bool2Nat#(False()) -> c_1()
          2: bool2Nat#(True()) -> c_2()
          3: e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
          4: e2#(a,b,res,False()) -> c_4()
          5: e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
          6: e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
          7: e4#(a,b,res,False()) -> c_7()
          8: e4#(a,b,res,True()) -> c_8()
          9: e5#(a,b,res,t) -> c_9()
          10: e6#(a,b,res,t) -> c_10()
          11: e7#(a,b,res,t) -> c_11()
          12: e8#(a,b,res,t) -> c_12()
          13: equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
          14: gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          15: help1#(0()) -> c_15()
          16: help1#(S(0())) -> c_16()
          17: help1#(S(S(x))) -> c_17()
          18: l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          19: l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
          20: l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          21: l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          22: l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          23: l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
          24: l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
          25: l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          26: l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
          27: l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
          28: l16#(x,y,res,tmp,mtmp,t) -> c_28()
          29: l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          30: l2#(x,y,res,tmp,mtmp,True()) -> c_30()
          31: l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          32: l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          33: l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          34: l5#(x,y,res,tmp,mtmp,True()) -> c_34()
          35: l6#(x,y,res,tmp,mtmp,t) -> c_35()
          36: l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
          37: l8#(res,y,res',True(),mtmp,t) -> c_37()
          38: l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          39: l9#(res,y,res',tmp,mtmp,t) -> c_39()
          40: m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          41: m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          42: m2#(0(),b,res,True()) -> c_42()
          43: m2#(S(0()),b,res,True()) -> c_43()
          44: m2#(S(S(x)),b,res,True()) -> c_44()
          45: m3#(0(),b,res,t) -> c_45()
          46: m3#(S(0()),b,res,t) -> c_46()
          47: m3#(S(S(x)),b,res,t) -> c_47()
          48: m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
          49: m5#(a,b,res,t) -> c_49()
          50: monus#(a,b) -> c_50(m1#(a,b,False(),False()))
          51: <#(x,0()) -> c_51()
          52: <#(0(),S(y)) -> c_52()
          53: <#(S(x),S(y)) -> c_53(<#(x,y))
* Step 4: PredecessorEstimation WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
            e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
            e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
            equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak DPs:
            <#(x,0()) -> c_51()
            <#(0(),S(y)) -> c_52()
            <#(S(x),S(y)) -> c_53(<#(x,y))
            bool2Nat#(False()) -> c_1()
            bool2Nat#(True()) -> c_2()
            e2#(a,b,res,False()) -> c_4()
            e4#(a,b,res,False()) -> c_7()
            e4#(a,b,res,True()) -> c_8()
            e5#(a,b,res,t) -> c_9()
            e6#(a,b,res,t) -> c_10()
            e7#(a,b,res,t) -> c_11()
            e8#(a,b,res,t) -> c_12()
            help1#(0()) -> c_15()
            help1#(S(0())) -> c_16()
            help1#(S(S(x))) -> c_17()
            l16#(x,y,res,tmp,mtmp,t) -> c_28()
            l2#(x,y,res,tmp,mtmp,True()) -> c_30()
            l5#(x,y,res,tmp,mtmp,True()) -> c_34()
            l6#(x,y,res,tmp,mtmp,t) -> c_35()
            l8#(res,y,res',True(),mtmp,t) -> c_37()
            l9#(res,y,res',tmp,mtmp,t) -> c_39()
            m2#(0(),b,res,True()) -> c_42()
            m2#(S(0()),b,res,True()) -> c_43()
            m2#(S(S(x)),b,res,True()) -> c_44()
            m3#(0(),b,res,t) -> c_45()
            m3#(S(0()),b,res,t) -> c_46()
            m3#(S(S(x)),b,res,t) -> c_47()
            m5#(a,b,res,t) -> c_49()
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/1,c_21/1,c_22/2,c_23/2,c_24/2,c_25/2,c_26/2
            ,c_27/2,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/2,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/2,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {3}
        by application of
          Pre({3}) = {2}.
        Here rules are labelled as follows:
          1: e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
          2: e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
          3: e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
          4: equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
          5: gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          6: l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          7: l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
          8: l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          9: l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          10: l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          11: l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
          12: l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
          13: l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          14: l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
          15: l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
          16: l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          17: l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          18: l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          19: l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          20: l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
          21: l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          22: m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          23: m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          24: m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
          25: monus#(a,b) -> c_50(m1#(a,b,False(),False()))
          26: <#(x,0()) -> c_51()
          27: <#(0(),S(y)) -> c_52()
          28: <#(S(x),S(y)) -> c_53(<#(x,y))
          29: bool2Nat#(False()) -> c_1()
          30: bool2Nat#(True()) -> c_2()
          31: e2#(a,b,res,False()) -> c_4()
          32: e4#(a,b,res,False()) -> c_7()
          33: e4#(a,b,res,True()) -> c_8()
          34: e5#(a,b,res,t) -> c_9()
          35: e6#(a,b,res,t) -> c_10()
          36: e7#(a,b,res,t) -> c_11()
          37: e8#(a,b,res,t) -> c_12()
          38: help1#(0()) -> c_15()
          39: help1#(S(0())) -> c_16()
          40: help1#(S(S(x))) -> c_17()
          41: l16#(x,y,res,tmp,mtmp,t) -> c_28()
          42: l2#(x,y,res,tmp,mtmp,True()) -> c_30()
          43: l5#(x,y,res,tmp,mtmp,True()) -> c_34()
          44: l6#(x,y,res,tmp,mtmp,t) -> c_35()
          45: l8#(res,y,res',True(),mtmp,t) -> c_37()
          46: l9#(res,y,res',tmp,mtmp,t) -> c_39()
          47: m2#(0(),b,res,True()) -> c_42()
          48: m2#(S(0()),b,res,True()) -> c_43()
          49: m2#(S(S(x)),b,res,True()) -> c_44()
          50: m3#(0(),b,res,t) -> c_45()
          51: m3#(S(0()),b,res,t) -> c_46()
          52: m3#(S(S(x)),b,res,t) -> c_47()
          53: m5#(a,b,res,t) -> c_49()
* Step 5: PredecessorEstimation WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
            e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
            equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak DPs:
            <#(x,0()) -> c_51()
            <#(0(),S(y)) -> c_52()
            <#(S(x),S(y)) -> c_53(<#(x,y))
            bool2Nat#(False()) -> c_1()
            bool2Nat#(True()) -> c_2()
            e2#(a,b,res,False()) -> c_4()
            e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
            e4#(a,b,res,False()) -> c_7()
            e4#(a,b,res,True()) -> c_8()
            e5#(a,b,res,t) -> c_9()
            e6#(a,b,res,t) -> c_10()
            e7#(a,b,res,t) -> c_11()
            e8#(a,b,res,t) -> c_12()
            help1#(0()) -> c_15()
            help1#(S(0())) -> c_16()
            help1#(S(S(x))) -> c_17()
            l16#(x,y,res,tmp,mtmp,t) -> c_28()
            l2#(x,y,res,tmp,mtmp,True()) -> c_30()
            l5#(x,y,res,tmp,mtmp,True()) -> c_34()
            l6#(x,y,res,tmp,mtmp,t) -> c_35()
            l8#(res,y,res',True(),mtmp,t) -> c_37()
            l9#(res,y,res',tmp,mtmp,t) -> c_39()
            m2#(0(),b,res,True()) -> c_42()
            m2#(S(0()),b,res,True()) -> c_43()
            m2#(S(S(x)),b,res,True()) -> c_44()
            m3#(0(),b,res,t) -> c_45()
            m3#(S(0()),b,res,t) -> c_46()
            m3#(S(S(x)),b,res,t) -> c_47()
            m5#(a,b,res,t) -> c_49()
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/1,c_21/1,c_22/2,c_23/2,c_24/2,c_25/2,c_26/2
            ,c_27/2,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/2,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/2,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2}
        by application of
          Pre({2}) = {1}.
        Here rules are labelled as follows:
          1: e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
          2: e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
          3: equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
          4: gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          5: l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          6: l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
          7: l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          8: l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          9: l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          10: l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
          11: l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
          12: l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          13: l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
          14: l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
          15: l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          16: l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          17: l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          18: l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          19: l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
          20: l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          21: m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          22: m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          23: m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
          24: monus#(a,b) -> c_50(m1#(a,b,False(),False()))
          25: <#(x,0()) -> c_51()
          26: <#(0(),S(y)) -> c_52()
          27: <#(S(x),S(y)) -> c_53(<#(x,y))
          28: bool2Nat#(False()) -> c_1()
          29: bool2Nat#(True()) -> c_2()
          30: e2#(a,b,res,False()) -> c_4()
          31: e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
          32: e4#(a,b,res,False()) -> c_7()
          33: e4#(a,b,res,True()) -> c_8()
          34: e5#(a,b,res,t) -> c_9()
          35: e6#(a,b,res,t) -> c_10()
          36: e7#(a,b,res,t) -> c_11()
          37: e8#(a,b,res,t) -> c_12()
          38: help1#(0()) -> c_15()
          39: help1#(S(0())) -> c_16()
          40: help1#(S(S(x))) -> c_17()
          41: l16#(x,y,res,tmp,mtmp,t) -> c_28()
          42: l2#(x,y,res,tmp,mtmp,True()) -> c_30()
          43: l5#(x,y,res,tmp,mtmp,True()) -> c_34()
          44: l6#(x,y,res,tmp,mtmp,t) -> c_35()
          45: l8#(res,y,res',True(),mtmp,t) -> c_37()
          46: l9#(res,y,res',tmp,mtmp,t) -> c_39()
          47: m2#(0(),b,res,True()) -> c_42()
          48: m2#(S(0()),b,res,True()) -> c_43()
          49: m2#(S(S(x)),b,res,True()) -> c_44()
          50: m3#(0(),b,res,t) -> c_45()
          51: m3#(S(0()),b,res,t) -> c_46()
          52: m3#(S(S(x)),b,res,t) -> c_47()
          53: m5#(a,b,res,t) -> c_49()
* Step 6: PredecessorEstimation WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
            equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak DPs:
            <#(x,0()) -> c_51()
            <#(0(),S(y)) -> c_52()
            <#(S(x),S(y)) -> c_53(<#(x,y))
            bool2Nat#(False()) -> c_1()
            bool2Nat#(True()) -> c_2()
            e2#(a,b,res,False()) -> c_4()
            e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
            e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
            e4#(a,b,res,False()) -> c_7()
            e4#(a,b,res,True()) -> c_8()
            e5#(a,b,res,t) -> c_9()
            e6#(a,b,res,t) -> c_10()
            e7#(a,b,res,t) -> c_11()
            e8#(a,b,res,t) -> c_12()
            help1#(0()) -> c_15()
            help1#(S(0())) -> c_16()
            help1#(S(S(x))) -> c_17()
            l16#(x,y,res,tmp,mtmp,t) -> c_28()
            l2#(x,y,res,tmp,mtmp,True()) -> c_30()
            l5#(x,y,res,tmp,mtmp,True()) -> c_34()
            l6#(x,y,res,tmp,mtmp,t) -> c_35()
            l8#(res,y,res',True(),mtmp,t) -> c_37()
            l9#(res,y,res',tmp,mtmp,t) -> c_39()
            m2#(0(),b,res,True()) -> c_42()
            m2#(S(0()),b,res,True()) -> c_43()
            m2#(S(S(x)),b,res,True()) -> c_44()
            m3#(0(),b,res,t) -> c_45()
            m3#(S(0()),b,res,t) -> c_46()
            m3#(S(S(x)),b,res,t) -> c_47()
            m5#(a,b,res,t) -> c_49()
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/1,c_21/1,c_22/2,c_23/2,c_24/2,c_25/2,c_26/2
            ,c_27/2,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/2,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/2,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1}
        by application of
          Pre({1}) = {2}.
        Here rules are labelled as follows:
          1: e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
          2: equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
          3: gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          4: l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          5: l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
          6: l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          7: l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          8: l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          9: l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
          10: l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
          11: l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          12: l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
          13: l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
          14: l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          15: l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          16: l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          17: l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          18: l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
          19: l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          20: m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          21: m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          22: m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
          23: monus#(a,b) -> c_50(m1#(a,b,False(),False()))
          24: <#(x,0()) -> c_51()
          25: <#(0(),S(y)) -> c_52()
          26: <#(S(x),S(y)) -> c_53(<#(x,y))
          27: bool2Nat#(False()) -> c_1()
          28: bool2Nat#(True()) -> c_2()
          29: e2#(a,b,res,False()) -> c_4()
          30: e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
          31: e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
          32: e4#(a,b,res,False()) -> c_7()
          33: e4#(a,b,res,True()) -> c_8()
          34: e5#(a,b,res,t) -> c_9()
          35: e6#(a,b,res,t) -> c_10()
          36: e7#(a,b,res,t) -> c_11()
          37: e8#(a,b,res,t) -> c_12()
          38: help1#(0()) -> c_15()
          39: help1#(S(0())) -> c_16()
          40: help1#(S(S(x))) -> c_17()
          41: l16#(x,y,res,tmp,mtmp,t) -> c_28()
          42: l2#(x,y,res,tmp,mtmp,True()) -> c_30()
          43: l5#(x,y,res,tmp,mtmp,True()) -> c_34()
          44: l6#(x,y,res,tmp,mtmp,t) -> c_35()
          45: l8#(res,y,res',True(),mtmp,t) -> c_37()
          46: l9#(res,y,res',tmp,mtmp,t) -> c_39()
          47: m2#(0(),b,res,True()) -> c_42()
          48: m2#(S(0()),b,res,True()) -> c_43()
          49: m2#(S(S(x)),b,res,True()) -> c_44()
          50: m3#(0(),b,res,t) -> c_45()
          51: m3#(S(0()),b,res,t) -> c_46()
          52: m3#(S(S(x)),b,res,t) -> c_47()
          53: m5#(a,b,res,t) -> c_49()
* Step 7: PredecessorEstimation WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak DPs:
            <#(x,0()) -> c_51()
            <#(0(),S(y)) -> c_52()
            <#(S(x),S(y)) -> c_53(<#(x,y))
            bool2Nat#(False()) -> c_1()
            bool2Nat#(True()) -> c_2()
            e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
            e2#(a,b,res,False()) -> c_4()
            e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
            e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
            e4#(a,b,res,False()) -> c_7()
            e4#(a,b,res,True()) -> c_8()
            e5#(a,b,res,t) -> c_9()
            e6#(a,b,res,t) -> c_10()
            e7#(a,b,res,t) -> c_11()
            e8#(a,b,res,t) -> c_12()
            help1#(0()) -> c_15()
            help1#(S(0())) -> c_16()
            help1#(S(S(x))) -> c_17()
            l16#(x,y,res,tmp,mtmp,t) -> c_28()
            l2#(x,y,res,tmp,mtmp,True()) -> c_30()
            l5#(x,y,res,tmp,mtmp,True()) -> c_34()
            l6#(x,y,res,tmp,mtmp,t) -> c_35()
            l8#(res,y,res',True(),mtmp,t) -> c_37()
            l9#(res,y,res',tmp,mtmp,t) -> c_39()
            m2#(0(),b,res,True()) -> c_42()
            m2#(S(0()),b,res,True()) -> c_43()
            m2#(S(S(x)),b,res,True()) -> c_44()
            m3#(0(),b,res,t) -> c_45()
            m3#(S(0()),b,res,t) -> c_46()
            m3#(S(S(x)),b,res,t) -> c_47()
            m5#(a,b,res,t) -> c_49()
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/1,c_21/1,c_22/2,c_23/2,c_24/2,c_25/2,c_26/2
            ,c_27/2,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/2,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/2,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1}
        by application of
          Pre({1}) = {17}.
        Here rules are labelled as follows:
          1: equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
          2: gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          3: l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          4: l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
          5: l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          6: l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          7: l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          8: l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
          9: l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
          10: l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          11: l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
          12: l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
          13: l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          14: l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          15: l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          16: l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          17: l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
          18: l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          19: m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          20: m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          21: m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
          22: monus#(a,b) -> c_50(m1#(a,b,False(),False()))
          23: <#(x,0()) -> c_51()
          24: <#(0(),S(y)) -> c_52()
          25: <#(S(x),S(y)) -> c_53(<#(x,y))
          26: bool2Nat#(False()) -> c_1()
          27: bool2Nat#(True()) -> c_2()
          28: e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
          29: e2#(a,b,res,False()) -> c_4()
          30: e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
          31: e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
          32: e4#(a,b,res,False()) -> c_7()
          33: e4#(a,b,res,True()) -> c_8()
          34: e5#(a,b,res,t) -> c_9()
          35: e6#(a,b,res,t) -> c_10()
          36: e7#(a,b,res,t) -> c_11()
          37: e8#(a,b,res,t) -> c_12()
          38: help1#(0()) -> c_15()
          39: help1#(S(0())) -> c_16()
          40: help1#(S(S(x))) -> c_17()
          41: l16#(x,y,res,tmp,mtmp,t) -> c_28()
          42: l2#(x,y,res,tmp,mtmp,True()) -> c_30()
          43: l5#(x,y,res,tmp,mtmp,True()) -> c_34()
          44: l6#(x,y,res,tmp,mtmp,t) -> c_35()
          45: l8#(res,y,res',True(),mtmp,t) -> c_37()
          46: l9#(res,y,res',tmp,mtmp,t) -> c_39()
          47: m2#(0(),b,res,True()) -> c_42()
          48: m2#(S(0()),b,res,True()) -> c_43()
          49: m2#(S(S(x)),b,res,True()) -> c_44()
          50: m3#(0(),b,res,t) -> c_45()
          51: m3#(S(0()),b,res,t) -> c_46()
          52: m3#(S(S(x)),b,res,t) -> c_47()
          53: m5#(a,b,res,t) -> c_49()
* Step 8: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak DPs:
            <#(x,0()) -> c_51()
            <#(0(),S(y)) -> c_52()
            <#(S(x),S(y)) -> c_53(<#(x,y))
            bool2Nat#(False()) -> c_1()
            bool2Nat#(True()) -> c_2()
            e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
            e2#(a,b,res,False()) -> c_4()
            e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
            e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
            e4#(a,b,res,False()) -> c_7()
            e4#(a,b,res,True()) -> c_8()
            e5#(a,b,res,t) -> c_9()
            e6#(a,b,res,t) -> c_10()
            e7#(a,b,res,t) -> c_11()
            e8#(a,b,res,t) -> c_12()
            equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
            help1#(0()) -> c_15()
            help1#(S(0())) -> c_16()
            help1#(S(S(x))) -> c_17()
            l16#(x,y,res,tmp,mtmp,t) -> c_28()
            l2#(x,y,res,tmp,mtmp,True()) -> c_30()
            l5#(x,y,res,tmp,mtmp,True()) -> c_34()
            l6#(x,y,res,tmp,mtmp,t) -> c_35()
            l8#(res,y,res',True(),mtmp,t) -> c_37()
            l9#(res,y,res',tmp,mtmp,t) -> c_39()
            m2#(0(),b,res,True()) -> c_42()
            m2#(S(0()),b,res,True()) -> c_43()
            m2#(S(S(x)),b,res,True()) -> c_44()
            m3#(0(),b,res,t) -> c_45()
            m3#(S(0()),b,res,t) -> c_46()
            m3#(S(S(x)),b,res,t) -> c_47()
            m5#(a,b,res,t) -> c_49()
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/1,c_21/1,c_22/2,c_23/2,c_24/2,c_25/2,c_26/2
            ,c_27/2,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/2,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/2,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
             -->_1 l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False())):2
          
          2:S:l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
             -->_1 l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False())):12
          
          3:S:l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
             -->_2 <#(S(x),S(y)) -> c_53(<#(x,y)):24
             -->_1 l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True())):5
             -->_1 l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False())):4
             -->_2 <#(0(),S(y)) -> c_52():23
             -->_2 <#(x,0()) -> c_51():22
          
          4:S:l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
             -->_1 l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y)):9
          
          5:S:l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
             -->_1 l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y)):6
          
          6:S:l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
             -->_2 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
             -->_1 l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y)):8
             -->_1 l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y)):7
          
          7:S:l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
             -->_1 l16#(x,y,res,tmp,mtmp,t) -> c_28():41
             -->_2 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          8:S:l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
             -->_1 l16#(x,y,res,tmp,mtmp,t) -> c_28():41
             -->_2 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          9:S:l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
             -->_2 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
             -->_1 l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0()))):11
             -->_1 l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0())):10
          
          10:S:l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
             -->_1 l16#(x,y,res,tmp,mtmp,t) -> c_28():41
             -->_2 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          11:S:l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
             -->_1 l16#(x,y,res,tmp,mtmp,t) -> c_28():41
             -->_2 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          12:S:l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
             -->_1 l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t)):13
          
          13:S:l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
             -->_1 l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False())):14
          
          14:S:l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
             -->_1 l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False())):15
          
          15:S:l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
             -->_1 l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y)):16
          
          16:S:l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
             -->_2 equal0#(a,b) -> c_13(e1#(a,b,False(),False())):37
             -->_1 l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t)):17
             -->_1 l8#(res,y,res',True(),mtmp,t) -> c_37():45
          
          17:S:l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
             -->_1 l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y)):3
          
          18:S:m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
             -->_1 m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False())):19
          
          19:S:m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
             -->_1 m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x)):20
          
          20:S:m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
             -->_2 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
             -->_1 m5#(a,b,res,t) -> c_49():53
          
          21:S:monus#(a,b) -> c_50(m1#(a,b,False(),False()))
             -->_1 m1#(a,x,res,t) -> c_40(m2#(a,x,res,False())):18
          
          22:W:<#(x,0()) -> c_51()
             
          
          23:W:<#(0(),S(y)) -> c_52()
             
          
          24:W:<#(S(x),S(y)) -> c_53(<#(x,y))
             -->_1 <#(S(x),S(y)) -> c_53(<#(x,y)):24
             -->_1 <#(0(),S(y)) -> c_52():23
             -->_1 <#(x,0()) -> c_51():22
          
          25:W:bool2Nat#(False()) -> c_1()
             
          
          26:W:bool2Nat#(True()) -> c_2()
             
          
          27:W:e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
             -->_1 e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True())):29
             -->_1 e2#(a,b,res,False()) -> c_4():28
             -->_2 <#(S(x),S(y)) -> c_53(<#(x,y)):24
             -->_2 <#(0(),S(y)) -> c_52():23
             -->_2 <#(x,0()) -> c_51():22
          
          28:W:e2#(a,b,res,False()) -> c_4()
             
          
          29:W:e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
             -->_1 e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a)):30
          
          30:W:e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
             -->_1 e4#(a,b,res,True()) -> c_8():32
             -->_1 e4#(a,b,res,False()) -> c_7():31
             -->_2 <#(S(x),S(y)) -> c_53(<#(x,y)):24
             -->_2 <#(0(),S(y)) -> c_52():23
             -->_2 <#(x,0()) -> c_51():22
          
          31:W:e4#(a,b,res,False()) -> c_7()
             
          
          32:W:e4#(a,b,res,True()) -> c_8()
             
          
          33:W:e5#(a,b,res,t) -> c_9()
             
          
          34:W:e6#(a,b,res,t) -> c_10()
             
          
          35:W:e7#(a,b,res,t) -> c_11()
             
          
          36:W:e8#(a,b,res,t) -> c_12()
             
          
          37:W:equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
             -->_1 e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b)):27
          
          38:W:help1#(0()) -> c_15()
             
          
          39:W:help1#(S(0())) -> c_16()
             
          
          40:W:help1#(S(S(x))) -> c_17()
             
          
          41:W:l16#(x,y,res,tmp,mtmp,t) -> c_28()
             
          
          42:W:l2#(x,y,res,tmp,mtmp,True()) -> c_30()
             
          
          43:W:l5#(x,y,res,tmp,mtmp,True()) -> c_34()
             
          
          44:W:l6#(x,y,res,tmp,mtmp,t) -> c_35()
             
          
          45:W:l8#(res,y,res',True(),mtmp,t) -> c_37()
             
          
          46:W:l9#(res,y,res',tmp,mtmp,t) -> c_39()
             
          
          47:W:m2#(0(),b,res,True()) -> c_42()
             
          
          48:W:m2#(S(0()),b,res,True()) -> c_43()
             
          
          49:W:m2#(S(S(x)),b,res,True()) -> c_44()
             
          
          50:W:m3#(0(),b,res,t) -> c_45()
             
          
          51:W:m3#(S(0()),b,res,t) -> c_46()
             
          
          52:W:m3#(S(S(x)),b,res,t) -> c_47()
             
          
          53:W:m5#(a,b,res,t) -> c_49()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          52: m3#(S(S(x)),b,res,t) -> c_47()
          51: m3#(S(0()),b,res,t) -> c_46()
          50: m3#(0(),b,res,t) -> c_45()
          49: m2#(S(S(x)),b,res,True()) -> c_44()
          48: m2#(S(0()),b,res,True()) -> c_43()
          47: m2#(0(),b,res,True()) -> c_42()
          46: l9#(res,y,res',tmp,mtmp,t) -> c_39()
          44: l6#(x,y,res,tmp,mtmp,t) -> c_35()
          43: l5#(x,y,res,tmp,mtmp,True()) -> c_34()
          42: l2#(x,y,res,tmp,mtmp,True()) -> c_30()
          40: help1#(S(S(x))) -> c_17()
          39: help1#(S(0())) -> c_16()
          38: help1#(0()) -> c_15()
          36: e8#(a,b,res,t) -> c_12()
          35: e7#(a,b,res,t) -> c_11()
          34: e6#(a,b,res,t) -> c_10()
          33: e5#(a,b,res,t) -> c_9()
          26: bool2Nat#(True()) -> c_2()
          25: bool2Nat#(False()) -> c_1()
          45: l8#(res,y,res',True(),mtmp,t) -> c_37()
          41: l16#(x,y,res,tmp,mtmp,t) -> c_28()
          53: m5#(a,b,res,t) -> c_49()
          37: equal0#(a,b) -> c_13(e1#(a,b,False(),False()))
          27: e1#(a,b,res,t) -> c_3(e2#(a,b,res,<(a,b)),<#(a,b))
          28: e2#(a,b,res,False()) -> c_4()
          29: e2#(a,b,res,True()) -> c_5(e3#(a,b,res,True()))
          30: e3#(a,b,res,t) -> c_6(e4#(a,b,res,<(b,a)),<#(b,a))
          24: <#(S(x),S(y)) -> c_53(<#(x,y))
          22: <#(x,0()) -> c_51()
          23: <#(0(),S(y)) -> c_52()
          31: e4#(a,b,res,False()) -> c_7()
          32: e4#(a,b,res,True()) -> c_8()
* Step 9: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/1,c_21/1,c_22/2,c_23/2,c_24/2,c_25/2,c_26/2
            ,c_27/2,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/2,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/2,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
             -->_1 l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False())):2
          
          2:S:l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
             -->_1 l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False())):12
          
          3:S:l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y))
             -->_1 l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True())):5
             -->_1 l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False())):4
          
          4:S:l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
             -->_1 l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y)):9
          
          5:S:l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
             -->_1 l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y)):6
          
          6:S:l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
             -->_2 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
             -->_1 l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y)):8
             -->_1 l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y)):7
          
          7:S:l13#(x,y,res,tmp,False(),t) -> c_23(l16#(x,y,gcd(0(),y),tmp,False(),t),gcd#(0(),y))
             -->_2 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          8:S:l13#(x,y,res,tmp,True(),t) -> c_24(l16#(x,y,gcd(S(0()),y),tmp,True(),t),gcd#(S(0()),y))
             -->_2 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          9:S:l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
             -->_2 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
             -->_1 l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0()))):11
             -->_1 l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0())):10
          
          10:S:l15#(x,y,res,tmp,False(),t) -> c_26(l16#(x,y,gcd(y,0()),tmp,False(),t),gcd#(y,0()))
             -->_2 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          11:S:l15#(x,y,res,tmp,True(),t) -> c_27(l16#(x,y,gcd(y,S(0())),tmp,True(),t),gcd#(y,S(0())))
             -->_2 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          12:S:l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
             -->_1 l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t)):13
          
          13:S:l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
             -->_1 l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False())):14
          
          14:S:l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
             -->_1 l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False())):15
          
          15:S:l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
             -->_1 l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y)):16
          
          16:S:l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t),equal0#(x,y))
             -->_1 l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t)):17
          
          17:S:l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
             -->_1 l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)),<#(x,y)):3
          
          18:S:m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
             -->_1 m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False())):19
          
          19:S:m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
             -->_1 m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x)):20
          
          20:S:m4#(S(x'),S(x),res,t) -> c_48(m5#(S(x'),S(x),monus(x',x),t),monus#(x',x))
             -->_2 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
          
          21:S:monus#(a,b) -> c_50(m1#(a,b,False(),False()))
             -->_1 m1#(a,x,res,t) -> c_40(m2#(a,x,res,False())):18
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
          l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
          l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
          l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
          l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
          l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
          m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
* Step 10: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/1,c_21/1,c_22/2,c_23/1,c_24/1,c_25/2,c_26/1
            ,c_27/1,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/1,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/1,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          <(x,0()) -> False()
          <(0(),S(y)) -> True()
          <(S(x),S(y)) -> <(x,y)
          e1(a,b,res,t) -> e2(a,b,res,<(a,b))
          e2(a,b,res,False()) -> False()
          e2(a,b,res,True()) -> e3(a,b,res,True())
          e3(a,b,res,t) -> e4(a,b,res,<(b,a))
          e4(a,b,res,False()) -> False()
          e4(a,b,res,True()) -> True()
          equal0(a,b) -> e1(a,b,False(),False())
          m1(a,x,res,t) -> m2(a,x,res,False())
          m2(a,b,res,False()) -> m4(a,b,res,False())
          m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
          m5(a,b,res,t) -> res
          monus(a,b) -> m1(a,b,False(),False())
          gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
          l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
          l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
          l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
          l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
          l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
          l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
          monus#(a,b) -> c_50(m1#(a,b,False(),False()))
* Step 11: PredecessorEstimationCP WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/1,c_21/1,c_22/2,c_23/1,c_24/1,c_25/2,c_26/1
            ,c_27/1,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/1,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/1,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          17: l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          20: m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
          
        Consider the set of all dependency pairs
          1: gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          2: l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          3: l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
          4: l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          5: l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          6: l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          7: l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
          8: l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
          9: l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          10: l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
          11: l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
          12: l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          13: l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          14: l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          15: l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          16: l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
          17: l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          18: m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
          19: m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          20: m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
          21: monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        Processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
        SPACE(?,?)on application of the dependency pairs
          {17,20}
        These cover all (indirect) predecessors of dependency pairs
          {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21}
        their number of applications is equally bounded.
        The dependency pairs are shifted into the weak component.
** Step 11.a:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/1,c_21/1,c_22/2,c_23/1,c_24/1,c_25/2,c_26/1
            ,c_27/1,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/1,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/1,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_14) = {1},
          uargs(c_18) = {1},
          uargs(c_19) = {1},
          uargs(c_20) = {1},
          uargs(c_21) = {1},
          uargs(c_22) = {1,2},
          uargs(c_23) = {1},
          uargs(c_24) = {1},
          uargs(c_25) = {1,2},
          uargs(c_26) = {1},
          uargs(c_27) = {1},
          uargs(c_29) = {1},
          uargs(c_31) = {1},
          uargs(c_32) = {1},
          uargs(c_33) = {1},
          uargs(c_36) = {1},
          uargs(c_38) = {1},
          uargs(c_40) = {1},
          uargs(c_41) = {1},
          uargs(c_48) = {1},
          uargs(c_50) = {1}
        
        Following symbols are considered usable:
          {m1,m2,m4,m5,monus,<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#,help1#,l1#,l10#,l11#,l12#
          ,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#,monus#}
        TcT has computed the following interpretation:
                  p(0) = [0]                                                       
                         [0]                                                       
                  p(<) = [0]                                                       
                         [0]                                                       
              p(False) = [0]                                                       
                         [1]                                                       
                  p(S) = [0 0] x1 + [0]                                            
                         [0 1]      [1]                                            
               p(True) = [1]                                                       
                         [1]                                                       
           p(bool2Nat) = [0]                                                       
                         [0]                                                       
                 p(e1) = [0 1] x3 + [0 0] x4 + [0]                                 
                         [0 0]      [0 1]      [0]                                 
                 p(e2) = [0 1] x1 + [0 1] x2 + [1]                                 
                         [1 0]      [1 1]      [1]                                 
                 p(e3) = [1 1] x4 + [0]                                            
                         [0 1]      [0]                                            
                 p(e4) = [0 0] x1 + [0]                                            
                         [1 0]      [0]                                            
                 p(e5) = [0]                                                       
                         [0]                                                       
                 p(e6) = [0]                                                       
                         [0]                                                       
                 p(e7) = [0]                                                       
                         [0]                                                       
                 p(e8) = [0]                                                       
                         [0]                                                       
             p(equal0) = [0]                                                       
                         [0]                                                       
                p(gcd) = [0]                                                       
                         [0]                                                       
              p(help1) = [0]                                                       
                         [0]                                                       
                 p(l1) = [0]                                                       
                         [0]                                                       
                p(l10) = [0]                                                       
                         [0]                                                       
                p(l11) = [0]                                                       
                         [0]                                                       
                p(l12) = [0]                                                       
                         [0]                                                       
                p(l13) = [0]                                                       
                         [0]                                                       
                p(l14) = [0]                                                       
                         [0]                                                       
                p(l15) = [0]                                                       
                         [0]                                                       
                p(l16) = [0]                                                       
                         [0]                                                       
                 p(l2) = [0]                                                       
                         [0]                                                       
                 p(l3) = [0]                                                       
                         [0]                                                       
                 p(l4) = [0]                                                       
                         [0]                                                       
                 p(l5) = [0]                                                       
                         [0]                                                       
                 p(l6) = [0]                                                       
                         [0]                                                       
                 p(l7) = [0]                                                       
                         [0]                                                       
                 p(l8) = [0]                                                       
                         [0]                                                       
                 p(l9) = [0]                                                       
                         [0]                                                       
                 p(m1) = [0 0] x3 + [0]                                            
                         [1 0]      [0]                                            
                 p(m2) = [0]                                                       
                         [0]                                                       
                 p(m3) = [0]                                                       
                         [0]                                                       
                 p(m4) = [0]                                                       
                         [0]                                                       
                 p(m5) = [1 0] x3 + [0]                                            
                         [0 1]      [0]                                            
              p(monus) = [0]                                                       
                         [0]                                                       
                 p(<#) = [0]                                                       
                         [0]                                                       
          p(bool2Nat#) = [0]                                                       
                         [0]                                                       
                p(e1#) = [0]                                                       
                         [0]                                                       
                p(e2#) = [0]                                                       
                         [0]                                                       
                p(e3#) = [0]                                                       
                         [0]                                                       
                p(e4#) = [0]                                                       
                         [0]                                                       
                p(e5#) = [0]                                                       
                         [0]                                                       
                p(e6#) = [0]                                                       
                         [0]                                                       
                p(e7#) = [0]                                                       
                         [0]                                                       
                p(e8#) = [0]                                                       
                         [0]                                                       
            p(equal0#) = [0]                                                       
                         [0]                                                       
               p(gcd#) = [0 1] x1 + [0 1] x2 + [1]                                 
                         [0 0]      [0 1]      [0]                                 
             p(help1#) = [0]                                                       
                         [0]                                                       
                p(l1#) = [0 1] x1 + [0 1] x2 + [1 1] x3 + [1 0] x4 + [1 0] x5 + [1]
                         [0 1]      [1 1]      [1 1]      [0 1]      [1 1]      [1]
               p(l10#) = [0 1] x1 + [0 1] x2 + [1 0] x3 + [1 0] x4 + [1 0] x5 + [0]
                         [1 1]      [1 1]      [1 1]      [0 1]      [0 1]      [1]
               p(l11#) = [0 1] x1 + [0 1] x2 + [0 0] x3 + [1 0] x4 + [1 0] x5 + [0]
                         [1 1]      [0 0]      [1 1]      [0 0]      [0 0]      [1]
               p(l12#) = [0 1] x1 + [0 1] x2 + [0 0] x4 + [1 0] x5 + [0 0] x6 + [0]
                         [1 1]      [1 1]      [1 0]      [0 0]      [0 1]      [0]
               p(l13#) = [0 1] x2 + [1 1] x5 + [0]                                 
                         [0 1]      [0 0]      [1]                                 
               p(l14#) = [0 1] x1 + [0 1] x2 + [0 0] x3 + [1 0] x4 + [0]           
                         [0 0]      [0 1]      [0 1]      [0 0]      [0]           
               p(l15#) = [0 1] x2 + [1 1] x5 + [0]                                 
                         [1 0]      [0 1]      [0]                                 
               p(l16#) = [0]                                                       
                         [0]                                                       
                p(l2#) = [0 1] x1 + [0 1] x2 + [1 0] x3 + [1 0] x5 + [0 1] x6 + [0]
                         [0 0]      [1 0]      [0 0]      [1 0]      [0 0]      [1]
                p(l3#) = [0 1] x1 + [0 1] x2 + [0 0] x4 + [1 0] x5 + [1 0] x6 + [1]
                         [0 1]      [1 1]      [0 1]      [1 0]      [0 0]      [1]
                p(l4#) = [0 1] x1 + [0 1] x2 + [1 0] x3 + [0 0] x4 + [1 0] x5 + [1]
                         [0 1]      [0 0]      [0 0]      [0 1]      [0 0]      [0]
                p(l5#) = [0 1] x1 + [0 1] x2 + [1 0] x3 + [0 0] x4 + [1 0] x5 + [1]
                         [0 1]      [1 1]      [1 0]      [1 1]      [1 0]      [1]
                p(l6#) = [0]                                                       
                         [0]                                                       
                p(l7#) = [0 1] x1 + [0 1] x2 + [1 0] x3 + [1 0] x5 + [1]           
                         [0 1]      [1 1]      [1 1]      [1 1]      [1]           
                p(l8#) = [0 1] x1 + [0 1] x2 + [1 0] x3 + [1 0] x5 + [1]           
                         [1 0]      [0 0]      [0 0]      [0 1]      [1]           
                p(l9#) = [0]                                                       
                         [0]                                                       
                p(m1#) = [0 1] x1 + [1 0] x3 + [0]                                 
                         [1 1]      [0 1]      [1]                                 
                p(m2#) = [0 1] x1 + [0 0] x4 + [0]                                 
                         [0 1]      [0 1]      [0]                                 
                p(m3#) = [0]                                                       
                         [0]                                                       
                p(m4#) = [0 1] x1 + [0]                                            
                         [0 1]      [0]                                            
                p(m5#) = [0]                                                       
                         [0]                                                       
             p(monus#) = [0 1] x1 + [0]                                            
                         [0 0]      [1]                                            
                p(c_1) = [0]                                                       
                         [0]                                                       
                p(c_2) = [0]                                                       
                         [0]                                                       
                p(c_3) = [0]                                                       
                         [0]                                                       
                p(c_4) = [0]                                                       
                         [0]                                                       
                p(c_5) = [0]                                                       
                         [0]                                                       
                p(c_6) = [0]                                                       
                         [0]                                                       
                p(c_7) = [0]                                                       
                         [0]                                                       
                p(c_8) = [0]                                                       
                         [0]                                                       
                p(c_9) = [0]                                                       
                         [0]                                                       
               p(c_10) = [0]                                                       
                         [0]                                                       
               p(c_11) = [0]                                                       
                         [0]                                                       
               p(c_12) = [0]                                                       
                         [0]                                                       
               p(c_13) = [0]                                                       
                         [0]                                                       
               p(c_14) = [1 0] x1 + [0]                                            
                         [0 0]      [0]                                            
               p(c_15) = [0]                                                       
                         [0]                                                       
               p(c_16) = [0]                                                       
                         [0]                                                       
               p(c_17) = [0]                                                       
                         [0]                                                       
               p(c_18) = [1 0] x1 + [0]                                            
                         [1 0]      [0]                                            
               p(c_19) = [1 0] x1 + [0]                                            
                         [0 1]      [0]                                            
               p(c_20) = [1 0] x1 + [0]                                            
                         [0 0]      [1]                                            
               p(c_21) = [1 0] x1 + [0]                                            
                         [0 0]      [1]                                            
               p(c_22) = [1 0] x1 + [1 0] x2 + [0]                                 
                         [0 0]      [0 0]      [0]                                 
               p(c_23) = [1 0] x1 + [0]                                            
                         [1 0]      [0]                                            
               p(c_24) = [1 0] x1 + [0]                                            
                         [0 0]      [1]                                            
               p(c_25) = [1 0] x1 + [1 0] x2 + [0]                                 
                         [1 0]      [0 0]      [0]                                 
               p(c_26) = [1 0] x1 + [0]                                            
                         [0 0]      [1]                                            
               p(c_27) = [1 0] x1 + [0]                                            
                         [0 1]      [0]                                            
               p(c_28) = [0]                                                       
                         [0]                                                       
               p(c_29) = [1 0] x1 + [0]                                            
                         [0 0]      [0]                                            
               p(c_30) = [0]                                                       
                         [0]                                                       
               p(c_31) = [1 0] x1 + [0]                                            
                         [1 0]      [0]                                            
               p(c_32) = [1 0] x1 + [0]                                            
                         [0 0]      [0]                                            
               p(c_33) = [1 0] x1 + [0]                                            
                         [1 0]      [0]                                            
               p(c_34) = [0]                                                       
                         [0]                                                       
               p(c_35) = [0]                                                       
                         [0]                                                       
               p(c_36) = [1 0] x1 + [0]                                            
                         [1 0]      [0]                                            
               p(c_37) = [0]                                                       
                         [0]                                                       
               p(c_38) = [1 0] x1 + [0]                                            
                         [0 0]      [1]                                            
               p(c_39) = [0]                                                       
                         [0]                                                       
               p(c_40) = [1 0] x1 + [0]                                            
                         [1 0]      [1]                                            
               p(c_41) = [1 0] x1 + [0]                                            
                         [0 1]      [0]                                            
               p(c_42) = [0]                                                       
                         [0]                                                       
               p(c_43) = [0]                                                       
                         [0]                                                       
               p(c_44) = [0]                                                       
                         [0]                                                       
               p(c_45) = [0]                                                       
                         [0]                                                       
               p(c_46) = [0]                                                       
                         [0]                                                       
               p(c_47) = [0]                                                       
                         [0]                                                       
               p(c_48) = [1 0] x1 + [0]                                            
                         [1 1]      [0]                                            
               p(c_49) = [0]                                                       
                         [0]                                                       
               p(c_50) = [1 0] x1 + [0]                                            
                         [0 0]      [0]                                            
               p(c_51) = [0]                                                       
                         [0]                                                       
               p(c_52) = [0]                                                       
                         [0]                                                       
               p(c_53) = [0]                                                       
                         [0]                                                       
        
        Following rules are strictly oriented:
        l8#(x,y,res,False(),mtmp,t) = [1 0] mtmp + [1 0] res + [0 1] x + [0 1] y + [1]
                                      [0 1]        [0 0]       [1 0]     [0 0]     [1]
                                    > [1 0] mtmp + [1 0] res + [0 1] x + [0 1] y + [0]
                                      [0 0]        [0 0]       [0 0]     [0 0]     [1]
                                    = c_38(l10#(x,y,res,False(),mtmp,t))              
        
              m4#(S(x'),S(x),res,t) = [0 1] x' + [1]                                  
                                      [0 1]      [1]                                  
                                    > [0 1] x' + [0]                                  
                                      [0 1]      [1]                                  
                                    = c_48(monus#(x',x))                              
        
        
        Following rules are (at-least) weakly oriented:
                             gcd#(x,y) =  [0 1] x + [0 1] y + [1]                                      
                                          [0 0]     [0 1]     [0]                                      
                                       >= [0 1] x + [0 1] y + [1]                                      
                                          [0 0]     [0 0]     [0]                                      
                                       =  c_14(l1#(x,y,0(),False(),False(),False()))                   
        
               l1#(x,y,res,tmp,mtmp,t) =  [1 0] mtmp + [1 1] res + [1 0] tmp + [0 1] x + [0 1] y + [1] 
                                          [1 1]        [1 1]       [0 1]       [0 1]     [1 1]     [1] 
                                       >= [1 0] mtmp + [1 0] res + [0 1] x + [0 1] y + [1]             
                                          [1 0]        [1 0]       [0 1]     [0 1]     [1]             
                                       =  c_18(l2#(x,y,res,tmp,mtmp,False()))                          
        
              l10#(x,y,res,tmp,mtmp,t) =  [1 0] mtmp + [1 0] res + [1 0] tmp + [0 1] x + [0 1] y + [0] 
                                          [0 1]        [1 1]       [0 1]       [1 1]     [1 1]     [1] 
                                       >= [1 0] mtmp + [0 0] res + [1 0] tmp + [0 1] x + [0 1] y + [0] 
                                          [0 0]        [1 1]       [0 0]       [1 1]     [0 0]     [1] 
                                       =  c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))                          
        
        l11#(x,y,res,tmp,mtmp,False()) =  [1 0] mtmp + [0 0] res + [1 0] tmp + [0 1] x + [0 1] y + [0] 
                                          [0 0]        [1 1]       [0 0]       [1 1]     [0 0]     [1] 
                                       >= [1 0] tmp + [0 1] x + [0 1] y + [0]                          
                                          [0 0]       [0 0]     [0 0]     [1]                          
                                       =  c_20(l14#(x,y,res,tmp,mtmp,False()))                         
        
         l11#(x,y,res,tmp,mtmp,True()) =  [1 0] mtmp + [0 0] res + [1 0] tmp + [0 1] x + [0 1] y + [0] 
                                          [0 0]        [1 1]       [0 0]       [1 1]     [0 0]     [1] 
                                       >= [1 0] mtmp + [0 1] x + [0 1] y + [0]                         
                                          [0 0]        [0 0]     [0 0]     [1]                         
                                       =  c_21(l12#(x,y,res,tmp,mtmp,True()))                          
        
              l12#(x,y,res,tmp,mtmp,t) =  [1 0] mtmp + [0 0] t + [0 0] tmp + [0 1] x + [0 1] y + [0]   
                                          [0 0]        [0 1]     [1 0]       [1 1]     [1 1]     [0]   
                                       >= [0 1] x + [0 1] y + [0]                                      
                                          [0 0]     [0 0]     [0]                                      
                                       =  c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))             
        
           l13#(x,y,res,tmp,False(),t) =  [0 1] y + [1]                                                
                                          [0 1]     [1]                                                
                                       >= [0 1] y + [1]                                                
                                          [0 1]     [1]                                                
                                       =  c_23(gcd#(0(),y))                                            
        
            l13#(x,y,res,tmp,True(),t) =  [0 1] y + [2]                                                
                                          [0 1]     [1]                                                
                                       >= [0 1] y + [2]                                                
                                          [0 0]     [1]                                                
                                       =  c_24(gcd#(S(0()),y))                                         
        
              l14#(x,y,res,tmp,mtmp,t) =  [0 0] res + [1 0] tmp + [0 1] x + [0 1] y + [0]              
                                          [0 1]       [0 0]       [0 0]     [0 1]     [0]              
                                       >= [0 1] x + [0 1] y + [0]                                      
                                          [0 0]     [0 1]     [0]                                      
                                       =  c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))             
        
           l15#(x,y,res,tmp,False(),t) =  [0 1] y + [1]                                                
                                          [1 0]     [1]                                                
                                       >= [0 1] y + [1]                                                
                                          [0 0]     [1]                                                
                                       =  c_26(gcd#(y,0()))                                            
        
            l15#(x,y,res,tmp,True(),t) =  [0 1] y + [2]                                                
                                          [1 0]     [1]                                                
                                       >= [0 1] y + [2]                                                
                                          [0 0]     [1]                                                
                                       =  c_27(gcd#(y,S(0())))                                         
        
         l2#(x,y,res,tmp,mtmp,False()) =  [1 0] mtmp + [1 0] res + [0 1] x + [0 1] y + [1]             
                                          [1 0]        [0 0]       [0 0]     [1 0]     [1]             
                                       >= [1 0] mtmp + [0 1] x + [0 1] y + [1]                         
                                          [0 0]        [0 0]     [0 0]     [0]                         
                                       =  c_29(l3#(x,y,res,tmp,mtmp,False()))                          
        
               l3#(x,y,res,tmp,mtmp,t) =  [1 0] mtmp + [1 0] t + [0 0] tmp + [0 1] x + [0 1] y + [1]   
                                          [1 0]        [0 0]     [0 1]       [0 1]     [1 1]     [1]   
                                       >= [1 0] mtmp + [0 1] x + [0 1] y + [1]                         
                                          [1 0]        [0 1]     [0 1]     [1]                         
                                       =  c_31(l4#(x,y,0(),tmp,mtmp,t))                                
        
              l4#(x',x,res,tmp,mtmp,t) =  [1 0] mtmp + [1 0] res + [0 0] tmp + [0 1] x + [0 1] x' + [1]
                                          [0 0]        [0 0]       [0 1]       [0 0]     [0 1]      [0]
                                       >= [1 0] mtmp + [1 0] res + [0 1] x + [0 1] x' + [1]            
                                          [0 0]        [0 0]       [0 0]     [0 0]      [0]            
                                       =  c_32(l5#(x',x,res,tmp,mtmp,False()))                         
        
         l5#(x,y,res,tmp,mtmp,False()) =  [1 0] mtmp + [1 0] res + [0 0] tmp + [0 1] x + [0 1] y + [1] 
                                          [1 0]        [1 0]       [1 1]       [0 1]     [1 1]     [1] 
                                       >= [1 0] mtmp + [1 0] res + [0 1] x + [0 1] y + [1]             
                                          [1 0]        [1 0]       [0 1]     [0 1]     [1]             
                                       =  c_33(l7#(x,y,res,tmp,mtmp,False()))                          
        
               l7#(x,y,res,tmp,mtmp,t) =  [1 0] mtmp + [1 0] res + [0 1] x + [0 1] y + [1]             
                                          [1 1]        [1 1]       [0 1]     [1 1]     [1]             
                                       >= [1 0] mtmp + [1 0] res + [0 1] x + [0 1] y + [1]             
                                          [1 0]        [1 0]       [0 1]     [0 1]     [1]             
                                       =  c_36(l8#(x,y,res,equal0(x,y),mtmp,t))                        
        
                        m1#(a,x,res,t) =  [0 1] a + [1 0] res + [0]                                    
                                          [1 1]     [0 1]       [1]                                    
                                       >= [0 1] a + [0]                                                
                                          [0 1]     [1]                                                
                                       =  c_40(m2#(a,x,res,False()))                                   
        
                  m2#(a,b,res,False()) =  [0 1] a + [0]                                                
                                          [0 1]     [1]                                                
                                       >= [0 1] a + [0]                                                
                                          [0 1]     [0]                                                
                                       =  c_41(m4#(a,b,res,False()))                                   
        
                           monus#(a,b) =  [0 1] a + [0]                                                
                                          [0 0]     [1]                                                
                                       >= [0 1] a + [0]                                                
                                          [0 0]     [0]                                                
                                       =  c_50(m1#(a,b,False(),False()))                               
        
                         m1(a,x,res,t) =  [0 0] res + [0]                                              
                                          [1 0]       [0]                                              
                                       >= [0]                                                          
                                          [0]                                                          
                                       =  m2(a,x,res,False())                                          
        
                   m2(a,b,res,False()) =  [0]                                                          
                                          [0]                                                          
                                       >= [0]                                                          
                                          [0]                                                          
                                       =  m4(a,b,res,False())                                          
        
                  m4(S(x'),S(x),res,t) =  [0]                                                          
                                          [0]                                                          
                                       >= [0]                                                          
                                          [0]                                                          
                                       =  m5(S(x'),S(x),monus(x',x),t)                                 
        
                         m5(a,b,res,t) =  [1 0] res + [0]                                              
                                          [0 1]       [0]                                              
                                       >= [1 0] res + [0]                                              
                                          [0 1]       [0]                                              
                                       =  res                                                          
        
                            monus(a,b) =  [0]                                                          
                                          [0]                                                          
                                       >= [0]                                                          
                                          [0]                                                          
                                       =  m1(a,b,False(),False())                                      
        
** Step 11.a:2: Assumption WORST_CASE(?,O(1))
    + Considered Problem:
        - Strict DPs:
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak DPs:
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/1,c_21/1,c_22/2,c_23/1,c_24/1,c_25/2,c_26/1
            ,c_27/1,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/1,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/1,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
    + Details:
        ()

** Step 11.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
            l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
            l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
            l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
            l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
            l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
            l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
            l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
            l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
            l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
            l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
            l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
            l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
            l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
            l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
            l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
            m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
            m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
            m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
            monus#(a,b) -> c_50(m1#(a,b,False(),False()))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/1,c_21/1,c_22/2,c_23/1,c_24/1,c_25/2,c_26/1
            ,c_27/1,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/1,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/1,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
             -->_1 l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False())):2
          
          2:W:l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
             -->_1 l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False())):12
          
          3:W:l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
             -->_1 l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True())):5
             -->_1 l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False())):4
          
          4:W:l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
             -->_1 l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y)):9
          
          5:W:l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
             -->_1 l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y)):6
          
          6:W:l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
             -->_2 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
             -->_1 l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y)):8
             -->_1 l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y)):7
          
          7:W:l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
             -->_1 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          8:W:l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
             -->_1 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          9:W:l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
             -->_2 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
             -->_1 l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0()))):11
             -->_1 l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0())):10
          
          10:W:l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
             -->_1 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          11:W:l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
             -->_1 gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False())):1
          
          12:W:l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
             -->_1 l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t)):13
          
          13:W:l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
             -->_1 l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False())):14
          
          14:W:l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
             -->_1 l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False())):15
          
          15:W:l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
             -->_1 l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t)):16
          
          16:W:l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
             -->_1 l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t)):17
          
          17:W:l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
             -->_1 l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y))):3
          
          18:W:m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
             -->_1 m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False())):19
          
          19:W:m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
             -->_1 m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x)):20
          
          20:W:m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
             -->_1 monus#(a,b) -> c_50(m1#(a,b,False(),False())):21
          
          21:W:monus#(a,b) -> c_50(m1#(a,b,False(),False()))
             -->_1 m1#(a,x,res,t) -> c_40(m2#(a,x,res,False())):18
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          1: gcd#(x,y) -> c_14(l1#(x,y,0(),False(),False(),False()))
          11: l15#(x,y,res,tmp,True(),t) -> c_27(gcd#(y,S(0())))
          9: l14#(x,y,res,tmp,mtmp,t) -> c_25(l15#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          4: l11#(x,y,res,tmp,mtmp,False()) -> c_20(l14#(x,y,res,tmp,mtmp,False()))
          3: l10#(x,y,res,tmp,mtmp,t) -> c_19(l11#(x,y,res,tmp,mtmp,<(x,y)))
          17: l8#(x,y,res,False(),mtmp,t) -> c_38(l10#(x,y,res,False(),mtmp,t))
          16: l7#(x,y,res,tmp,mtmp,t) -> c_36(l8#(x,y,res,equal0(x,y),mtmp,t))
          15: l5#(x,y,res,tmp,mtmp,False()) -> c_33(l7#(x,y,res,tmp,mtmp,False()))
          14: l4#(x',x,res,tmp,mtmp,t) -> c_32(l5#(x',x,res,tmp,mtmp,False()))
          13: l3#(x,y,res,tmp,mtmp,t) -> c_31(l4#(x,y,0(),tmp,mtmp,t))
          12: l2#(x,y,res,tmp,mtmp,False()) -> c_29(l3#(x,y,res,tmp,mtmp,False()))
          2: l1#(x,y,res,tmp,mtmp,t) -> c_18(l2#(x,y,res,tmp,mtmp,False()))
          10: l15#(x,y,res,tmp,False(),t) -> c_26(gcd#(y,0()))
          8: l13#(x,y,res,tmp,True(),t) -> c_24(gcd#(S(0()),y))
          6: l12#(x,y,res,tmp,mtmp,t) -> c_22(l13#(x,y,res,tmp,monus(x,y),t),monus#(x,y))
          5: l11#(x,y,res,tmp,mtmp,True()) -> c_21(l12#(x,y,res,tmp,mtmp,True()))
          7: l13#(x,y,res,tmp,False(),t) -> c_23(gcd#(0(),y))
          21: monus#(a,b) -> c_50(m1#(a,b,False(),False()))
          20: m4#(S(x'),S(x),res,t) -> c_48(monus#(x',x))
          19: m2#(a,b,res,False()) -> c_41(m4#(a,b,res,False()))
          18: m1#(a,x,res,t) -> c_40(m2#(a,x,res,False()))
** Step 11.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            equal0(a,b) -> e1(a,b,False(),False())
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2,<#/2,bool2Nat#/1
            ,e1#/4,e2#/4,e3#/4,e4#/4,e5#/4,e6#/4,e7#/4,e8#/4,equal0#/2,gcd#/2,help1#/1,l1#/6,l10#/6,l11#/6,l12#/6,l13#/6
            ,l14#/6,l15#/6,l16#/6,l2#/6,l3#/6,l4#/6,l5#/6,l6#/6,l7#/6,l8#/6,l9#/6,m1#/4,m2#/4,m3#/4,m4#/4,m5#/4
            ,monus#/2} / {0/0,False/0,S/1,True/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/1,c_21/1,c_22/2,c_23/1,c_24/1,c_25/2,c_26/1
            ,c_27/1,c_28/0,c_29/1,c_30/0,c_31/1,c_32/1,c_33/1,c_34/0,c_35/0,c_36/1,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1
            ,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0,c_48/1,c_49/0,c_50/1,c_51/0,c_52/0,c_53/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,bool2Nat#,e1#,e2#,e3#,e4#,e5#,e6#,e7#,e8#,equal0#,gcd#
            ,help1#,l1#,l10#,l11#,l12#,l13#,l14#,l15#,l16#,l2#,l3#,l4#,l5#,l6#,l7#,l8#,l9#,m1#,m2#,m3#,m4#,m5#
            ,monus#} and constructors {0,False,S,True}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))