* Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: gcd(x,0()) -> x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2} / {-/2,0/0,2,if/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {gcd} and constructors {-,0,<,if,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: gcd(x,0()) -> x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2} / {-/2,0/0,2,if/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {gcd} and constructors {-,0,<,if,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs gcd#(x,0()) -> c_1() gcd#(0(),y) -> c_2() gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) Weak DPs and mark the set of starting terms. * Step 3: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: gcd#(x,0()) -> c_1() gcd#(0(),y) -> c_2() gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) - Weak TRS: gcd(x,0()) -> x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2,gcd#/2} / {-/2,0/0,2,if/3,s/1,c_1/0,c_2/0,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {gcd#} and constructors {-,0,<,if,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: gcd#(x,0()) -> c_1() gcd#(0(),y) -> c_2() gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) * Step 4: Trivial WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: gcd#(x,0()) -> c_1() gcd#(0(),y) -> c_2() gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) - Signature: {gcd/2,gcd#/2} / {-/2,0/0,2,if/3,s/1,c_1/0,c_2/0,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {gcd#} and constructors {-,0,<,if,s} + Applied Processor: Trivial + Details: Consider the dependency graph 1:S:gcd#(x,0()) -> c_1() 2:S:gcd#(0(),y) -> c_2() 3:S:gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) The dependency graph contains no loops, we remove all dependency pairs. * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {gcd/2,gcd#/2} / {-/2,0/0,2,if/3,s/1,c_1/0,c_2/0,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {gcd#} and constructors {-,0,<,if,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))