YES Time: 0.229545 TRS: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} DP: DP: { +#(0 x, 0 y) -> 0# +(x, y), +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, j y) -> 0# +(x, y), +#(1 x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y), +#(j x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()), opp# 0 x -> 0# opp x, opp# 0 x -> opp# x, opp# 1 x -> opp# x, opp# j x -> opp# x, -#(x, y) -> +#(x, opp y), -#(x, y) -> opp# y, *#(0 x, y) -> 0# *(x, y), *#(0 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y), *#(1 x, y) -> +#(0 *(x, y), y), *#(1 x, y) -> *#(x, y), *#(j x, y) -> 0# *(x, y), *#(j x, y) -> -#(0 *(x, y), y), *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} TRS: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} UR: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z)), a(w, v) -> w, a(w, v) -> v} EDG: { (+#(j x, j y) -> +#(+(x, y), j #()), +#(j x, j y) -> +#(+(x, y), j #())) (+#(j x, j y) -> +#(+(x, y), j #()), +#(j x, j y) -> +#(x, y)) (+#(j x, j y) -> +#(+(x, y), j #()), +#(1 x, j y) -> +#(x, y)) (+#(j x, j y) -> +#(+(x, y), j #()), +#(1 x, j y) -> 0# +(x, y)) (+#(j x, j y) -> +#(+(x, y), j #()), +#(+(x, y), z) -> +#(y, z)) (+#(j x, j y) -> +#(+(x, y), j #()), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(j x, j y) -> +#(+(x, y), j #()), +#(0 x, j y) -> +#(x, y)) (-#(x, y) -> opp# y, opp# j x -> opp# x) (-#(x, y) -> opp# y, opp# 1 x -> opp# x) (-#(x, y) -> opp# y, opp# 0 x -> opp# x) (-#(x, y) -> opp# y, opp# 0 x -> 0# opp x) (*#(j x, y) -> -#(0 *(x, y), y), -#(x, y) -> opp# y) (*#(j x, y) -> -#(0 *(x, y), y), -#(x, y) -> +#(x, opp y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j x, y) -> -#(0 *(x, y), y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j x, y) -> 0# *(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1 x, y) -> 0# *(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0 x, y) -> 0# *(x, y)) (opp# 1 x -> opp# x, opp# j x -> opp# x) (opp# 1 x -> opp# x, opp# 1 x -> opp# x) (opp# 1 x -> opp# x, opp# 0 x -> opp# x) (opp# 1 x -> opp# x, opp# 0 x -> 0# opp x) (+#(0 x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(0 x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(0 x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(0 x, j y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(0 x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(0 x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(0 x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0 x, j y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(0 x, j y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(1 x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(j x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(j x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(j x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(j x, 0 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(j x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(j x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(j x, j y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(j x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(j x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(j x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(j x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(j x, j y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(j x, j y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(j x, y) -> -#(0 *(x, y), y)) (*#(1 x, y) -> *#(x, y), *#(j x, y) -> 0# *(x, y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y)) (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y)) (-#(x, y) -> +#(x, opp y), +#(j x, j y) -> +#(+(x, y), j #())) (-#(x, y) -> +#(x, opp y), +#(j x, j y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(j x, 1 y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(j x, 1 y) -> 0# +(x, y)) (-#(x, y) -> +#(x, opp y), +#(j x, 0 y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(1 x, j y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(1 x, j y) -> 0# +(x, y)) (-#(x, y) -> +#(x, opp y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (-#(x, y) -> +#(x, opp y), +#(1 x, 1 y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(1 x, 0 y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(+(x, y), z) -> +#(y, z)) (-#(x, y) -> +#(x, opp y), +#(+(x, y), z) -> +#(x, +(y, z))) (-#(x, y) -> +#(x, opp y), +#(0 x, j y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(0 x, 1 y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(0 x, 0 y) -> +#(x, y)) (-#(x, y) -> +#(x, opp y), +#(0 x, 0 y) -> 0# +(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> -#(0 *(x, y), y)) (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> 0# *(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> 0# *(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(0 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(0 x, y) -> 0# *(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0 x, 0 y) -> 0# +(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0 x, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0 x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0 x, j y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(1 x, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(+(x, y), z) -> +#(y, z), +#(1 x, j y) -> 0# +(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(1 x, j y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(j x, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(j x, 1 y) -> 0# +(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(j x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(j x, j y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(j x, j y) -> +#(+(x, y), j #())) (*#(j x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y)) (*#(j x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y)) (*#(j x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(j x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(j x, y) -> 0# *(x, y)) (*#(j x, y) -> *#(x, y), *#(j x, y) -> -#(0 *(x, y), y)) (*#(j x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y)) (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(j x, y) -> 0# *(x, y)) (*#(0 x, y) -> *#(x, y), *#(j x, y) -> -#(0 *(x, y), y)) (*#(0 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (+#(j x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(j x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(j x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(j x, 1 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(j x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(1 x, j y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, j y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, j y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(1 x, j y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(1 x, j y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(1 x, j y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(1 x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())) (opp# j x -> opp# x, opp# 0 x -> 0# opp x) (opp# j x -> opp# x, opp# 0 x -> opp# x) (opp# j x -> opp# x, opp# 1 x -> opp# x) (opp# j x -> opp# x, opp# j x -> opp# x) (opp# 0 x -> opp# x, opp# 0 x -> 0# opp x) (opp# 0 x -> opp# x, opp# 0 x -> opp# x) (opp# 0 x -> opp# x, opp# 1 x -> opp# x) (opp# 0 x -> opp# x, opp# j x -> opp# x) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 0 y) -> 0# +(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, j y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, j y) -> 0# +(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, j y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, 1 y) -> 0# +(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, j y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, j y) -> +#(+(x, y), j #())) (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 0 y) -> 0# +(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 0 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 1 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, j y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(j x, 1 y) -> 0# +(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(j x, 1 y) -> +#(x, y)) } STATUS: arrows: 0.728516 SCCS (3): Scc: { *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Scc: {opp# 0 x -> opp# x, opp# 1 x -> opp# x, opp# j x -> opp# x} Scc: { +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())} SCC (5): Strict: { *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = 0, [-](x0, x1) = 0, [*](x0, x1) = x0 + x1 + 1, [0](x0) = x0, [1](x0) = x0, [j](x0) = x0, [opp](x0) = 0, [#] = 0, [*#](x0, x1) = x0 Strict: *#(*(x, y), z) -> *#(y, z) 1 + 1x + 1y + 0z >= 0 + 1y + 0z *#(*(x, y), z) -> *#(x, *(y, z)) 1 + 1x + 1y + 0z >= 0 + 1x + 0y + 0z *#(j x, y) -> *#(x, y) 0 + 1x + 0y >= 0 + 1x + 0y *#(1 x, y) -> *#(x, y) 0 + 1x + 0y >= 0 + 1x + 0y *#(0 x, y) -> *#(x, y) 0 + 1x + 0y >= 0 + 1x + 0y Weak: *(*(x, y), z) -> *(x, *(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z *(j x, y) -> -(0 *(x, y), y) 1 + 1x + 1y >= 0 + 0x + 0y *(1 x, y) -> +(0 *(x, y), y) 1 + 1x + 1y >= 0 + 0x + 0y *(0 x, y) -> 0 *(x, y) 1 + 1x + 1y >= 1 + 1x + 1y *(#(), x) -> #() 1 + 1x >= 0 -(x, y) -> +(x, opp y) 0 + 0x + 0y >= 0 + 0x + 0y opp j x -> 1 opp x 0 + 0x >= 0 + 0x opp 1 x -> j opp x 0 + 0x >= 0 + 0x opp 0 x -> 0 opp x 0 + 0x >= 0 + 0x opp #() -> #() 0 >= 0 +(j x, j y) -> 1 +(+(x, y), j #()) 0 + 0x + 0y >= 0 + 0x + 0y +(j x, 1 y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(j x, 0 y) -> j +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(1 x, j y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 0 + 0x + 0y >= 0 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(+(x, y), z) -> +(x, +(y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z +(0 x, j y) -> j +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(#(), x) -> x 0 + 0x >= 1x +(x, #()) -> x 0 + 0x >= 1x 0 #() -> #() 0 >= 0 SCCS (1): Scc: {*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)} SCC (3): Strict: {*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = 0, [-](x0, x1) = x0 + x1, [*](x0, x1) = x0, [0](x0) = x0, [1](x0) = x0, [j](x0) = x0 + 1, [opp](x0) = 0, [#] = 0, [*#](x0, x1) = x0 Strict: *#(j x, y) -> *#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y *#(1 x, y) -> *#(x, y) 0 + 1x + 0y >= 0 + 1x + 0y *#(0 x, y) -> *#(x, y) 0 + 1x + 0y >= 0 + 1x + 0y Weak: *(*(x, y), z) -> *(x, *(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z *(j x, y) -> -(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 2y *(1 x, y) -> +(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 0y *(0 x, y) -> 0 *(x, y) 0 + 0x + 1y >= 0 + 0x + 1y *(#(), x) -> #() 0 + 1x >= 0 -(x, y) -> +(x, opp y) 0 + 1x + 1y >= 0 + 0x + 0y opp j x -> 1 opp x 0 + 0x >= 0 + 0x opp 1 x -> j opp x 0 + 0x >= 1 + 0x opp 0 x -> 0 opp x 0 + 0x >= 0 + 0x opp #() -> #() 0 >= 0 +(j x, j y) -> 1 +(+(x, y), j #()) 0 + 0x + 0y >= 0 + 0x + 0y +(j x, 1 y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(j x, 0 y) -> j +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(1 x, j y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 0 + 0x + 0y >= 1 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(+(x, y), z) -> +(x, +(y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z +(0 x, j y) -> j +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(#(), x) -> x 0 + 0x >= 1x +(x, #()) -> x 0 + 0x >= 1x 0 #() -> #() 0 >= 0 SCCS (1): Scc: {*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)} SCC (2): Strict: {*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0, [-](x0, x1) = x0 + x1, [*](x0, x1) = x0, [0](x0) = x0, [1](x0) = x0 + 1, [j](x0) = 0, [opp](x0) = 1, [#] = 0, [*#](x0, x1) = x0 Strict: *#(1 x, y) -> *#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y *#(0 x, y) -> *#(x, y) 0 + 1x + 0y >= 0 + 1x + 0y Weak: *(*(x, y), z) -> *(x, *(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z *(j x, y) -> -(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 2y *(1 x, y) -> +(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 1y *(0 x, y) -> 0 *(x, y) 0 + 0x + 1y >= 0 + 0x + 1y *(#(), x) -> #() 0 + 1x >= 0 -(x, y) -> +(x, opp y) 0 + 1x + 1y >= 1 + 0x + 0y opp j x -> 1 opp x 1 + 0x >= 2 + 0x opp 1 x -> j opp x 1 + 0x >= 0 + 0x opp 0 x -> 0 opp x 1 + 0x >= 1 + 0x opp #() -> #() 1 >= 0 +(j x, j y) -> 1 +(+(x, y), j #()) 0 + 0x + 0y >= 1 + 0x + 0y +(j x, 1 y) -> 0 +(x, y) 1 + 0x + 1y >= 0 + 0x + 1y +(j x, 0 y) -> j +(x, y) 0 + 0x + 1y >= 0 + 0x + 0y +(1 x, j y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 1y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 1 + 0x + 1y >= 0 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 0 + 0x + 1y >= 1 + 0x + 1y +(+(x, y), z) -> +(x, +(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z +(0 x, j y) -> j +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 1 + 0x + 1y >= 1 + 0x + 1y +(0 x, 0 y) -> 0 +(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +(#(), x) -> x 0 + 1x >= 1x +(x, #()) -> x 0 + 0x >= 1x 0 #() -> #() 0 >= 0 SCCS (1): Scc: {*#(0 x, y) -> *#(x, y)} SCC (1): Strict: {*#(0 x, y) -> *#(x, y)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1, [*](x0, x1) = x0 + x1 + 1, [0](x0) = x0 + 1, [1](x0) = 0, [j](x0) = 0, [opp](x0) = x0 + 1, [#] = 1, [*#](x0, x1) = x0 Strict: *#(0 x, y) -> *#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: *(*(x, y), z) -> *(x, *(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z *(j x, y) -> -(0 *(x, y), y) 1 + 0x + 1y >= 2 + 1x + 2y *(1 x, y) -> +(0 *(x, y), y) 1 + 0x + 1y >= 3 + 1x + 2y *(0 x, y) -> 0 *(x, y) 2 + 1x + 1y >= 2 + 1x + 1y *(#(), x) -> #() 2 + 1x >= 1 -(x, y) -> +(x, opp y) 0 + 1x + 1y >= 2 + 1x + 1y opp j x -> 1 opp x 1 + 0x >= 0 + 0x opp 1 x -> j opp x 1 + 0x >= 0 + 0x opp 0 x -> 0 opp x 2 + 1x >= 2 + 1x opp #() -> #() 2 >= 1 +(j x, j y) -> 1 +(+(x, y), j #()) 1 + 0x + 0y >= 0 + 0x + 0y +(j x, 1 y) -> 0 +(x, y) 1 + 0x + 0y >= 2 + 1x + 1y +(j x, 0 y) -> j +(x, y) 2 + 0x + 1y >= 0 + 0x + 0y +(1 x, j y) -> 0 +(x, y) 1 + 0x + 0y >= 2 + 1x + 1y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 1 + 0x + 0y >= 0 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 2 + 0x + 1y >= 0 + 0x + 0y +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(0 x, j y) -> j +(x, y) 2 + 1x + 0y >= 0 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 2 + 1x + 0y >= 0 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(#(), x) -> x 2 + 1x >= 1x +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 Qed SCC (3): Strict: {opp# 0 x -> opp# x, opp# 1 x -> opp# x, opp# j x -> opp# x} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = 0, [-](x0, x1) = x0 + x1, [*](x0, x1) = x0, [0](x0) = x0, [1](x0) = x0, [j](x0) = x0 + 1, [opp](x0) = 0, [#] = 0, [opp#](x0) = x0 Strict: opp# j x -> opp# x 1 + 1x >= 0 + 1x opp# 1 x -> opp# x 0 + 1x >= 0 + 1x opp# 0 x -> opp# x 0 + 1x >= 0 + 1x Weak: *(*(x, y), z) -> *(x, *(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z *(j x, y) -> -(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 2y *(1 x, y) -> +(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 0y *(0 x, y) -> 0 *(x, y) 0 + 0x + 1y >= 0 + 0x + 1y *(#(), x) -> #() 0 + 1x >= 0 -(x, y) -> +(x, opp y) 0 + 1x + 1y >= 0 + 0x + 0y opp j x -> 1 opp x 0 + 0x >= 0 + 0x opp 1 x -> j opp x 0 + 0x >= 1 + 0x opp 0 x -> 0 opp x 0 + 0x >= 0 + 0x opp #() -> #() 0 >= 0 +(j x, j y) -> 1 +(+(x, y), j #()) 0 + 0x + 0y >= 0 + 0x + 0y +(j x, 1 y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(j x, 0 y) -> j +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(1 x, j y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 0 + 0x + 0y >= 1 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(+(x, y), z) -> +(x, +(y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z +(0 x, j y) -> j +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(#(), x) -> x 0 + 0x >= 1x +(x, #()) -> x 0 + 0x >= 1x 0 #() -> #() 0 >= 0 SCCS (1): Scc: {opp# 0 x -> opp# x, opp# 1 x -> opp# x} SCC (2): Strict: {opp# 0 x -> opp# x, opp# 1 x -> opp# x} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0, [-](x0, x1) = x0 + x1, [*](x0, x1) = x0, [0](x0) = x0, [1](x0) = x0 + 1, [j](x0) = 0, [opp](x0) = 1, [#] = 0, [opp#](x0) = x0 Strict: opp# 1 x -> opp# x 1 + 1x >= 0 + 1x opp# 0 x -> opp# x 0 + 1x >= 0 + 1x Weak: *(*(x, y), z) -> *(x, *(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z *(j x, y) -> -(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 2y *(1 x, y) -> +(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 1y *(0 x, y) -> 0 *(x, y) 0 + 0x + 1y >= 0 + 0x + 1y *(#(), x) -> #() 0 + 1x >= 0 -(x, y) -> +(x, opp y) 0 + 1x + 1y >= 1 + 0x + 0y opp j x -> 1 opp x 1 + 0x >= 2 + 0x opp 1 x -> j opp x 1 + 0x >= 0 + 0x opp 0 x -> 0 opp x 1 + 0x >= 1 + 0x opp #() -> #() 1 >= 0 +(j x, j y) -> 1 +(+(x, y), j #()) 0 + 0x + 0y >= 1 + 0x + 0y +(j x, 1 y) -> 0 +(x, y) 1 + 0x + 1y >= 0 + 0x + 1y +(j x, 0 y) -> j +(x, y) 0 + 0x + 1y >= 0 + 0x + 0y +(1 x, j y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 1y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 1 + 0x + 1y >= 0 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 0 + 0x + 1y >= 1 + 0x + 1y +(+(x, y), z) -> +(x, +(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z +(0 x, j y) -> j +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 1 + 0x + 1y >= 1 + 0x + 1y +(0 x, 0 y) -> 0 +(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +(#(), x) -> x 0 + 1x >= 1x +(x, #()) -> x 0 + 0x >= 1x 0 #() -> #() 0 >= 0 SCCS (1): Scc: {opp# 0 x -> opp# x} SCC (1): Strict: {opp# 0 x -> opp# x} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1, [*](x0, x1) = x0 + x1 + 1, [0](x0) = x0 + 1, [1](x0) = 0, [j](x0) = 0, [opp](x0) = x0 + 1, [#] = 1, [opp#](x0) = x0 Strict: opp# 0 x -> opp# x 1 + 1x >= 0 + 1x Weak: *(*(x, y), z) -> *(x, *(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z *(j x, y) -> -(0 *(x, y), y) 1 + 0x + 1y >= 2 + 1x + 2y *(1 x, y) -> +(0 *(x, y), y) 1 + 0x + 1y >= 3 + 1x + 2y *(0 x, y) -> 0 *(x, y) 2 + 1x + 1y >= 2 + 1x + 1y *(#(), x) -> #() 2 + 1x >= 1 -(x, y) -> +(x, opp y) 0 + 1x + 1y >= 2 + 1x + 1y opp j x -> 1 opp x 1 + 0x >= 0 + 0x opp 1 x -> j opp x 1 + 0x >= 0 + 0x opp 0 x -> 0 opp x 2 + 1x >= 2 + 1x opp #() -> #() 2 >= 1 +(j x, j y) -> 1 +(+(x, y), j #()) 1 + 0x + 0y >= 0 + 0x + 0y +(j x, 1 y) -> 0 +(x, y) 1 + 0x + 0y >= 2 + 1x + 1y +(j x, 0 y) -> j +(x, y) 2 + 0x + 1y >= 0 + 0x + 0y +(1 x, j y) -> 0 +(x, y) 1 + 0x + 0y >= 2 + 1x + 1y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 1 + 0x + 0y >= 0 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 2 + 0x + 1y >= 0 + 0x + 0y +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(0 x, j y) -> j +(x, y) 2 + 1x + 0y >= 0 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 2 + 1x + 0y >= 0 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(#(), x) -> x 2 + 1x >= 1x +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 Qed SCC (13): Strict: { +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #())} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} 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, [0](x0) = x0 + 1, [1](x0) = x0 + 1, [j](x0) = x0 + 1, [opp](x0) = 1, [#] = 0, [+#](x0, x1) = x0 + x1 + 1 Strict: +#(j x, j y) -> +#(+(x, y), j #()) 3 + 1x + 1y >= 2 + 1x + 1y +#(j x, j y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(j x, 1 y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(j x, 0 y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(1 x, j y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(1 x, 1 y) -> +#(+(x, y), 1 #()) 3 + 1x + 1y >= 2 + 1x + 1y +#(1 x, 1 y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(1 x, 0 y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(+(x, y), z) -> +#(y, z) 1 + 1x + 1y + 1z >= 1 + 1y + 1z +#(+(x, y), z) -> +#(x, +(y, z)) 1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z +#(0 x, j y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(0 x, 1 y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(0 x, 0 y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y Weak: *(*(x, y), z) -> *(x, *(y, z)) 2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z *(j x, y) -> -(0 *(x, y), y) 2 + 1x + 0y >= 0 + 0x + 0y *(1 x, y) -> +(0 *(x, y), y) 2 + 1x + 0y >= 2 + 1x + 1y *(0 x, y) -> 0 *(x, y) 2 + 1x + 0y >= 2 + 1x + 0y *(#(), x) -> #() 1 + 0x >= 0 -(x, y) -> +(x, opp y) 0 + 0x + 0y >= 1 + 1x + 0y opp j x -> 1 opp x 1 + 0x >= 2 + 0x opp 1 x -> j opp x 1 + 0x >= 2 + 0x opp 0 x -> 0 opp x 1 + 0x >= 2 + 0x opp #() -> #() 1 >= 0 +(j x, j y) -> 1 +(+(x, y), j #()) 2 + 1x + 1y >= 2 + 1x + 1y +(j x, 1 y) -> 0 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(j x, 0 y) -> j +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(1 x, j y) -> 0 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 2 + 1x + 1y >= 2 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(+(x, y), z) -> +(x, +(y, z)) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z +(0 x, j y) -> j +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(0 x, 1 y) -> 1 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(0 x, 0 y) -> 0 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(#(), x) -> x 0 + 1x >= 1x +(x, #()) -> x 0 + 1x >= 1x 0 #() -> #() 1 >= 0 SCCS (1): Scc: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} SCC (2): Strict: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(0 x, j y) -> j +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> j +(+(x, y), 1 #()), +(1 x, j y) -> 0 +(x, y), +(j x, 0 y) -> j +(x, y), +(j x, 1 y) -> 0 +(x, y), +(j x, j y) -> 1 +(+(x, y), j #()), opp #() -> #(), opp 0 x -> 0 opp x, opp 1 x -> j opp x, opp j x -> 1 opp x, -(x, y) -> +(x, opp y), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(j x, y) -> -(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = 0, [*](x0, x1) = x0, [0](x0) = x0 + 1, [1](x0) = 0, [j](x0) = 0, [opp](x0) = x0 + 1, [#] = 1, [+#](x0, x1) = x0 Strict: +#(+(x, y), z) -> +#(y, z) 1 + 1x + 1y + 0z >= 0 + 1y + 0z +#(+(x, y), z) -> +#(x, +(y, z)) 1 + 1x + 1y + 0z >= 0 + 1x + 0y + 0z Weak: *(*(x, y), z) -> *(x, *(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z *(j x, y) -> -(0 *(x, y), y) 0 + 0x + 1y >= 0 + 0x + 0y *(1 x, y) -> +(0 *(x, y), y) 0 + 0x + 1y >= 2 + 0x + 2y *(0 x, y) -> 0 *(x, y) 0 + 0x + 1y >= 1 + 0x + 1y *(#(), x) -> #() 0 + 1x >= 1 -(x, y) -> +(x, opp y) 0 + 0x + 0y >= 2 + 1x + 1y opp j x -> 1 opp x 1 + 0x >= 0 + 0x opp 1 x -> j opp x 1 + 0x >= 0 + 0x opp 0 x -> 0 opp x 2 + 1x >= 2 + 1x opp #() -> #() 2 >= 1 +(j x, j y) -> 1 +(+(x, y), j #()) 1 + 0x + 0y >= 0 + 0x + 0y +(j x, 1 y) -> 0 +(x, y) 1 + 0x + 0y >= 2 + 1x + 1y +(j x, 0 y) -> j +(x, y) 2 + 0x + 1y >= 0 + 0x + 0y +(1 x, j y) -> 0 +(x, y) 1 + 0x + 0y >= 2 + 1x + 1y +(1 x, 1 y) -> j +(+(x, y), 1 #()) 1 + 0x + 0y >= 0 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 2 + 0x + 1y >= 0 + 0x + 0y +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(0 x, j y) -> j +(x, y) 2 + 1x + 0y >= 0 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 2 + 1x + 0y >= 0 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(#(), x) -> x 2 + 1x >= 1x +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 Qed