YES Time: 0.186737 TRS: {+(x, c(y, z)) -> c(y, +(x, 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()), +(c(x, y), z) -> c(x, +(y, z)), c(x, c(y, z)) -> c(+(x, y), z), c(0(), x) -> x} DP: DP: {+#(x, c(y, z)) -> +#(x, z), +#(x, c(y, z)) -> c#(y, +(x, 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()), +#(c(x, y), z) -> +#(y, z), +#(c(x, y), z) -> c#(x, +(y, z)), c#(x, c(y, z)) -> +#(x, y), c#(x, c(y, z)) -> c#(+(x, y), z)} TRS: {+(x, c(y, z)) -> c(y, +(x, 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()), +(c(x, y), z) -> c(x, +(y, z)), c(x, c(y, z)) -> c(+(x, y), z), c(0(), x) -> x} EDG: {(+#(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)) (+#(x, c(y, z)) -> +#(x, z), +#(c(x, y), z) -> c#(x, +(y, z))) (+#(x, c(y, z)) -> +#(x, z), +#(c(x, y), z) -> +#(y, z)) (+#(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), +#(x, c(y, z)) -> c#(y, +(x, z))) (+#(x, c(y, z)) -> +#(x, 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), +#(9(), 9()) -> c#(1(), 8())) (+#(c(x, y), z) -> +#(y, z), +#(9(), 8()) -> c#(1(), 7())) (+#(c(x, y), z) -> +#(y, z), +#(9(), 7()) -> c#(1(), 6())) (+#(c(x, y), z) -> +#(y, z), +#(9(), 6()) -> c#(1(), 5())) (+#(c(x, y), z) -> +#(y, z), +#(9(), 5()) -> c#(1(), 4())) (+#(c(x, y), z) -> +#(y, z), +#(9(), 4()) -> c#(1(), 3())) (+#(c(x, y), z) -> +#(y, z), +#(9(), 3()) -> c#(1(), 2())) (+#(c(x, y), z) -> +#(y, z), +#(9(), 2()) -> c#(1(), 1())) (+#(c(x, y), z) -> +#(y, z), +#(9(), 1()) -> c#(1(), 0())) (+#(c(x, y), z) -> +#(y, z), +#(8(), 9()) -> c#(1(), 7())) (+#(c(x, y), z) -> +#(y, z), +#(8(), 8()) -> c#(1(), 6())) (+#(c(x, y), z) -> +#(y, z), +#(8(), 7()) -> c#(1(), 5())) (+#(c(x, y), z) -> +#(y, z), +#(8(), 6()) -> c#(1(), 4())) (+#(c(x, y), z) -> +#(y, z), +#(8(), 5()) -> c#(1(), 3())) (+#(c(x, y), z) -> +#(y, z), +#(8(), 4()) -> c#(1(), 2())) (+#(c(x, y), z) -> +#(y, z), +#(8(), 3()) -> c#(1(), 1())) (+#(c(x, y), z) -> +#(y, z), +#(8(), 2()) -> c#(1(), 0())) (+#(c(x, y), z) -> +#(y, z), +#(7(), 9()) -> c#(1(), 6())) (+#(c(x, y), z) -> +#(y, z), +#(7(), 8()) -> c#(1(), 5())) (+#(c(x, y), z) -> +#(y, z), +#(7(), 7()) -> c#(1(), 4())) (+#(c(x, y), z) -> +#(y, z), +#(7(), 6()) -> c#(1(), 3())) (+#(c(x, y), z) -> +#(y, z), +#(7(), 5()) -> c#(1(), 2())) (+#(c(x, y), z) -> +#(y, z), +#(7(), 4()) -> c#(1(), 1())) (+#(c(x, y), z) -> +#(y, z), +#(7(), 3()) -> c#(1(), 0())) (+#(c(x, y), z) -> +#(y, z), +#(6(), 9()) -> c#(1(), 5())) (+#(c(x, y), z) -> +#(y, z), +#(6(), 8()) -> c#(1(), 4())) (+#(c(x, y), z) -> +#(y, z), +#(6(), 7()) -> c#(1(), 3())) (+#(c(x, y), z) -> +#(y, z), +#(6(), 6()) -> c#(1(), 2())) (+#(c(x, y), z) -> +#(y, z), +#(6(), 5()) -> c#(1(), 1())) (+#(c(x, y), z) -> +#(y, z), +#(6(), 4()) -> c#(1(), 0())) (+#(c(x, y), z) -> +#(y, z), +#(5(), 9()) -> c#(1(), 4())) (+#(c(x, y), z) -> +#(y, z), +#(5(), 8()) -> c#(1(), 3())) (+#(c(x, y), z) -> +#(y, z), +#(5(), 7()) -> c#(1(), 2())) (+#(c(x, y), z) -> +#(y, z), +#(5(), 6()) -> c#(1(), 1())) (+#(c(x, y), z) -> +#(y, z), +#(5(), 5()) -> c#(1(), 0())) (+#(c(x, y), z) -> +#(y, z), +#(4(), 9()) -> c#(1(), 3())) (+#(c(x, y), z) -> +#(y, z), +#(4(), 8()) -> c#(1(), 2())) (+#(c(x, y), z) -> +#(y, z), +#(4(), 7()) -> c#(1(), 1())) (+#(c(x, y), z) -> +#(y, z), +#(4(), 6()) -> c#(1(), 0())) (+#(c(x, y), z) -> +#(y, z), +#(3(), 9()) -> c#(1(), 2())) (+#(c(x, y), z) -> +#(y, z), +#(3(), 8()) -> c#(1(), 1())) (+#(c(x, y), z) -> +#(y, z), +#(3(), 7()) -> c#(1(), 0())) (+#(c(x, y), z) -> +#(y, z), +#(2(), 9()) -> c#(1(), 1())) (+#(c(x, y), z) -> +#(y, z), +#(2(), 8()) -> c#(1(), 0())) (+#(c(x, y), z) -> +#(y, z), +#(1(), 9()) -> c#(1(), 0())) (+#(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, 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))) (c#(x, c(y, z)) -> +#(x, y), +#(1(), 9()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(2(), 8()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(2(), 9()) -> c#(1(), 1())) (c#(x, c(y, z)) -> +#(x, y), +#(3(), 7()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(3(), 8()) -> c#(1(), 1())) (c#(x, c(y, z)) -> +#(x, y), +#(3(), 9()) -> c#(1(), 2())) (c#(x, c(y, z)) -> +#(x, y), +#(4(), 6()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(4(), 7()) -> c#(1(), 1())) (c#(x, c(y, z)) -> +#(x, y), +#(4(), 8()) -> c#(1(), 2())) (c#(x, c(y, z)) -> +#(x, y), +#(4(), 9()) -> c#(1(), 3())) (c#(x, c(y, z)) -> +#(x, y), +#(5(), 5()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(5(), 6()) -> c#(1(), 1())) (c#(x, c(y, z)) -> +#(x, y), +#(5(), 7()) -> c#(1(), 2())) (c#(x, c(y, z)) -> +#(x, y), +#(5(), 8()) -> c#(1(), 3())) (c#(x, c(y, z)) -> +#(x, y), +#(5(), 9()) -> c#(1(), 4())) (c#(x, c(y, z)) -> +#(x, y), +#(6(), 4()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(6(), 5()) -> c#(1(), 1())) (c#(x, c(y, z)) -> +#(x, y), +#(6(), 6()) -> c#(1(), 2())) (c#(x, c(y, z)) -> +#(x, y), +#(6(), 7()) -> c#(1(), 3())) (c#(x, c(y, z)) -> +#(x, y), +#(6(), 8()) -> c#(1(), 4())) (c#(x, c(y, z)) -> +#(x, y), +#(6(), 9()) -> c#(1(), 5())) (c#(x, c(y, z)) -> +#(x, y), +#(7(), 3()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(7(), 4()) -> c#(1(), 1())) (c#(x, c(y, z)) -> +#(x, y), +#(7(), 5()) -> c#(1(), 2())) (c#(x, c(y, z)) -> +#(x, y), +#(7(), 6()) -> c#(1(), 3())) (c#(x, c(y, z)) -> +#(x, y), +#(7(), 7()) -> c#(1(), 4())) (c#(x, c(y, z)) -> +#(x, y), +#(7(), 8()) -> c#(1(), 5())) (c#(x, c(y, z)) -> +#(x, y), +#(7(), 9()) -> c#(1(), 6())) (c#(x, c(y, z)) -> +#(x, y), +#(8(), 2()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(8(), 3()) -> c#(1(), 1())) (c#(x, c(y, z)) -> +#(x, y), +#(8(), 4()) -> c#(1(), 2())) (c#(x, c(y, z)) -> +#(x, y), +#(8(), 5()) -> c#(1(), 3())) (c#(x, c(y, z)) -> +#(x, y), +#(8(), 6()) -> c#(1(), 4())) (c#(x, c(y, z)) -> +#(x, y), +#(8(), 7()) -> c#(1(), 5())) (c#(x, c(y, z)) -> +#(x, y), +#(8(), 8()) -> c#(1(), 6())) (c#(x, c(y, z)) -> +#(x, y), +#(8(), 9()) -> c#(1(), 7())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 1()) -> c#(1(), 0())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 2()) -> c#(1(), 1())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 3()) -> c#(1(), 2())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 4()) -> c#(1(), 3())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 5()) -> c#(1(), 4())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 6()) -> c#(1(), 5())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 7()) -> c#(1(), 6())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 8()) -> c#(1(), 7())) (c#(x, c(y, z)) -> +#(x, y), +#(9(), 9()) -> c#(1(), 8())) (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)) -> c#(+(x, y), z), c#(x, c(y, z)) -> +#(x, y)) (c#(x, c(y, z)) -> c#(+(x, y), z), c#(x, c(y, z)) -> c#(+(x, y), 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))} STATUS: arrows: 0.941176 SCCS (1): Scc: {+#(x, c(y, z)) -> +#(x, z), +#(x, c(y, z)) -> c#(y, +(x, z)), +#(c(x, y), z) -> +#(y, z), +#(c(x, y), z) -> c#(x, +(y, z)), c#(x, c(y, z)) -> +#(x, y), c#(x, c(y, z)) -> c#(+(x, y), z)} SCC (6): Strict: {+#(x, c(y, z)) -> +#(x, z), +#(x, c(y, z)) -> c#(y, +(x, z)), +#(c(x, y), z) -> +#(y, z), +#(c(x, y), z) -> c#(x, +(y, z)), c#(x, c(y, z)) -> +#(x, y), c#(x, c(y, z)) -> c#(+(x, y), z)} Weak: {+(x, c(y, z)) -> c(y, +(x, 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()), +(c(x, y), z) -> c(x, +(y, z)), c(x, c(y, z)) -> c(+(x, y), z), c(0(), x) -> x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [c](x0, x1) = x0 + x1 + 1, [0] = 0, [1] = 0, [2] = 1, [3] = 0, [4] = 1, [5] = 0, [6] = 1, [7] = 1, [8] = 1, [9] = 1, [+#](x0, x1) = x0 + x1 + 1, [c#](x0, x1) = x0 + x1 + 1 Strict: c#(x, c(y, z)) -> c#(+(x, y), z) 2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z c#(x, c(y, z)) -> +#(x, y) 2 + 1y + 1x + 1z >= 1 + 1y + 1x +#(c(x, y), z) -> c#(x, +(y, z)) 2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z +#(c(x, y), z) -> +#(y, z) 2 + 1y + 1x + 1z >= 1 + 1y + 1z +#(x, c(y, z)) -> c#(y, +(x, z)) 2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z +#(x, c(y, z)) -> +#(x, z) 2 + 1y + 1x + 1z >= 1 + 1x + 1z Weak: c(0(), x) -> x 1 + 1x >= 1x c(x, c(y, z)) -> c(+(x, y), z) 2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z +(c(x, y), z) -> c(x, +(y, z)) 2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z +(9(), 9()) -> c(1(), 8()) 3 >= 2 +(9(), 8()) -> c(1(), 7()) 3 >= 2 +(9(), 7()) -> c(1(), 6()) 3 >= 2 +(9(), 6()) -> c(1(), 5()) 3 >= 1 +(9(), 5()) -> c(1(), 4()) 2 >= 2 +(9(), 4()) -> c(1(), 3()) 3 >= 1 +(9(), 3()) -> c(1(), 2()) 2 >= 2 +(9(), 2()) -> c(1(), 1()) 3 >= 1 +(9(), 1()) -> c(1(), 0()) 2 >= 1 +(9(), 0()) -> 9() 2 >= 1 +(8(), 9()) -> c(1(), 7()) 3 >= 2 +(8(), 8()) -> c(1(), 6()) 3 >= 2 +(8(), 7()) -> c(1(), 5()) 3 >= 1 +(8(), 6()) -> c(1(), 4()) 3 >= 2 +(8(), 5()) -> c(1(), 3()) 2 >= 1 +(8(), 4()) -> c(1(), 2()) 3 >= 2 +(8(), 3()) -> c(1(), 1()) 2 >= 1 +(8(), 2()) -> c(1(), 0()) 3 >= 1 +(8(), 1()) -> 9() 2 >= 1 +(8(), 0()) -> 8() 2 >= 1 +(7(), 9()) -> c(1(), 6()) 3 >= 2 +(7(), 8()) -> c(1(), 5()) 3 >= 1 +(7(), 7()) -> c(1(), 4()) 3 >= 2 +(7(), 6()) -> c(1(), 3()) 3 >= 1 +(7(), 5()) -> c(1(), 2()) 2 >= 2 +(7(), 4()) -> c(1(), 1()) 3 >= 1 +(7(), 3()) -> c(1(), 0()) 2 >= 1 +(7(), 2()) -> 9() 3 >= 1 +(7(), 1()) -> 8() 2 >= 1 +(7(), 0()) -> 7() 2 >= 1 +(6(), 9()) -> c(1(), 5()) 3 >= 1 +(6(), 8()) -> c(1(), 4()) 3 >= 2 +(6(), 7()) -> c(1(), 3()) 3 >= 1 +(6(), 6()) -> c(1(), 2()) 3 >= 2 +(6(), 5()) -> c(1(), 1()) 2 >= 1 +(6(), 4()) -> c(1(), 0()) 3 >= 1 +(6(), 3()) -> 9() 2 >= 1 +(6(), 2()) -> 8() 3 >= 1 +(6(), 1()) -> 7() 2 >= 1 +(6(), 0()) -> 6() 2 >= 1 +(5(), 9()) -> c(1(), 4()) 2 >= 2 +(5(), 8()) -> c(1(), 3()) 2 >= 1 +(5(), 7()) -> c(1(), 2()) 2 >= 2 +(5(), 6()) -> c(1(), 1()) 2 >= 1 +(5(), 5()) -> c(1(), 0()) 1 >= 1 +(5(), 4()) -> 9() 2 >= 1 +(5(), 3()) -> 8() 1 >= 1 +(5(), 2()) -> 7() 2 >= 1 +(5(), 1()) -> 6() 1 >= 1 +(5(), 0()) -> 5() 1 >= 0 +(4(), 9()) -> c(1(), 3()) 3 >= 1 +(4(), 8()) -> c(1(), 2()) 3 >= 2 +(4(), 7()) -> c(1(), 1()) 3 >= 1 +(4(), 6()) -> c(1(), 0()) 3 >= 1 +(4(), 5()) -> 9() 2 >= 1 +(4(), 4()) -> 8() 3 >= 1 +(4(), 3()) -> 7() 2 >= 1 +(4(), 2()) -> 6() 3 >= 1 +(4(), 1()) -> 5() 2 >= 0 +(4(), 0()) -> 4() 2 >= 1 +(3(), 9()) -> c(1(), 2()) 2 >= 2 +(3(), 8()) -> c(1(), 1()) 2 >= 1 +(3(), 7()) -> c(1(), 0()) 2 >= 1 +(3(), 6()) -> 9() 2 >= 1 +(3(), 5()) -> 8() 1 >= 1 +(3(), 4()) -> 7() 2 >= 1 +(3(), 3()) -> 6() 1 >= 1 +(3(), 2()) -> 5() 2 >= 0 +(3(), 1()) -> 4() 1 >= 1 +(3(), 0()) -> 3() 1 >= 0 +(2(), 9()) -> c(1(), 1()) 3 >= 1 +(2(), 8()) -> c(1(), 0()) 3 >= 1 +(2(), 7()) -> 9() 3 >= 1 +(2(), 6()) -> 8() 3 >= 1 +(2(), 5()) -> 7() 2 >= 1 +(2(), 4()) -> 6() 3 >= 1 +(2(), 3()) -> 5() 2 >= 0 +(2(), 2()) -> 4() 3 >= 1 +(2(), 1()) -> 3() 2 >= 0 +(2(), 0()) -> 2() 2 >= 1 +(1(), 9()) -> c(1(), 0()) 2 >= 1 +(1(), 8()) -> 9() 2 >= 1 +(1(), 7()) -> 8() 2 >= 1 +(1(), 6()) -> 7() 2 >= 1 +(1(), 5()) -> 6() 1 >= 1 +(1(), 4()) -> 5() 2 >= 0 +(1(), 3()) -> 4() 1 >= 1 +(1(), 2()) -> 3() 2 >= 0 +(1(), 1()) -> 2() 1 >= 1 +(1(), 0()) -> 1() 1 >= 0 +(0(), 9()) -> 9() 2 >= 1 +(0(), 8()) -> 8() 2 >= 1 +(0(), 7()) -> 7() 2 >= 1 +(0(), 6()) -> 6() 2 >= 1 +(0(), 5()) -> 5() 1 >= 0 +(0(), 4()) -> 4() 2 >= 1 +(0(), 3()) -> 3() 1 >= 0 +(0(), 2()) -> 2() 2 >= 1 +(0(), 1()) -> 1() 1 >= 0 +(0(), 0()) -> 0() 1 >= 0 +(x, c(y, z)) -> c(y, +(x, z)) 2 + 1y + 1x + 1z >= 2 + 1y + 1x + 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: {+(x, c(y, z)) -> c(y, +(x, 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()), +(c(x, y), z) -> c(x, +(y, z)), c(x, c(y, z)) -> c(+(x, y), z), c(0(), x) -> x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + 1, [c](x0, x1) = x0 + 1, [0] = 0, [1] = 1, [2] = 1, [3] = 1, [4] = 1, [5] = 1, [6] = 1, [7] = 1, [8] = 1, [9] = 1, [c#](x0, x1) = x0 Strict: c#(x, c(y, z)) -> c#(+(x, y), z) 1 + 0y + 0x + 1z >= 0 + 0y + 0x + 1z Weak: c(0(), x) -> x 1 + 1x >= 1x c(x, c(y, z)) -> c(+(x, y), z) 2 + 0y + 0x + 1z >= 1 + 0y + 0x + 1z +(c(x, y), z) -> c(x, +(y, z)) 1 + 0y + 0x + 1z >= 2 + 0y + 0x + 1z +(9(), 9()) -> c(1(), 8()) 2 >= 2 +(9(), 8()) -> c(1(), 7()) 2 >= 2 +(9(), 7()) -> c(1(), 6()) 2 >= 2 +(9(), 6()) -> c(1(), 5()) 2 >= 2 +(9(), 5()) -> c(1(), 4()) 2 >= 2 +(9(), 4()) -> c(1(), 3()) 2 >= 2 +(9(), 3()) -> c(1(), 2()) 2 >= 2 +(9(), 2()) -> c(1(), 1()) 2 >= 2 +(9(), 1()) -> c(1(), 0()) 2 >= 1 +(9(), 0()) -> 9() 1 >= 1 +(8(), 9()) -> c(1(), 7()) 2 >= 2 +(8(), 8()) -> c(1(), 6()) 2 >= 2 +(8(), 7()) -> c(1(), 5()) 2 >= 2 +(8(), 6()) -> c(1(), 4()) 2 >= 2 +(8(), 5()) -> c(1(), 3()) 2 >= 2 +(8(), 4()) -> c(1(), 2()) 2 >= 2 +(8(), 3()) -> c(1(), 1()) 2 >= 2 +(8(), 2()) -> c(1(), 0()) 2 >= 1 +(8(), 1()) -> 9() 2 >= 1 +(8(), 0()) -> 8() 1 >= 1 +(7(), 9()) -> c(1(), 6()) 2 >= 2 +(7(), 8()) -> c(1(), 5()) 2 >= 2 +(7(), 7()) -> c(1(), 4()) 2 >= 2 +(7(), 6()) -> c(1(), 3()) 2 >= 2 +(7(), 5()) -> c(1(), 2()) 2 >= 2 +(7(), 4()) -> c(1(), 1()) 2 >= 2 +(7(), 3()) -> c(1(), 0()) 2 >= 1 +(7(), 2()) -> 9() 2 >= 1 +(7(), 1()) -> 8() 2 >= 1 +(7(), 0()) -> 7() 1 >= 1 +(6(), 9()) -> c(1(), 5()) 2 >= 2 +(6(), 8()) -> c(1(), 4()) 2 >= 2 +(6(), 7()) -> c(1(), 3()) 2 >= 2 +(6(), 6()) -> c(1(), 2()) 2 >= 2 +(6(), 5()) -> c(1(), 1()) 2 >= 2 +(6(), 4()) -> c(1(), 0()) 2 >= 1 +(6(), 3()) -> 9() 2 >= 1 +(6(), 2()) -> 8() 2 >= 1 +(6(), 1()) -> 7() 2 >= 1 +(6(), 0()) -> 6() 1 >= 1 +(5(), 9()) -> c(1(), 4()) 2 >= 2 +(5(), 8()) -> c(1(), 3()) 2 >= 2 +(5(), 7()) -> c(1(), 2()) 2 >= 2 +(5(), 6()) -> c(1(), 1()) 2 >= 2 +(5(), 5()) -> c(1(), 0()) 2 >= 1 +(5(), 4()) -> 9() 2 >= 1 +(5(), 3()) -> 8() 2 >= 1 +(5(), 2()) -> 7() 2 >= 1 +(5(), 1()) -> 6() 2 >= 1 +(5(), 0()) -> 5() 1 >= 1 +(4(), 9()) -> c(1(), 3()) 2 >= 2 +(4(), 8()) -> c(1(), 2()) 2 >= 2 +(4(), 7()) -> c(1(), 1()) 2 >= 2 +(4(), 6()) -> c(1(), 0()) 2 >= 1 +(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() 1 >= 1 +(3(), 9()) -> c(1(), 2()) 2 >= 2 +(3(), 8()) -> c(1(), 1()) 2 >= 2 +(3(), 7()) -> c(1(), 0()) 2 >= 1 +(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() 1 >= 1 +(2(), 9()) -> c(1(), 1()) 2 >= 2 +(2(), 8()) -> c(1(), 0()) 2 >= 1 +(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() 1 >= 1 +(1(), 9()) -> c(1(), 0()) 2 >= 1 +(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() 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() 2 >= 1 +(0(), 1()) -> 1() 2 >= 1 +(0(), 0()) -> 0() 1 >= 0 +(x, c(y, z)) -> c(y, +(x, z)) 2 + 0y + 0x + 1z >= 2 + 0y + 0x + 1z Qed