MAYBE Problem: f(s(X)) -> f(X) g(cons(0(),Y)) -> g(Y) g(cons(s(X),Y)) -> s(X) h(cons(X,Y)) -> h(g(cons(X,Y))) Proof: DP Processor: DPs: f#(s(X)) -> f#(X) g#(cons(0(),Y)) -> g#(Y) h#(cons(X,Y)) -> g#(cons(X,Y)) h#(cons(X,Y)) -> h#(g(cons(X,Y))) TRS: f(s(X)) -> f(X) g(cons(0(),Y)) -> g(Y) g(cons(s(X),Y)) -> s(X) h(cons(X,Y)) -> h(g(cons(X,Y))) Usable Rule Processor: DPs: f#(s(X)) -> f#(X) g#(cons(0(),Y)) -> g#(Y) h#(cons(X,Y)) -> g#(cons(X,Y)) h#(cons(X,Y)) -> h#(g(cons(X,Y))) TRS: g(cons(0(),Y)) -> g(Y) g(cons(s(X),Y)) -> s(X) ADG Processor: DPs: f#(s(X)) -> f#(X) g#(cons(0(),Y)) -> g#(Y) h#(cons(X,Y)) -> g#(cons(X,Y)) h#(cons(X,Y)) -> h#(g(cons(X,Y))) TRS: g(cons(0(),Y)) -> g(Y) g(cons(s(X),Y)) -> s(X) graph: h#(cons(X,Y)) -> g#(cons(X,Y)) -> g#(cons(0(),Y)) -> g#(Y) g#(cons(0(),Y)) -> g#(Y) -> g#(cons(0(),Y)) -> g#(Y) f#(s(X)) -> f#(X) -> f#(s(X)) -> f#(X) Restore Modifier: DPs: f#(s(X)) -> f#(X) g#(cons(0(),Y)) -> g#(Y) h#(cons(X,Y)) -> g#(cons(X,Y)) h#(cons(X,Y)) -> h#(g(cons(X,Y))) TRS: f(s(X)) -> f(X) g(cons(0(),Y)) -> g(Y) g(cons(s(X),Y)) -> s(X) h(cons(X,Y)) -> h(g(cons(X,Y))) SCC Processor: #sccs: 2 #rules: 2 #arcs: 3/16 DPs: f#(s(X)) -> f#(X) TRS: f(s(X)) -> f(X) g(cons(0(),Y)) -> g(Y) g(cons(s(X),Y)) -> s(X) h(cons(X,Y)) -> h(g(cons(X,Y))) Open DPs: g#(cons(0(),Y)) -> g#(Y) TRS: f(s(X)) -> f(X) g(cons(0(),Y)) -> g(Y) g(cons(s(X),Y)) -> s(X) h(cons(X,Y)) -> h(g(cons(X,Y))) Open