MAYBE Time: 0.044591 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, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))} 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, y) -> -#(*(s x, s y), s *(s x, y)), f#(s x, y) -> *#(y, y), f#(s x, y) -> *#(s x, y), f#(s x, y) -> *#(s x, s y), f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y))} 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, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))} 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: {(-#(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, y) -> -#(*(s x, s y), s *(s x, y)), -#(s x, s y) -> -#(x, y)) (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y))) (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> *#(s x, s y)) (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> *#(s x, y)) (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> *#(y, y)) (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> -#(*(s x, s y), s *(s x, y))) (f#(s x, y) -> *#(s x, s y), *#(x, s y) -> +#(x, *(x, y))) (f#(s x, y) -> *#(s x, s y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y)) (f#(s x, y) -> *#(y, y), *#(x, s y) -> +#(x, *(x, y))) (f#(s x, y) -> *#(y, y), *#(x, s y) -> *#(x, y)) (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y)) (f#(s x, y) -> *#(s x, y), *#(x, s y) -> +#(x, *(x, y))) (f#(s x, y) -> *#(s x, y), *#(x, s y) -> *#(x, y))} STATUS: arrows: 0.790123 SCCS (4): Scc: {f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y))} Scc: {-#(s x, s y) -> -#(x, y)} Scc: {*#(x, s y) -> *#(x, y)} Scc: {+#(s x, y) -> +#(x, y)} SCC (1): Strict: {f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, 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, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))} Fail 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, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))} 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, [f](x0, x1) = x0, [s](x0) = x0 + 1, [0] = 1, [-#](x0, x1) = x0 Strict: -#(s x, s y) -> -#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y)) 1 + 1x + 0y >= 3 + 0x + 1y *(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 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, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))} 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, [f](x0, x1) = x0, [s](x0) = x0 + 1, [0] = 1, [*#](x0, x1) = x0 Strict: *#(x, s y) -> *#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y)) 1 + 1x + 0y >= 3 + 0x + 1y *(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 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, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))} 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, [f](x0, x1) = x0, [s](x0) = x0 + 1, [0] = 1, [+#](x0, x1) = x0 Strict: +#(s x, y) -> +#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y)) 1 + 1x + 0y >= 3 + 0x + 1y *(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