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