tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c23()
            A() -> c24()
            GCD(z0,z1) -> c1(GCD2(z0,z1,0()))
            GCD2(z0,z1,z2) -> c2(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z0,0()))
            GCD2(z0,z1,z2) -> c3(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z1,0()))
            GCD2(z0,z1,z2) -> c4(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z0,z1))
            GCD2(z0,z1,z2) -> c5(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z1,z0))
            GCD2(z0,z1,z2) -> c6(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),INC(z2))
            IF1(false(),z0,z1,z2,z3,z4,z5) -> c8(IF2(z0,z1,z2,z3,z4,z5))
            IF1(true(),z0,z1,z2,z3,z4,z5) -> c7()
            IF2(false(),z0,z1,z2,z3,z4) -> c10(IF3(z0,z1,z2,z3,z4))
            IF2(true(),z0,z1,z2,z3,z4) -> c9()
            IF3(false(),z0,z1,z2,z3) -> c11(GCD2(minus(z1,z2),z2,z3),MINUS(z1,z2))
            IF3(true(),z0,z1,z2,z3) -> c12(IF4(z0,z1,z2,z3))
            IF4(false(),z0,z1,z2) -> c13(GCD2(z0,minus(z1,z0),z2),MINUS(z1,z0))
            IF4(true(),z0,z1,z2) -> c14()
            INC(0()) -> c15()
            INC(s(z0)) -> c16(INC(z0))
            LE(0(),z0) -> c18()
            LE(s(z0),0()) -> c17()
            LE(s(z0),s(z1)) -> c19(LE(z0,z1))
            MINUS(z0,0()) -> c20()
            MINUS(0(),z0) -> c21()
            MINUS(s(z0),s(z1)) -> c22(MINUS(z0,z1))
        - Weak TRS:
            a() -> b()
            a() -> c()
            gcd(z0,z1) -> gcd2(z0,z1,0())
            gcd2(z0,z1,z2) -> if1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2))
            if1(false(),z0,z1,z2,z3,z4,z5) -> if2(z0,z1,z2,z3,z4,z5)
            if1(true(),z0,z1,z2,z3,z4,z5) -> pair(result(z4),neededIterations(z5))
            if2(false(),z0,z1,z2,z3,z4) -> if3(z0,z1,z2,z3,z4)
            if2(true(),z0,z1,z2,z3,z4) -> pair(result(z2),neededIterations(z4))
            if3(false(),z0,z1,z2,z3) -> gcd2(minus(z1,z2),z2,z3)
            if3(true(),z0,z1,z2,z3) -> if4(z0,z1,z2,z3)
            if4(false(),z0,z1,z2) -> gcd2(z0,minus(z1,z0),z2)
            if4(true(),z0,z1,z2) -> pair(result(z0),neededIterations(z2))
            inc(0()) -> 0()
            inc(s(z0)) -> s(inc(z0))
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            minus(z0,0()) -> z0
            minus(0(),z0) -> 0()
            minus(s(z0),s(z1)) -> minus(z0,z1)
        - Signature:
            {A/0,GCD/2,GCD2/3,IF1/7,IF2/6,IF3/5,IF4/4,INC/1,LE/2,MINUS/2,a/0,gcd/2,gcd2/3,if1/7,if2/6,if3/5,if4/4,inc/1
            ,le/2,minus/2} / {0/0,b/0,c/0,c1/1,c10/1,c11/2,c12/1,c13/2,c14/0,c15/0,c16/1,c17/0,c18/0,c19/1,c2/2,c20/0
            ,c21/0,c22/1,c23/0,c24/0,c3/2,c4/2,c5/2,c6/2,c7/0,c8/1,c9/0,false/0,neededIterations/1,pair/2,result/1,s/1
            ,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,GCD,GCD2,IF1,IF2,IF3,IF4,INC,LE,MINUS,a,gcd,gcd2,if1
            ,if2,if3,if4,inc,le,minus} and constructors {0,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22
            ,c23,c24,c3,c4,c5,c6,c7,c8,c9,false,neededIterations,pair,result,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c23()
            A() -> c24()
            GCD(z0,z1) -> c1(GCD2(z0,z1,0()))
            GCD2(z0,z1,z2) -> c2(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z0,0()))
            GCD2(z0,z1,z2) -> c3(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z1,0()))
            GCD2(z0,z1,z2) -> c4(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z0,z1))
            GCD2(z0,z1,z2) -> c5(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z1,z0))
            GCD2(z0,z1,z2) -> c6(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),INC(z2))
            IF1(false(),z0,z1,z2,z3,z4,z5) -> c8(IF2(z0,z1,z2,z3,z4,z5))
            IF1(true(),z0,z1,z2,z3,z4,z5) -> c7()
            IF2(false(),z0,z1,z2,z3,z4) -> c10(IF3(z0,z1,z2,z3,z4))
            IF2(true(),z0,z1,z2,z3,z4) -> c9()
            IF3(false(),z0,z1,z2,z3) -> c11(GCD2(minus(z1,z2),z2,z3),MINUS(z1,z2))
            IF3(true(),z0,z1,z2,z3) -> c12(IF4(z0,z1,z2,z3))
            IF4(false(),z0,z1,z2) -> c13(GCD2(z0,minus(z1,z0),z2),MINUS(z1,z0))
            IF4(true(),z0,z1,z2) -> c14()
            INC(0()) -> c15()
            INC(s(z0)) -> c16(INC(z0))
            LE(0(),z0) -> c18()
            LE(s(z0),0()) -> c17()
            LE(s(z0),s(z1)) -> c19(LE(z0,z1))
            MINUS(z0,0()) -> c20()
            MINUS(0(),z0) -> c21()
            MINUS(s(z0),s(z1)) -> c22(MINUS(z0,z1))
        - Weak TRS:
            a() -> b()
            a() -> c()
            gcd(z0,z1) -> gcd2(z0,z1,0())
            gcd2(z0,z1,z2) -> if1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2))
            if1(false(),z0,z1,z2,z3,z4,z5) -> if2(z0,z1,z2,z3,z4,z5)
            if1(true(),z0,z1,z2,z3,z4,z5) -> pair(result(z4),neededIterations(z5))
            if2(false(),z0,z1,z2,z3,z4) -> if3(z0,z1,z2,z3,z4)
            if2(true(),z0,z1,z2,z3,z4) -> pair(result(z2),neededIterations(z4))
            if3(false(),z0,z1,z2,z3) -> gcd2(minus(z1,z2),z2,z3)
            if3(true(),z0,z1,z2,z3) -> if4(z0,z1,z2,z3)
            if4(false(),z0,z1,z2) -> gcd2(z0,minus(z1,z0),z2)
            if4(true(),z0,z1,z2) -> pair(result(z0),neededIterations(z2))
            inc(0()) -> 0()
            inc(s(z0)) -> s(inc(z0))
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            minus(z0,0()) -> z0
            minus(0(),z0) -> 0()
            minus(s(z0),s(z1)) -> minus(z0,z1)
        - Signature:
            {A/0,GCD/2,GCD2/3,IF1/7,IF2/6,IF3/5,IF4/4,INC/1,LE/2,MINUS/2,a/0,gcd/2,gcd2/3,if1/7,if2/6,if3/5,if4/4,inc/1
            ,le/2,minus/2} / {0/0,b/0,c/0,c1/1,c10/1,c11/2,c12/1,c13/2,c14/0,c15/0,c16/1,c17/0,c18/0,c19/1,c2/2,c20/0
            ,c21/0,c22/1,c23/0,c24/0,c3/2,c4/2,c5/2,c6/2,c7/0,c8/1,c9/0,false/0,neededIterations/1,pair/2,result/1,s/1
            ,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,GCD,GCD2,IF1,IF2,IF3,IF4,INC,LE,MINUS,a,gcd,gcd2,if1
            ,if2,if3,if4,inc,le,minus} and constructors {0,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22
            ,c23,c24,c3,c4,c5,c6,c7,c8,c9,false,neededIterations,pair,result,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c23()
            A() -> c24()
            GCD(z0,z1) -> c1(GCD2(z0,z1,0()))
            GCD2(z0,z1,z2) -> c2(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z0,0()))
            GCD2(z0,z1,z2) -> c3(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z1,0()))
            GCD2(z0,z1,z2) -> c4(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z0,z1))
            GCD2(z0,z1,z2) -> c5(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),LE(z1,z0))
            GCD2(z0,z1,z2) -> c6(IF1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2)),INC(z2))
            IF1(false(),z0,z1,z2,z3,z4,z5) -> c8(IF2(z0,z1,z2,z3,z4,z5))
            IF1(true(),z0,z1,z2,z3,z4,z5) -> c7()
            IF2(false(),z0,z1,z2,z3,z4) -> c10(IF3(z0,z1,z2,z3,z4))
            IF2(true(),z0,z1,z2,z3,z4) -> c9()
            IF3(false(),z0,z1,z2,z3) -> c11(GCD2(minus(z1,z2),z2,z3),MINUS(z1,z2))
            IF3(true(),z0,z1,z2,z3) -> c12(IF4(z0,z1,z2,z3))
            IF4(false(),z0,z1,z2) -> c13(GCD2(z0,minus(z1,z0),z2),MINUS(z1,z0))
            IF4(true(),z0,z1,z2) -> c14()
            INC(0()) -> c15()
            INC(s(z0)) -> c16(INC(z0))
            LE(0(),z0) -> c18()
            LE(s(z0),0()) -> c17()
            LE(s(z0),s(z1)) -> c19(LE(z0,z1))
            MINUS(z0,0()) -> c20()
            MINUS(0(),z0) -> c21()
            MINUS(s(z0),s(z1)) -> c22(MINUS(z0,z1))
        - Weak TRS:
            a() -> b()
            a() -> c()
            gcd(z0,z1) -> gcd2(z0,z1,0())
            gcd2(z0,z1,z2) -> if1(le(z0,0()),le(z1,0()),le(z0,z1),le(z1,z0),z0,z1,inc(z2))
            if1(false(),z0,z1,z2,z3,z4,z5) -> if2(z0,z1,z2,z3,z4,z5)
            if1(true(),z0,z1,z2,z3,z4,z5) -> pair(result(z4),neededIterations(z5))
            if2(false(),z0,z1,z2,z3,z4) -> if3(z0,z1,z2,z3,z4)
            if2(true(),z0,z1,z2,z3,z4) -> pair(result(z2),neededIterations(z4))
            if3(false(),z0,z1,z2,z3) -> gcd2(minus(z1,z2),z2,z3)
            if3(true(),z0,z1,z2,z3) -> if4(z0,z1,z2,z3)
            if4(false(),z0,z1,z2) -> gcd2(z0,minus(z1,z0),z2)
            if4(true(),z0,z1,z2) -> pair(result(z0),neededIterations(z2))
            inc(0()) -> 0()
            inc(s(z0)) -> s(inc(z0))
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            minus(z0,0()) -> z0
            minus(0(),z0) -> 0()
            minus(s(z0),s(z1)) -> minus(z0,z1)
        - Signature:
            {A/0,GCD/2,GCD2/3,IF1/7,IF2/6,IF3/5,IF4/4,INC/1,LE/2,MINUS/2,a/0,gcd/2,gcd2/3,if1/7,if2/6,if3/5,if4/4,inc/1
            ,le/2,minus/2} / {0/0,b/0,c/0,c1/1,c10/1,c11/2,c12/1,c13/2,c14/0,c15/0,c16/1,c17/0,c18/0,c19/1,c2/2,c20/0
            ,c21/0,c22/1,c23/0,c24/0,c3/2,c4/2,c5/2,c6/2,c7/0,c8/1,c9/0,false/0,neededIterations/1,pair/2,result/1,s/1
            ,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,GCD,GCD2,IF1,IF2,IF3,IF4,INC,LE,MINUS,a,gcd,gcd2,if1
            ,if2,if3,if4,inc,le,minus} and constructors {0,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22
            ,c23,c24,c3,c4,c5,c6,c7,c8,c9,false,neededIterations,pair,result,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          INC(x){x -> s(x)} =
            INC(s(x)) ->^+ c16(INC(x))
              = C[INC(x) = INC(x){}]

WORST_CASE(Omega(n^1),?)