MAYBE Problem: +(1(),x) -> +(+(0(),1()),x) +(0(),x) -> x Proof: DP Processor: DPs: +#(1(),x) -> +#(0(),1()) +#(1(),x) -> +#(+(0(),1()),x) TRS: +(1(),x) -> +(+(0(),1()),x) +(0(),x) -> x Open