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