MAYBE Time: 0.091334 TRS: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), pow(x, y) -> f(x, y, s 0())} DP: DP: { -#(s x, s y) -> -#(x, y), *#(x, s y) -> *#(x, y), odd# s s x -> odd# x, half# s s x -> half# x, f#(x, s y, z) -> *#(x, x), f#(x, s y, z) -> *#(x, z), f#(x, s y, z) -> if#(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), f#(x, s y, z) -> odd# s y, f#(x, s y, z) -> half# s y, f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> f#(*(x, x), half s y, z), pow#(x, y) -> f#(x, y, s 0())} TRS: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), pow(x, y) -> f(x, y, s 0())} UR: { *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), a(w, v) -> w, a(w, v) -> v} EDG: {(pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> f#(*(x, x), half s y, z)) (pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> f#(x, y, *(x, z))) (pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> half# s y) (pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> odd# s y) (pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> if#(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z))) (pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> *#(x, z)) (pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> *#(x, x)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (f#(x, s y, z) -> *#(x, x), *#(x, s y) -> *#(x, y)) (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> f#(*(x, x), half s y, z)) (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> f#(x, y, *(x, z))) (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> half# s y) (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> odd# s y) (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> if#(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z))) (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> *#(x, z)) (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> *#(x, x)) (half# s s x -> half# x, half# s s x -> half# x) (f#(x, s y, z) -> half# s y, half# s s x -> half# x) (f#(x, s y, z) -> odd# s y, odd# s s x -> odd# x) (odd# s s x -> odd# x, odd# s s x -> odd# x) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (f#(x, s y, z) -> *#(x, z), *#(x, s y) -> *#(x, y)) (f#(x, s y, z) -> f#(*(x, x), half s y, z), f#(x, s y, z) -> *#(x, x)) (f#(x, s y, z) -> f#(*(x, x), half s y, z), f#(x, s y, z) -> *#(x, z)) (f#(x, s y, z) -> f#(*(x, x), half s y, z), f#(x, s y, z) -> if#(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z))) (f#(x, s y, z) -> f#(*(x, x), half s y, z), f#(x, s y, z) -> odd# s y) (f#(x, s y, z) -> f#(*(x, x), half s y, z), f#(x, s y, z) -> half# s y) (f#(x, s y, z) -> f#(*(x, x), half s y, z), f#(x, s y, z) -> f#(x, y, *(x, z))) (f#(x, s y, z) -> f#(*(x, x), half s y, z), f#(x, s y, z) -> f#(*(x, x), half s y, z))} STATUS: arrows: 0.798611 SCCS (5): Scc: {-#(s x, s y) -> -#(x, y)} Scc: {f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> f#(*(x, x), half s y, z)} Scc: {half# s s x -> half# x} Scc: {odd# s s x -> odd# x} Scc: {*#(x, s y) -> *#(x, y)} SCC (1): Strict: {-#(s x, s y) -> -#(x, y)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), pow(x, y) -> f(x, y, s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [f](x0, x1, x2) = x0 + x1 + x2 + 1, [-](x0, x1) = x0 + 1, [*](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [pow](x0, x1) = 0, [s](x0) = x0 + 1, [odd](x0) = x0 + 1, [half](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [-#](x0, x1) = x0 + 1 Strict: -#(s x, s y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: pow(x, y) -> f(x, y, s 0()) 0 + 0x + 0y >= 3 + 1x + 1y f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)) 2 + 1x + 1y + 1z >= 3 + 0x + 1y + 0z f(x, 0(), z) -> z 2 + 1x + 1z >= 1z half s s x -> s half x 3 + 1x >= 2 + 1x half s 0() -> 0() 3 >= 1 half 0() -> 0() 2 >= 1 odd s s x -> odd x 3 + 1x >= 1 + 1x odd s 0() -> true() 3 >= 1 odd 0() -> false() 2 >= 1 if(false(), x, y) -> false() 2 + 0x + 0y >= 1 if(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> true() 2 + 0x + 0y >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x *(x, s y) -> +(*(x, y), x) 2 + 1x + 1y >= 2 + 2x + 1y *(x, 0()) -> 0() 2 + 1x >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x Qed SCC (2): Strict: {f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> f#(*(x, x), half s y, z)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), pow(x, y) -> f(x, y, s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [f](x0, x1, x2) = x0 + x1 + 1, [-](x0, x1) = x0 + 1, [*](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [pow](x0, x1) = 0, [s](x0) = x0 + 1, [odd](x0) = x0 + 1, [half](x0) = x0, [0] = 1, [true] = 1, [false] = 1, [f#](x0, x1, x2) = x0 Strict: f#(x, s y, z) -> f#(*(x, x), half s y, z) 1 + 0x + 1y + 0z >= 1 + 0x + 1y + 0z f#(x, s y, z) -> f#(x, y, *(x, z)) 1 + 0x + 1y + 0z >= 0 + 0x + 1y + 0z Weak: pow(x, y) -> f(x, y, s 0()) 0 + 0x + 0y >= 3 + 0x + 1y f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)) 2 + 0x + 1y + 1z >= 3 + 0x + 1y + 0z f(x, 0(), z) -> z 2 + 0x + 1z >= 1z half s s x -> s half x 2 + 1x >= 1 + 1x half s 0() -> 0() 2 >= 1 half 0() -> 0() 1 >= 1 odd s s x -> odd x 3 + 1x >= 1 + 1x odd s 0() -> true() 3 >= 1 odd 0() -> false() 2 >= 1 if(false(), x, y) -> false() 2 + 0x + 0y >= 1 if(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> true() 2 + 0x + 0y >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x *(x, s y) -> +(*(x, y), x) 2 + 1x + 1y >= 2 + 2x + 1y *(x, 0()) -> 0() 2 + 1x >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x SCCS (1): Scc: {f#(x, s y, z) -> f#(*(x, x), half s y, z)} SCC (1): Strict: {f#(x, s y, z) -> f#(*(x, x), half s y, z)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), pow(x, y) -> f(x, y, s 0())} Fail SCC (1): Strict: {half# s s x -> half# x} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), pow(x, y) -> f(x, y, s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [f](x0, x1, x2) = x0 + x1 + x2 + 1, [-](x0, x1) = x0 + 1, [*](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [pow](x0, x1) = 0, [s](x0) = x0 + 1, [odd](x0) = x0 + 1, [half](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [half#](x0) = x0 Strict: half# s s x -> half# x 2 + 1x >= 0 + 1x Weak: pow(x, y) -> f(x, y, s 0()) 0 + 0x + 0y >= 3 + 1x + 1y f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)) 2 + 1x + 1y + 1z >= 3 + 0x + 1y + 0z f(x, 0(), z) -> z 2 + 1x + 1z >= 1z half s s x -> s half x 3 + 1x >= 2 + 1x half s 0() -> 0() 3 >= 1 half 0() -> 0() 2 >= 1 odd s s x -> odd x 3 + 1x >= 1 + 1x odd s 0() -> true() 3 >= 1 odd 0() -> false() 2 >= 1 if(false(), x, y) -> false() 2 + 0x + 0y >= 1 if(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> true() 2 + 0x + 0y >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x *(x, s y) -> +(*(x, y), x) 2 + 1x + 1y >= 2 + 2x + 1y *(x, 0()) -> 0() 2 + 1x >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x Qed SCC (1): Strict: {odd# s s x -> odd# x} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), pow(x, y) -> f(x, y, s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [f](x0, x1, x2) = x0 + x1 + x2 + 1, [-](x0, x1) = x0 + 1, [*](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [pow](x0, x1) = 0, [s](x0) = x0 + 1, [odd](x0) = x0 + 1, [half](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [odd#](x0) = x0 Strict: odd# s s x -> odd# x 2 + 1x >= 0 + 1x Weak: pow(x, y) -> f(x, y, s 0()) 0 + 0x + 0y >= 3 + 1x + 1y f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)) 2 + 1x + 1y + 1z >= 3 + 0x + 1y + 0z f(x, 0(), z) -> z 2 + 1x + 1z >= 1z half s s x -> s half x 3 + 1x >= 2 + 1x half s 0() -> 0() 3 >= 1 half 0() -> 0() 2 >= 1 odd s s x -> odd x 3 + 1x >= 1 + 1x odd s 0() -> true() 3 >= 1 odd 0() -> false() 2 >= 1 if(false(), x, y) -> false() 2 + 0x + 0y >= 1 if(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> true() 2 + 0x + 0y >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x *(x, s y) -> +(*(x, y), x) 2 + 1x + 1y >= 2 + 2x + 1y *(x, 0()) -> 0() 2 + 1x >= 1 -(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), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), if(true(), x, y) -> x, if(true(), x, y) -> true(), if(false(), x, y) -> y, if(false(), x, y) -> false(), odd 0() -> false(), odd s 0() -> true(), odd s s x -> odd x, half 0() -> 0(), half s 0() -> 0(), half s s x -> s half x, f(x, 0(), z) -> z, f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)), pow(x, y) -> f(x, y, s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [f](x0, x1, x2) = x0 + x1 + x2 + 1, [-](x0, x1) = x0 + 1, [*](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [pow](x0, x1) = 0, [s](x0) = x0 + 1, [odd](x0) = x0 + 1, [half](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [*#](x0, x1) = x0 + 1 Strict: *#(x, s y) -> *#(x, y) 2 + 0x + 1y >= 1 + 0x + 1y Weak: pow(x, y) -> f(x, y, s 0()) 0 + 0x + 0y >= 3 + 1x + 1y f(x, s y, z) -> if(odd s y, f(x, y, *(x, z)), f(*(x, x), half s y, z)) 2 + 1x + 1y + 1z >= 3 + 0x + 1y + 0z f(x, 0(), z) -> z 2 + 1x + 1z >= 1z half s s x -> s half x 3 + 1x >= 2 + 1x half s 0() -> 0() 3 >= 1 half 0() -> 0() 2 >= 1 odd s s x -> odd x 3 + 1x >= 1 + 1x odd s 0() -> true() 3 >= 1 odd 0() -> false() 2 >= 1 if(false(), x, y) -> false() 2 + 0x + 0y >= 1 if(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> true() 2 + 0x + 0y >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x *(x, s y) -> +(*(x, y), x) 2 + 1x + 1y >= 2 + 2x + 1y *(x, 0()) -> 0() 2 + 1x >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x Qed