*** 1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: 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))) Weak DP Rules: Weak TRS Rules: Signature: {gcd/2} / {-/2,0/0,2,if/3,s/1} Obligation: Innermost basic terms: {gcd}/{-,0,<,if,s} Applied Processor: DependencyPairs {dpKind_ = DT} Proof: 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. *** 1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP 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))) Strict TRS Rules: Weak DP Rules: Weak TRS Rules: 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 basic terms: {gcd#}/{-,0,<,if,s} Applied Processor: UsableRules Proof: 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))) *** 1.1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP 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))) Strict TRS Rules: Weak DP Rules: Weak TRS Rules: Signature: {gcd/2,gcd#/2} / {-/2,0/0,2,if/3,s/1,c_1/0,c_2/0,c_3/2} Obligation: Innermost basic terms: {gcd#}/{-,0,<,if,s} Applied Processor: Trivial Proof: 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. *** 1.1.1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: Signature: {gcd/2,gcd#/2} / {-/2,0/0,2,if/3,s/1,c_1/0,c_2/0,c_3/2} Obligation: Innermost basic terms: {gcd#}/{-,0,<,if,s} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).