MAYBE Time: 0.044812 TRS: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), +(0(), y) -> y, +(s x, y) -> s +(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(x, *(x, y)), f s x -> f -(*(s s 0(), s x), s s x)} DP: DP: {-#(s x, s y) -> -#(x, y), +#(s x, y) -> +#(x, y), *#(x, s y) -> +#(x, *(x, y)), *#(x, s y) -> *#(x, y), f# s x -> -#(*(s s 0(), s x), s s x), f# s x -> *#(s s 0(), s x), f# s x -> f# -(*(s s 0(), s x), s s x)} TRS: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), +(0(), y) -> y, +(s x, y) -> s +(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(x, *(x, y)), f s x -> f -(*(s s 0(), s x), s s x)} UR: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), +(0(), y) -> y, +(s x, y) -> s +(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(x, *(x, y)), a(z, w) -> z, a(z, w) -> w} EDG: {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(x, *(x, y))) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> -#(*(s s 0(), s x), s s x)) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> *#(s s 0(), s x)) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> f# -(*(s s 0(), s x), s s x)) (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y)) (f# s x -> *#(s s 0(), s x), *#(x, s y) -> +#(x, *(x, y))) (f# s x -> *#(s s 0(), s x), *#(x, s y) -> *#(x, y)) (f# s x -> -#(*(s s 0(), s x), s s x), -#(s x, s y) -> -#(x, y))} EDG: {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(x, *(x, y))) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> -#(*(s s 0(), s x), s s x)) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> *#(s s 0(), s x)) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> f# -(*(s s 0(), s x), s s x)) (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y)) (f# s x -> *#(s s 0(), s x), *#(x, s y) -> +#(x, *(x, y))) (f# s x -> *#(s s 0(), s x), *#(x, s y) -> *#(x, y)) (f# s x -> -#(*(s s 0(), s x), s s x), -#(s x, s y) -> -#(x, y))} EDG: {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(x, *(x, y))) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> -#(*(s s 0(), s x), s s x)) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> *#(s s 0(), s x)) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> f# -(*(s s 0(), s x), s s x)) (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y)) (f# s x -> *#(s s 0(), s x), *#(x, s y) -> +#(x, *(x, y))) (f# s x -> *#(s s 0(), s x), *#(x, s y) -> *#(x, y)) (f# s x -> -#(*(s s 0(), s x), s s x), -#(s x, s y) -> -#(x, y))} EDG: {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(x, *(x, y))) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> -#(*(s s 0(), s x), s s x)) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> *#(s s 0(), s x)) (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> f# -(*(s s 0(), s x), s s x)) (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y)) (f# s x -> *#(s s 0(), s x), *#(x, s y) -> +#(x, *(x, y))) (f# s x -> *#(s s 0(), s x), *#(x, s y) -> *#(x, y)) (f# s x -> -#(*(s s 0(), s x), s s x), -#(s x, s y) -> -#(x, y))} STATUS: arrows: 0.775510 SCCS (4): Scc: {f# s x -> f# -(*(s s 0(), s x), s s x)} Scc: {*#(x, s y) -> *#(x, y)} Scc: {+#(s x, y) -> +#(x, y)} Scc: {-#(s x, s y) -> -#(x, y)} SCC (1): Strict: {f# s x -> f# -(*(s s 0(), s x), s s x)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), +(0(), y) -> y, +(s x, y) -> s +(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(x, *(x, y)), f s x -> f -(*(s s 0(), s x), s s x)} Fail SCC (1): Strict: {*#(x, s y) -> *#(x, y)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), +(0(), y) -> y, +(s x, y) -> s +(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(x, *(x, y)), f s x -> f -(*(s s 0(), s x), s s x)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [-](x0, x1) = x0 + x1, [+](x0, x1) = 0, [*](x0, x1) = 0, [s](x0) = x0 + 1, [f](x0) = x0 + 1, [0] = 0, [*#](x0, x1) = x0 Strict: *#(x, s y) -> *#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: f s x -> f -(*(s s 0(), s x), s s x) 2 + 1x >= 3 + 1x *(x, s y) -> +(x, *(x, y)) 0 + 0x + 0y >= 0 + 0x + 0y *(x, 0()) -> 0() 0 + 0x >= 0 +(s x, y) -> s +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(0(), y) -> y 0 + 0y >= 1y -(s x, s y) -> -(x, y) 2 + 1x + 1y >= 0 + 1x + 1y -(x, 0()) -> x 0 + 1x >= 1x Qed SCC (1): Strict: {+#(s x, y) -> +#(x, y)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), +(0(), y) -> y, +(s x, y) -> s +(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(x, *(x, y)), f s x -> f -(*(s s 0(), s x), s s x)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [-](x0, x1) = x0 + x1, [+](x0, x1) = 0, [*](x0, x1) = 0, [s](x0) = x0 + 1, [f](x0) = x0 + 1, [0] = 0, [+#](x0, x1) = x0 Strict: +#(s x, y) -> +#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: f s x -> f -(*(s s 0(), s x), s s x) 2 + 1x >= 3 + 1x *(x, s y) -> +(x, *(x, y)) 0 + 0x + 0y >= 0 + 0x + 0y *(x, 0()) -> 0() 0 + 0x >= 0 +(s x, y) -> s +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(0(), y) -> y 0 + 0y >= 1y -(s x, s y) -> -(x, y) 2 + 1x + 1y >= 0 + 1x + 1y -(x, 0()) -> x 0 + 1x >= 1x Qed SCC (1): Strict: {-#(s x, s y) -> -#(x, y)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), +(0(), y) -> y, +(s x, y) -> s +(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(x, *(x, y)), f s x -> f -(*(s s 0(), s x), s s x)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [-](x0, x1) = x0 + 1, [+](x0, x1) = x0 + 1, [*](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [f](x0) = x0, [0] = 1, [-#](x0, x1) = x0 Strict: -#(s x, s y) -> -#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: f s x -> f -(*(s s 0(), s x), s s x) 1 + 1x >= 3 + 1x *(x, s y) -> +(x, *(x, y)) 2 + 0x + 1y >= 1 + 1x + 0y *(x, 0()) -> 0() 2 + 0x >= 1 +(s x, y) -> s +(x, y) 2 + 1x + 0y >= 2 + 1x + 0y +(0(), y) -> y 2 + 0y >= 1y -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x Qed