MAYBE Problem: f(0()) -> cons(0(),f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() Proof: DP Processor: DPs: f#(0()) -> f#(s(0())) f#(s(0())) -> p#(s(0())) f#(s(0())) -> f#(p(s(0()))) TRS: f(0()) -> cons(0(),f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() CDG Processor: DPs: f#(0()) -> f#(s(0())) f#(s(0())) -> p#(s(0())) f#(s(0())) -> f#(p(s(0()))) TRS: f(0()) -> cons(0(),f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() graph: f#(s(0())) -> f#(p(s(0()))) -> f#(0()) -> f#(s(0())) f#(0()) -> f#(s(0())) -> f#(s(0())) -> p#(s(0())) f#(0()) -> f#(s(0())) -> f#(s(0())) -> f#(p(s(0()))) SCC Processor: #sccs: 1 #rules: 2 #arcs: 3/9 DPs: f#(s(0())) -> f#(p(s(0()))) f#(0()) -> f#(s(0())) TRS: f(0()) -> cons(0(),f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() Open