MAYBE Problem: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) Proof: DP Processor: DPs: f#(s(x),s(y)) -> f#(x,y) g#(0(),x) -> f#(x,x) g#(0(),x) -> g#(f(x,x),x) TRS: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) EDG Processor: DPs: f#(s(x),s(y)) -> f#(x,y) g#(0(),x) -> f#(x,x) g#(0(),x) -> g#(f(x,x),x) TRS: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) graph: g#(0(),x) -> f#(x,x) -> f#(s(x),s(y)) -> f#(x,y) f#(s(x),s(y)) -> f#(x,y) -> f#(s(x),s(y)) -> f#(x,y) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/9 DPs: f#(s(x),s(y)) -> f#(x,y) TRS: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) Open