MAYBE Time: 0.009169 TRS: { gcd2(x, y, i) -> if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), gcd(x, y) -> gcd2(x, y, 0()), if1(true(), b1, b2, b3, x, y, i) -> pair(result y, neededIterations i), if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), inc 0() -> 0(), inc s i -> s inc i, if2(true(), b2, b3, x, y, i) -> pair(result x, neededIterations i), if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i), if3(true(), b3, x, y, i) -> if4(b3, x, y, i), if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), if4(true(), x, y, i) -> pair(result x, neededIterations i), if4(false(), x, y, i) -> gcd2(x, minus(y, x), i), a() -> b(), a() -> c()} DP: DP: { gcd2#(x, y, i) -> if1#(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), gcd2#(x, y, i) -> le#(x, y), gcd2#(x, y, i) -> le#(x, 0()), gcd2#(x, y, i) -> le#(y, x), gcd2#(x, y, i) -> le#(y, 0()), gcd2#(x, y, i) -> inc# i, gcd#(x, y) -> gcd2#(x, y, 0()), if1#(false(), b1, b2, b3, x, y, i) -> if2#(b1, b2, b3, x, y, i), le#(s x, s y) -> le#(x, y), inc# s i -> inc# i, if2#(false(), b2, b3, x, y, i) -> if3#(b2, b3, x, y, i), if3#(true(), b3, x, y, i) -> if4#(b3, x, y, i), if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), if3#(false(), b3, x, y, i) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y), if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i), if4#(false(), x, y, i) -> minus#(y, x)} TRS: { gcd2(x, y, i) -> if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), gcd(x, y) -> gcd2(x, y, 0()), if1(true(), b1, b2, b3, x, y, i) -> pair(result y, neededIterations i), if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), inc 0() -> 0(), inc s i -> s inc i, if2(true(), b2, b3, x, y, i) -> pair(result x, neededIterations i), if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i), if3(true(), b3, x, y, i) -> if4(b3, x, y, i), if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), if4(true(), x, y, i) -> pair(result x, neededIterations i), if4(false(), x, y, i) -> gcd2(x, minus(y, x), i), a() -> b(), a() -> c()} EDG: {(gcd2#(x, y, i) -> if1#(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), if1#(false(), b1, b2, b3, x, y, i) -> if2#(b1, b2, b3, x, y, i)) (if2#(false(), b2, b3, x, y, i) -> if3#(b2, b3, x, y, i), if3#(false(), b3, x, y, i) -> minus#(x, y)) (if2#(false(), b2, b3, x, y, i) -> if3#(b2, b3, x, y, i), if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i)) (if2#(false(), b2, b3, x, y, i) -> if3#(b2, b3, x, y, i), if3#(true(), b3, x, y, i) -> if4#(b3, x, y, i)) (gcd2#(x, y, i) -> inc# i, inc# s i -> inc# i) (if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), gcd2#(x, y, i) -> inc# i) (if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), gcd2#(x, y, i) -> le#(y, 0())) (if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), gcd2#(x, y, i) -> le#(y, x)) (if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), gcd2#(x, y, i) -> le#(x, 0())) (if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), gcd2#(x, y, i) -> le#(x, y)) (if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), gcd2#(x, y, i) -> if1#(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i)) (if4#(false(), x, y, i) -> minus#(y, x), minus#(s x, s y) -> minus#(x, y)) (gcd2#(x, y, i) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (if3#(false(), b3, x, y, i) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (gcd#(x, y) -> gcd2#(x, y, 0()), gcd2#(x, y, i) -> if1#(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i)) (gcd#(x, y) -> gcd2#(x, y, 0()), gcd2#(x, y, i) -> le#(x, y)) (gcd#(x, y) -> gcd2#(x, y, 0()), gcd2#(x, y, i) -> le#(x, 0())) (gcd#(x, y) -> gcd2#(x, y, 0()), gcd2#(x, y, i) -> le#(y, x)) (gcd#(x, y) -> gcd2#(x, y, 0()), gcd2#(x, y, i) -> le#(y, 0())) (gcd#(x, y) -> gcd2#(x, y, 0()), gcd2#(x, y, i) -> inc# i) (gcd2#(x, y, i) -> le#(y, x), le#(s x, s y) -> le#(x, y)) (inc# s i -> inc# i, inc# s i -> inc# i) (if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i), gcd2#(x, y, i) -> if1#(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i)) (if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i), gcd2#(x, y, i) -> le#(x, y)) (if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i), gcd2#(x, y, i) -> le#(x, 0())) (if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i), gcd2#(x, y, i) -> le#(y, x)) (if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i), gcd2#(x, y, i) -> le#(y, 0())) (if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i), gcd2#(x, y, i) -> inc# i) (if1#(false(), b1, b2, b3, x, y, i) -> if2#(b1, b2, b3, x, y, i), if2#(false(), b2, b3, x, y, i) -> if3#(b2, b3, x, y, i)) (if3#(true(), b3, x, y, i) -> if4#(b3, x, y, i), if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i)) (if3#(true(), b3, x, y, i) -> if4#(b3, x, y, i), if4#(false(), x, y, i) -> minus#(y, x))} STATUS: arrows: 0.885813 SCCS (4): Scc: { gcd2#(x, y, i) -> if1#(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), if1#(false(), b1, b2, b3, x, y, i) -> if2#(b1, b2, b3, x, y, i), if2#(false(), b2, b3, x, y, i) -> if3#(b2, b3, x, y, i), if3#(true(), b3, x, y, i) -> if4#(b3, x, y, i), if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i)} Scc: {minus#(s x, s y) -> minus#(x, y)} Scc: {inc# s i -> inc# i} Scc: {le#(s x, s y) -> le#(x, y)} SCC (6): Strict: { gcd2#(x, y, i) -> if1#(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), if1#(false(), b1, b2, b3, x, y, i) -> if2#(b1, b2, b3, x, y, i), if2#(false(), b2, b3, x, y, i) -> if3#(b2, b3, x, y, i), if3#(true(), b3, x, y, i) -> if4#(b3, x, y, i), if3#(false(), b3, x, y, i) -> gcd2#(minus(x, y), y, i), if4#(false(), x, y, i) -> gcd2#(x, minus(y, x), i)} Weak: { gcd2(x, y, i) -> if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), gcd(x, y) -> gcd2(x, y, 0()), if1(true(), b1, b2, b3, x, y, i) -> pair(result y, neededIterations i), if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), inc 0() -> 0(), inc s i -> s inc i, if2(true(), b2, b3, x, y, i) -> pair(result x, neededIterations i), if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i), if3(true(), b3, x, y, i) -> if4(b3, x, y, i), if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), if4(true(), x, y, i) -> pair(result x, neededIterations i), if4(false(), x, y, i) -> gcd2(x, minus(y, x), i), a() -> b(), a() -> c()} Open SCC (1): Strict: {minus#(s x, s y) -> minus#(x, y)} Weak: { gcd2(x, y, i) -> if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), gcd(x, y) -> gcd2(x, y, 0()), if1(true(), b1, b2, b3, x, y, i) -> pair(result y, neededIterations i), if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), inc 0() -> 0(), inc s i -> s inc i, if2(true(), b2, b3, x, y, i) -> pair(result x, neededIterations i), if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i), if3(true(), b3, x, y, i) -> if4(b3, x, y, i), if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), if4(true(), x, y, i) -> pair(result x, neededIterations i), if4(false(), x, y, i) -> gcd2(x, minus(y, x), i), a() -> b(), a() -> c()} Open SCC (1): Strict: {inc# s i -> inc# i} Weak: { gcd2(x, y, i) -> if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), gcd(x, y) -> gcd2(x, y, 0()), if1(true(), b1, b2, b3, x, y, i) -> pair(result y, neededIterations i), if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), inc 0() -> 0(), inc s i -> s inc i, if2(true(), b2, b3, x, y, i) -> pair(result x, neededIterations i), if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i), if3(true(), b3, x, y, i) -> if4(b3, x, y, i), if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), if4(true(), x, y, i) -> pair(result x, neededIterations i), if4(false(), x, y, i) -> gcd2(x, minus(y, x), i), a() -> b(), a() -> c()} Open SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { gcd2(x, y, i) -> if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc i), gcd(x, y) -> gcd2(x, y, 0()), if1(true(), b1, b2, b3, x, y, i) -> pair(result y, neededIterations i), if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), inc 0() -> 0(), inc s i -> s inc i, if2(true(), b2, b3, x, y, i) -> pair(result x, neededIterations i), if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i), if3(true(), b3, x, y, i) -> if4(b3, x, y, i), if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), if4(true(), x, y, i) -> pair(result x, neededIterations i), if4(false(), x, y, i) -> gcd2(x, minus(y, x), i), a() -> b(), a() -> c()} Open