MAYBE Time: 0.008813 TRS: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z)), sum nil() -> 0 #(), sum cons(x, l) -> +(x, sum l), prod nil() -> 1 #(), prod cons(x, l) -> *(x, prod l)} DP: DP: { +#(0 x, 0 y) -> 0# +(x, y), +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()), *#(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), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z), sum# nil() -> 0# #(), sum# cons(x, l) -> +#(x, sum l), sum# cons(x, l) -> sum# l, prod# cons(x, l) -> *#(x, prod l), prod# cons(x, l) -> prod# l} TRS: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z)), sum nil() -> 0 #(), sum cons(x, l) -> +(x, sum l), prod nil() -> 1 #(), prod cons(x, l) -> *(x, prod l)} EDG: {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 0 y) -> +#(x, 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)), +#(0 x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 0 y) -> 0# +(x, 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)), *#(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)) (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> sum# l) (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> +#(x, sum l)) (sum# cons(x, l) -> sum# l, sum# nil() -> 0# #()) (sum# cons(x, l) -> +#(x, sum l), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (sum# cons(x, l) -> +#(x, sum l), +#(1 x, 1 y) -> +#(x, y)) (sum# cons(x, l) -> +#(x, sum l), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (sum# cons(x, l) -> +#(x, sum l), +#(1 x, 0 y) -> +#(x, y)) (sum# cons(x, l) -> +#(x, sum l), +#(+(x, y), z) -> +#(y, z)) (sum# cons(x, l) -> +#(x, sum l), +#(+(x, y), z) -> +#(x, +(y, z))) (sum# cons(x, l) -> +#(x, sum l), +#(0 x, 1 y) -> +#(x, y)) (sum# cons(x, l) -> +#(x, sum l), +#(0 x, 0 y) -> +#(x, y)) (sum# cons(x, l) -> +#(x, sum l), +#(0 x, 0 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, 1 y) -> 0# +(+(x, y), 1 #())) (+#(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, 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)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y)) (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(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), *#(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), +#(+(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) -> 0# +(+(x, y), 1 #())) (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y)) (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(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), +#(+(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) -> 0# +(+(x, y), 1 #())) (+#(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 #())) (prod# cons(x, l) -> *#(x, prod l), *#(0 x, y) -> 0# *(x, y)) (prod# cons(x, l) -> *#(x, prod l), *#(0 x, y) -> *#(x, y)) (prod# cons(x, l) -> *#(x, prod l), *#(1 x, y) -> 0# *(x, y)) (prod# cons(x, l) -> *#(x, prod l), *#(1 x, y) -> +#(0 *(x, y), y)) (prod# cons(x, l) -> *#(x, prod l), *#(1 x, y) -> *#(x, y)) (prod# cons(x, l) -> *#(x, prod l), *#(*(x, y), z) -> *#(x, *(y, z))) (prod# cons(x, l) -> *#(x, prod l), *#(*(x, y), z) -> *#(y, z)) (prod# cons(x, l) -> prod# l, prod# cons(x, l) -> *#(x, prod l)) (prod# cons(x, l) -> prod# l, prod# cons(x, l) -> prod# l) (*#(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))} STATUS: arrows: 0.746032 SCCS (4): Scc: {prod# cons(x, l) -> prod# l} Scc: {sum# cons(x, l) -> sum# l} Scc: { *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Scc: { +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 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 #())} SCC (1): Strict: {prod# cons(x, l) -> prod# l} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z)), sum nil() -> 0 #(), sum cons(x, l) -> +(x, sum l), prod nil() -> 1 #(), prod cons(x, l) -> *(x, prod l)} Open SCC (1): Strict: {sum# cons(x, l) -> sum# l} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z)), sum nil() -> 0 #(), sum cons(x, l) -> +(x, sum l), prod nil() -> 1 #(), prod cons(x, l) -> *(x, prod l)} Open SCC (4): Strict: { *#(0 x, y) -> *#(x, y), *#(1 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), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z)), sum nil() -> 0 #(), sum cons(x, l) -> +(x, sum l), prod nil() -> 1 #(), prod cons(x, l) -> *(x, prod l)} Open SCC (7): Strict: { +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 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 #())} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), *(#(), x) -> #(), *(0 x, y) -> 0 *(x, y), *(1 x, y) -> +(0 *(x, y), y), *(*(x, y), z) -> *(x, *(y, z)), sum nil() -> 0 #(), sum cons(x, l) -> +(x, sum l), prod nil() -> 1 #(), prod cons(x, l) -> *(x, prod l)} Open