YES Time: 0.090726 TRS: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), gcd(0(), y) -> y, gcd(s x, 0()) -> s x, gcd(s x, s y) -> if_gcd(le(y, x), s x, s y), if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y), if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)} DP: DP: { le#(s x, s y) -> le#(x, y), minus#(s x, s y) -> minus#(x, y), gcd#(s x, s y) -> le#(y, x), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> minus#(x, y), if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), if_gcd#(false(), s x, s y) -> minus#(y, x), if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x)} TRS: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), gcd(0(), y) -> y, gcd(s x, 0()) -> s x, gcd(s x, s y) -> if_gcd(le(y, x), s x, s y), if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y), if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)} UR: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), a(z, w) -> z, a(z, w) -> w} EDG: {(if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(s x, s y) -> minus#(x, y)) (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y)) (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> le#(y, x)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> minus#(x, y)) (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y)) (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> minus#(y, x)) (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x)) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> le#(y, x)) (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y)) (gcd#(s x, s y) -> le#(y, x), le#(s x, s y) -> le#(x, y))} STATUS: arrows: 0.796875 SCCS (3): Scc: { gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x)} Scc: {minus#(s x, s y) -> minus#(x, y)} Scc: {le#(s x, s y) -> le#(x, y)} SCC (3): Strict: { gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), gcd(0(), y) -> y, gcd(s x, 0()) -> s x, gcd(s x, s y) -> if_gcd(le(y, x), s x, s y), if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y), if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_gcd](x0, x1, x2) = x0 + 1, [le](x0, x1) = 0, [minus](x0, x1) = x0, [gcd](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [if_gcd#](x0, x1, x2) = x0 + x1, [gcd#](x0, x1) = x0 + x1 + 1 Strict: if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x) 2 + 1y + 1x >= 2 + 1y + 1x if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y) 2 + 1y + 1x >= 2 + 1y + 1x gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y) 3 + 1y + 1x >= 2 + 1y + 1x Weak: if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x) 2 + 0y + 1x >= 1 + 1y + 0x if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y) 2 + 0y + 1x >= 1 + 0y + 1x gcd(s x, s y) -> if_gcd(le(y, x), s x, s y) 2 + 0y + 1x >= 2 + 0y + 1x gcd(s x, 0()) -> s x 2 + 1x >= 1 + 1x gcd(0(), y) -> y 2 + 0y >= 1y minus(s x, s y) -> minus(x, y) 1 + 0y + 1x >= 0 + 0y + 1x minus(x, 0()) -> x 0 + 1x >= 1x le(s x, s y) -> le(x, y) 0 + 0y + 0x >= 0 + 0y + 0x le(s x, 0()) -> false() 0 + 0x >= 0 le(0(), y) -> true() 0 + 0y >= 0 SCCS (0): SCC (1): Strict: {minus#(s x, s y) -> minus#(x, y)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), gcd(0(), y) -> y, gcd(s x, 0()) -> s x, gcd(s x, s y) -> if_gcd(le(y, x), s x, s y), if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y), if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_gcd](x0, x1, x2) = x0 + 1, [le](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + 1, [gcd](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [minus#](x0, x1) = x0 + 1 Strict: minus#(s x, s y) -> minus#(x, y) 2 + 0y + 1x >= 1 + 0y + 1x Weak: if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x) 2 + 0y + 1x >= 3 + 1y + 1x if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y) 2 + 0y + 1x >= 3 + 1y + 1x gcd(s x, s y) -> if_gcd(le(y, x), s x, s y) 3 + 1y + 1x >= 2 + 0y + 1x gcd(s x, 0()) -> s x 3 + 1x >= 1 + 1x gcd(0(), y) -> y 2 + 1y >= 1y minus(s x, s y) -> minus(x, y) 2 + 0y + 1x >= 1 + 0y + 1x minus(x, 0()) -> x 1 + 1x >= 1x le(s x, s y) -> le(x, y) 2 + 0y + 1x >= 1 + 0y + 1x le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 0 Qed SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), gcd(0(), y) -> y, gcd(s x, 0()) -> s x, gcd(s x, s y) -> if_gcd(le(y, x), s x, s y), if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y), if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_gcd](x0, x1, x2) = x0 + 1, [le](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + 1, [gcd](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [le#](x0, x1) = x0 + 1 Strict: le#(s x, s y) -> le#(x, y) 2 + 0y + 1x >= 1 + 0y + 1x Weak: if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x) 2 + 0y + 1x >= 3 + 1y + 1x if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y) 2 + 0y + 1x >= 3 + 1y + 1x gcd(s x, s y) -> if_gcd(le(y, x), s x, s y) 3 + 1y + 1x >= 2 + 0y + 1x gcd(s x, 0()) -> s x 3 + 1x >= 1 + 1x gcd(0(), y) -> y 2 + 1y >= 1y minus(s x, s y) -> minus(x, y) 2 + 0y + 1x >= 1 + 0y + 1x minus(x, 0()) -> x 1 + 1x >= 1x le(s x, s y) -> le(x, y) 2 + 0y + 1x >= 1 + 0y + 1x le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 0 Qed