MAYBE Time: 0.076915 TRS: { p s N -> N, +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), lt(N, M) -> gt(M, N), d(s N, s M) -> d(N, M), d(0(), N) -> N, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM), quot(N, NzM) -> u_11(is_NzNat NzM, N, NzM), quot(N, NzM) -> u_21(is_NzNat NzM, NzM, N), quot(NzM, NzM) -> u_01 is_NzNat NzM, u_1(True(), N, NzM) -> s quot(d(N, NzM), NzM), u_01 True() -> s 0(), u_21(True(), NzM, N) -> u_2 gt(NzM, N), u_2 True() -> 0(), gcd(NzN, NzM) -> u_31(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd(NzM, NzM) -> u_02(is_NzNat NzM, NzM), gcd(0(), N) -> 0(), u_02(True(), NzM) -> NzM, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM), u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)} DP: DP: { +#(s N, s M) -> +#(N, M), *#(s N, s M) -> +#(N, +(M, *(N, M))), *#(s N, s M) -> +#(M, *(N, M)), *#(s N, s M) -> *#(N, M), gt#(NzN, 0()) -> u_4# is_NzNat NzN, gt#(NzN, 0()) -> is_NzNat# NzN, gt#(s N, s M) -> gt#(N, M), lt#(N, M) -> gt#(M, N), d#(s N, s M) -> d#(N, M), u_11#(True(), N, NzM) -> gt#(N, NzM), u_11#(True(), N, NzM) -> u_1#(gt(N, NzM), N, NzM), quot#(N, NzM) -> is_NzNat# NzM, quot#(N, NzM) -> u_11#(is_NzNat NzM, N, NzM), quot#(N, NzM) -> u_21#(is_NzNat NzM, NzM, N), quot#(NzM, NzM) -> is_NzNat# NzM, quot#(NzM, NzM) -> u_01# is_NzNat NzM, u_1#(True(), N, NzM) -> d#(N, NzM), u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM), u_21#(True(), NzM, N) -> gt#(NzM, N), u_21#(True(), NzM, N) -> u_2# gt(NzM, N), gcd#(NzN, NzM) -> is_NzNat# NzN, gcd#(NzN, NzM) -> is_NzNat# NzM, gcd#(NzN, NzM) -> u_31#(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd#(NzM, NzM) -> is_NzNat# NzM, gcd#(NzM, NzM) -> u_02#(is_NzNat NzM, NzM), u_31#(True(), True(), NzN, NzM) -> gt#(NzN, NzM), u_31#(True(), True(), NzN, NzM) -> u_3#(gt(NzN, NzM), NzN, NzM), u_3#(True(), NzN, NzM) -> d#(NzN, NzM), u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM)} TRS: { p s N -> N, +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), lt(N, M) -> gt(M, N), d(s N, s M) -> d(N, M), d(0(), N) -> N, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM), quot(N, NzM) -> u_11(is_NzNat NzM, N, NzM), quot(N, NzM) -> u_21(is_NzNat NzM, NzM, N), quot(NzM, NzM) -> u_01 is_NzNat NzM, u_1(True(), N, NzM) -> s quot(d(N, NzM), NzM), u_01 True() -> s 0(), u_21(True(), NzM, N) -> u_2 gt(NzM, N), u_2 True() -> 0(), gcd(NzN, NzM) -> u_31(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd(NzM, NzM) -> u_02(is_NzNat NzM, NzM), gcd(0(), N) -> 0(), u_02(True(), NzM) -> NzM, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM), u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)} UR: { +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), d(s N, s M) -> d(N, M), d(0(), N) -> N, a(x, y) -> x, a(x, y) -> y} EDG: {(u_11#(True(), N, NzM) -> gt#(N, NzM), gt#(s N, s M) -> gt#(N, M)) (u_11#(True(), N, NzM) -> gt#(N, NzM), gt#(NzN, 0()) -> is_NzNat# NzN) (u_11#(True(), N, NzM) -> gt#(N, NzM), gt#(NzN, 0()) -> u_4# is_NzNat NzN) (u_31#(True(), True(), NzN, NzM) -> gt#(NzN, NzM), gt#(s N, s M) -> gt#(N, M)) (u_31#(True(), True(), NzN, NzM) -> gt#(NzN, NzM), gt#(NzN, 0()) -> is_NzNat# NzN) (u_31#(True(), True(), NzN, NzM) -> gt#(NzN, NzM), gt#(NzN, 0()) -> u_4# is_NzNat NzN) (*#(s N, s M) -> +#(N, +(M, *(N, M))), +#(s N, s M) -> +#(N, M)) (*#(s N, s M) -> *#(N, M), *#(s N, s M) -> *#(N, M)) (*#(s N, s M) -> *#(N, M), *#(s N, s M) -> +#(M, *(N, M))) (*#(s N, s M) -> *#(N, M), *#(s N, s M) -> +#(N, +(M, *(N, M)))) (d#(s N, s M) -> d#(N, M), d#(s N, s M) -> d#(N, M)) (quot#(N, NzM) -> u_21#(is_NzNat NzM, NzM, N), u_21#(True(), NzM, N) -> u_2# gt(NzM, N)) (quot#(N, NzM) -> u_21#(is_NzNat NzM, NzM, N), u_21#(True(), NzM, N) -> gt#(NzM, N)) (quot#(N, NzM) -> u_11#(is_NzNat NzM, N, NzM), u_11#(True(), N, NzM) -> u_1#(gt(N, NzM), N, NzM)) (quot#(N, NzM) -> u_11#(is_NzNat NzM, N, NzM), u_11#(True(), N, NzM) -> gt#(N, NzM)) (lt#(N, M) -> gt#(M, N), gt#(s N, s M) -> gt#(N, M)) (lt#(N, M) -> gt#(M, N), gt#(NzN, 0()) -> is_NzNat# NzN) (lt#(N, M) -> gt#(M, N), gt#(NzN, 0()) -> u_4# is_NzNat NzN) (u_21#(True(), NzM, N) -> gt#(NzM, N), gt#(s N, s M) -> gt#(N, M)) (u_21#(True(), NzM, N) -> gt#(NzM, N), gt#(NzN, 0()) -> is_NzNat# NzN) (u_21#(True(), NzM, N) -> gt#(NzM, N), gt#(NzN, 0()) -> u_4# is_NzNat NzN) (u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM), gcd#(NzM, NzM) -> u_02#(is_NzNat NzM, NzM)) (u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM), gcd#(NzM, NzM) -> is_NzNat# NzM) (u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM), gcd#(NzN, NzM) -> u_31#(is_NzNat NzN, is_NzNat NzM, NzN, NzM)) (u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM), gcd#(NzN, NzM) -> is_NzNat# NzM) (u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM), gcd#(NzN, NzM) -> is_NzNat# NzN) (u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM), quot#(N, NzM) -> is_NzNat# NzM) (u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM), quot#(N, NzM) -> u_11#(is_NzNat NzM, N, NzM)) (u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM), quot#(N, NzM) -> u_21#(is_NzNat NzM, NzM, N)) (u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM), quot#(NzM, NzM) -> is_NzNat# NzM) (u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM), quot#(NzM, NzM) -> u_01# is_NzNat NzM) (u_31#(True(), True(), NzN, NzM) -> u_3#(gt(NzN, NzM), NzN, NzM), u_3#(True(), NzN, NzM) -> d#(NzN, NzM)) (u_31#(True(), True(), NzN, NzM) -> u_3#(gt(NzN, NzM), NzN, NzM), u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM)) (u_11#(True(), N, NzM) -> u_1#(gt(N, NzM), N, NzM), u_1#(True(), N, NzM) -> d#(N, NzM)) (u_11#(True(), N, NzM) -> u_1#(gt(N, NzM), N, NzM), u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM)) (*#(s N, s M) -> +#(M, *(N, M)), +#(s N, s M) -> +#(N, M)) (gt#(s N, s M) -> gt#(N, M), gt#(NzN, 0()) -> u_4# is_NzNat NzN) (gt#(s N, s M) -> gt#(N, M), gt#(NzN, 0()) -> is_NzNat# NzN) (gt#(s N, s M) -> gt#(N, M), gt#(s N, s M) -> gt#(N, M)) (+#(s N, s M) -> +#(N, M), +#(s N, s M) -> +#(N, M)) (u_3#(True(), NzN, NzM) -> d#(NzN, NzM), d#(s N, s M) -> d#(N, M)) (u_1#(True(), N, NzM) -> d#(N, NzM), d#(s N, s M) -> d#(N, M)) (gcd#(NzN, NzM) -> u_31#(is_NzNat NzN, is_NzNat NzM, NzN, NzM), u_31#(True(), True(), NzN, NzM) -> gt#(NzN, NzM)) (gcd#(NzN, NzM) -> u_31#(is_NzNat NzN, is_NzNat NzM, NzN, NzM), u_31#(True(), True(), NzN, NzM) -> u_3#(gt(NzN, NzM), NzN, NzM))} STATUS: arrows: 0.947681 SCCS (6): Scc: {u_11#(True(), N, NzM) -> u_1#(gt(N, NzM), N, NzM), quot#(N, NzM) -> u_11#(is_NzNat NzM, N, NzM), u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM)} Scc: {*#(s N, s M) -> *#(N, M)} Scc: {+#(s N, s M) -> +#(N, M)} Scc: { gcd#(NzN, NzM) -> u_31#(is_NzNat NzN, is_NzNat NzM, NzN, NzM), u_31#(True(), True(), NzN, NzM) -> u_3#(gt(NzN, NzM), NzN, NzM), u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM)} Scc: {d#(s N, s M) -> d#(N, M)} Scc: {gt#(s N, s M) -> gt#(N, M)} SCC (3): Strict: {u_11#(True(), N, NzM) -> u_1#(gt(N, NzM), N, NzM), quot#(N, NzM) -> u_11#(is_NzNat NzM, N, NzM), u_1#(True(), N, NzM) -> quot#(d(N, NzM), NzM)} Weak: { p s N -> N, +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), lt(N, M) -> gt(M, N), d(s N, s M) -> d(N, M), d(0(), N) -> N, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM), quot(N, NzM) -> u_11(is_NzNat NzM, N, NzM), quot(N, NzM) -> u_21(is_NzNat NzM, NzM, N), quot(NzM, NzM) -> u_01 is_NzNat NzM, u_1(True(), N, NzM) -> s quot(d(N, NzM), NzM), u_01 True() -> s 0(), u_21(True(), NzM, N) -> u_2 gt(NzM, N), u_2 True() -> 0(), gcd(NzN, NzM) -> u_31(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd(NzM, NzM) -> u_02(is_NzNat NzM, NzM), gcd(0(), N) -> 0(), u_02(True(), NzM) -> NzM, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM), u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)} Open SCC (1): Strict: {*#(s N, s M) -> *#(N, M)} Weak: { p s N -> N, +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), lt(N, M) -> gt(M, N), d(s N, s M) -> d(N, M), d(0(), N) -> N, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM), quot(N, NzM) -> u_11(is_NzNat NzM, N, NzM), quot(N, NzM) -> u_21(is_NzNat NzM, NzM, N), quot(NzM, NzM) -> u_01 is_NzNat NzM, u_1(True(), N, NzM) -> s quot(d(N, NzM), NzM), u_01 True() -> s 0(), u_21(True(), NzM, N) -> u_2 gt(NzM, N), u_2 True() -> 0(), gcd(NzN, NzM) -> u_31(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd(NzM, NzM) -> u_02(is_NzNat NzM, NzM), gcd(0(), N) -> 0(), u_02(True(), NzM) -> NzM, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM), u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)} Open SCC (1): Strict: {+#(s N, s M) -> +#(N, M)} Weak: { p s N -> N, +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), lt(N, M) -> gt(M, N), d(s N, s M) -> d(N, M), d(0(), N) -> N, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM), quot(N, NzM) -> u_11(is_NzNat NzM, N, NzM), quot(N, NzM) -> u_21(is_NzNat NzM, NzM, N), quot(NzM, NzM) -> u_01 is_NzNat NzM, u_1(True(), N, NzM) -> s quot(d(N, NzM), NzM), u_01 True() -> s 0(), u_21(True(), NzM, N) -> u_2 gt(NzM, N), u_2 True() -> 0(), gcd(NzN, NzM) -> u_31(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd(NzM, NzM) -> u_02(is_NzNat NzM, NzM), gcd(0(), N) -> 0(), u_02(True(), NzM) -> NzM, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM), u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)} Open SCC (3): Strict: { gcd#(NzN, NzM) -> u_31#(is_NzNat NzN, is_NzNat NzM, NzN, NzM), u_31#(True(), True(), NzN, NzM) -> u_3#(gt(NzN, NzM), NzN, NzM), u_3#(True(), NzN, NzM) -> gcd#(d(NzN, NzM), NzM)} Weak: { p s N -> N, +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), lt(N, M) -> gt(M, N), d(s N, s M) -> d(N, M), d(0(), N) -> N, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM), quot(N, NzM) -> u_11(is_NzNat NzM, N, NzM), quot(N, NzM) -> u_21(is_NzNat NzM, NzM, N), quot(NzM, NzM) -> u_01 is_NzNat NzM, u_1(True(), N, NzM) -> s quot(d(N, NzM), NzM), u_01 True() -> s 0(), u_21(True(), NzM, N) -> u_2 gt(NzM, N), u_2 True() -> 0(), gcd(NzN, NzM) -> u_31(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd(NzM, NzM) -> u_02(is_NzNat NzM, NzM), gcd(0(), N) -> 0(), u_02(True(), NzM) -> NzM, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM), u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)} Open SCC (1): Strict: {d#(s N, s M) -> d#(N, M)} Weak: { p s N -> N, +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), lt(N, M) -> gt(M, N), d(s N, s M) -> d(N, M), d(0(), N) -> N, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM), quot(N, NzM) -> u_11(is_NzNat NzM, N, NzM), quot(N, NzM) -> u_21(is_NzNat NzM, NzM, N), quot(NzM, NzM) -> u_01 is_NzNat NzM, u_1(True(), N, NzM) -> s quot(d(N, NzM), NzM), u_01 True() -> s 0(), u_21(True(), NzM, N) -> u_2 gt(NzM, N), u_2 True() -> 0(), gcd(NzN, NzM) -> u_31(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd(NzM, NzM) -> u_02(is_NzNat NzM, NzM), gcd(0(), N) -> 0(), u_02(True(), NzM) -> NzM, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM), u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)} Open SCC (1): Strict: {gt#(s N, s M) -> gt#(N, M)} Weak: { p s N -> N, +(N, 0()) -> N, +(s N, s M) -> s s +(N, M), *(N, 0()) -> 0(), *(s N, s M) -> s +(N, +(M, *(N, M))), gt(NzN, 0()) -> u_4 is_NzNat NzN, gt(s N, s M) -> gt(N, M), gt(0(), M) -> False(), u_4 True() -> True(), is_NzNat s N -> True(), is_NzNat 0() -> False(), lt(N, M) -> gt(M, N), d(s N, s M) -> d(N, M), d(0(), N) -> N, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM), quot(N, NzM) -> u_11(is_NzNat NzM, N, NzM), quot(N, NzM) -> u_21(is_NzNat NzM, NzM, N), quot(NzM, NzM) -> u_01 is_NzNat NzM, u_1(True(), N, NzM) -> s quot(d(N, NzM), NzM), u_01 True() -> s 0(), u_21(True(), NzM, N) -> u_2 gt(NzM, N), u_2 True() -> 0(), gcd(NzN, NzM) -> u_31(is_NzNat NzN, is_NzNat NzM, NzN, NzM), gcd(NzM, NzM) -> u_02(is_NzNat NzM, NzM), gcd(0(), N) -> 0(), u_02(True(), NzM) -> NzM, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM), u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)} Open