YES Time: 0.046753 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))} 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, y) -> +#(0 *(x, y), y), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(1 x, y) -> +#(0 *(x, y), y), +#(+(x, y), z) -> +#(y, z)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 0 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 1 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, j y) -> 0# +(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, j y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, 0 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, 1 y) -> 0# +(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, 1 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, j y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, j y) -> +#(+(x, y), j #())) (+#(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)) } 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))} SPSC: Simple Projection: pi(*#) = 0 Strict: { *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} EDG: {(*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(0 x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))} SCCS (1): Scc: { *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC (4): Strict: { *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y), *#(*(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))} SPSC: Simple Projection: pi(*#) = 0 Strict: { *#(0 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} EDG: {(*#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(j x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(0 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))} SCCS (1): Scc: { *#(0 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC (3): Strict: { *#(0 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y), *#(*(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))} SPSC: Simple Projection: pi(*#) = 0 Strict: { *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} EDG: {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(j x, y) -> *#(x, y)) (*#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))} SCCS (1): Scc: { *#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC (2): Strict: { *#(j x, y) -> *#(x, y), *#(*(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))} SPSC: Simple Projection: pi(*#) = 0 Strict: {*#(*(x, y), z) -> *#(y, z)} EDG: {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))} SCCS (1): Scc: {*#(*(x, y), z) -> *#(y, z)} SCC (1): Strict: {*#(*(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))} SPSC: Simple Projection: pi(*#) = 0 Strict: {} 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))} SPSC: Simple Projection: pi(opp#) = 0 Strict: {opp# 0 x -> opp# x, opp# j x -> opp# x} EDG: {(opp# j x -> opp# x, opp# j x -> opp# x) (opp# j x -> opp# x, opp# 0 x -> opp# x) (opp# 0 x -> opp# x, opp# 0 x -> opp# x) (opp# 0 x -> opp# x, opp# j x -> opp# x)} SCCS (1): Scc: {opp# 0 x -> opp# x, opp# j x -> opp# x} SCC (2): Strict: {opp# 0 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))} SPSC: Simple Projection: pi(opp#) = 0 Strict: {opp# j x -> opp# x} EDG: {(opp# j x -> opp# x, opp# j x -> opp# x)} SCCS (1): Scc: {opp# j x -> opp# x} SCC (1): Strict: {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))} SPSC: Simple Projection: pi(opp#) = 0 Strict: {} 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: EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(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))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))} 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))} SPSC: Simple Projection: pi(+#) = 0 Strict: {+#(+(x, y), z) -> +#(y, z)} EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))} SCCS (1): Scc: {+#(+(x, y), z) -> +#(y, z)} SCC (1): Strict: {+#(+(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))} SPSC: Simple Projection: pi(+#) = 0 Strict: {} Qed