MAYBE Time: 0.019 Problem: Equations: TRS: 1() -> s(0()) 2() -> s(1()) 3() -> s(2()) 4() -> s(3()) 5() -> s(4()) 6() -> s(5()) 7() -> s(6()) 8() -> s(7()) 9() -> s(8()) max'C(0(),x) -> x max'C(s(x),s(y)) -> s(max'C(x,y)) app(empty(),X) -> X max(singl(x)) -> x max(app(singl(x),Y)) -> max2(x,Y) max2(x,empty()) -> x max2(x,singl(y)) -> max'C(x,y) max2(x,app(singl(y),Z)) -> max2(max'C(x,y),Z) Proof: Open