YES Time: 0.030576 TRS: { pred s X -> X, minus(X, s Y) -> pred minus(X, Y), minus(X, 0()) -> X, le(s X, s Y) -> le(X, Y), le(s X, 0()) -> false(), le(0(), Y) -> true(), gcd(s X, s Y) -> if(le(Y, X), s X, s Y), gcd(s X, 0()) -> s X, gcd(0(), Y) -> 0(), if(false(), s X, s Y) -> gcd(minus(Y, X), s X), if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)} DP: DP: { minus#(X, s Y) -> pred# minus(X, Y), minus#(X, s Y) -> minus#(X, Y), le#(s X, s Y) -> le#(X, Y), gcd#(s X, s Y) -> le#(Y, X), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> minus#(Y, X), if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), if#(true(), s X, s Y) -> minus#(X, Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)} TRS: { pred s X -> X, minus(X, s Y) -> pred minus(X, Y), minus(X, 0()) -> X, le(s X, s Y) -> le(X, Y), le(s X, 0()) -> false(), le(0(), Y) -> true(), gcd(s X, s Y) -> if(le(Y, X), s X, s Y), gcd(s X, 0()) -> s X, gcd(0(), Y) -> 0(), if(false(), s X, s Y) -> gcd(minus(Y, X), s X), if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)} EDG: {(le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y)) (gcd#(s X, s Y) -> le#(Y, X), le#(s X, s Y) -> le#(X, Y)) (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y)) (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> le#(Y, X)) (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> le#(Y, X)) (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y)) (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> minus#(Y, X)) (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X)) (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> minus#(X, Y)) (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)) (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> pred# minus(X, Y)) (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> minus#(X, Y)) (if#(true(), s X, s Y) -> minus#(X, Y), minus#(X, s Y) -> pred# minus(X, Y)) (if#(true(), s X, s Y) -> minus#(X, Y), minus#(X, s Y) -> minus#(X, Y)) (minus#(X, s Y) -> minus#(X, Y), minus#(X, s Y) -> pred# minus(X, Y)) (minus#(X, s Y) -> minus#(X, Y), minus#(X, s Y) -> minus#(X, Y))} SCCS (3): Scc: { gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)} Scc: {le#(s X, s Y) -> le#(X, Y)} Scc: {minus#(X, s Y) -> minus#(X, Y)} SCC (3): Strict: { gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)} Weak: { pred s X -> X, minus(X, s Y) -> pred minus(X, Y), minus(X, 0()) -> X, le(s X, s Y) -> le(X, Y), le(s X, 0()) -> false(), le(0(), Y) -> true(), gcd(s X, s Y) -> if(le(Y, X), s X, s Y), gcd(s X, 0()) -> s X, gcd(0(), Y) -> 0(), if(false(), s X, s Y) -> gcd(minus(Y, X), s X), if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [minus](x0, x1) = x0, [le](x0, x1) = 1, [gcd](x0, x1) = x0 + 1, [pred](x0) = x0, [s](x0) = x0 + 1, [0] = 1, [false] = 1, [true] = 0, [if#](x0, x1, x2) = x0 + x1 + x2, [gcd#](x0, x1) = x0 + x1 + 1 Strict: if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y) 2 + 1X + 1Y >= 2 + 1X + 1Y if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X) 3 + 1X + 1Y >= 2 + 1X + 1Y gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y) 3 + 1X + 1Y >= 3 + 1X + 1Y Weak: EDG: {(if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y)) (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y))} SCCS (1): Scc: { gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)} SCC (2): Strict: { gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)} Weak: { pred s X -> X, minus(X, s Y) -> pred minus(X, Y), minus(X, 0()) -> X, le(s X, s Y) -> le(X, Y), le(s X, 0()) -> false(), le(0(), Y) -> true(), gcd(s X, s Y) -> if(le(Y, X), s X, s Y), gcd(s X, 0()) -> s X, gcd(0(), Y) -> 0(), if(false(), s X, s Y) -> gcd(minus(Y, X), s X), if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [minus](x0, x1) = x0, [le](x0, x1) = 0, [gcd](x0, x1) = x0 + 1, [pred](x0) = x0, [s](x0) = x0 + 1, [0] = 1, [false] = 0, [true] = 0, [if#](x0, x1, x2) = x0, [gcd#](x0, x1) = x0 Strict: if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y) 1 + 1X + 0Y >= 0 + 1X + 0Y gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y) 1 + 1X + 0Y >= 1 + 1X + 0Y Weak: EDG: {} SCCS (0): Qed SCC (1): Strict: {le#(s X, s Y) -> le#(X, Y)} Weak: { pred s X -> X, minus(X, s Y) -> pred minus(X, Y), minus(X, 0()) -> X, le(s X, s Y) -> le(X, Y), le(s X, 0()) -> false(), le(0(), Y) -> true(), gcd(s X, s Y) -> if(le(Y, X), s X, s Y), gcd(s X, 0()) -> s X, gcd(0(), Y) -> 0(), if(false(), s X, s Y) -> gcd(minus(Y, X), s X), if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)} SPSC: Simple Projection: pi(le#) = 1 Strict: {} Qed SCC (1): Strict: {minus#(X, s Y) -> minus#(X, Y)} Weak: { pred s X -> X, minus(X, s Y) -> pred minus(X, Y), minus(X, 0()) -> X, le(s X, s Y) -> le(X, Y), le(s X, 0()) -> false(), le(0(), Y) -> true(), gcd(s X, s Y) -> if(le(Y, X), s X, s Y), gcd(s X, 0()) -> s X, gcd(0(), Y) -> 0(), if(false(), s X, s Y) -> gcd(minus(Y, X), s X), if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)} SPSC: Simple Projection: pi(minus#) = 1 Strict: {} Qed