MAYBE Problem: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(q(x)) -> d(e(x)) Proof: DP Processor: DPs: d#(s(x)) -> d#(x) e#(q(x)) -> e#(x) e#(q(x)) -> d#(e(x)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(q(x)) -> d(e(x)) TDG Processor: DPs: d#(s(x)) -> d#(x) e#(q(x)) -> e#(x) e#(q(x)) -> d#(e(x)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(q(x)) -> d(e(x)) graph: e#(q(x)) -> e#(x) -> e#(q(x)) -> d#(e(x)) e#(q(x)) -> e#(x) -> e#(q(x)) -> e#(x) e#(q(x)) -> d#(e(x)) -> d#(s(x)) -> d#(x) d#(s(x)) -> d#(x) -> d#(s(x)) -> d#(x) Restore Modifier: DPs: d#(s(x)) -> d#(x) e#(q(x)) -> e#(x) e#(q(x)) -> d#(e(x)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(q(x)) -> d(e(x)) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/9 DPs: e#(q(x)) -> e#(x) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(q(x)) -> d(e(x)) Open DPs: d#(s(x)) -> d#(x) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(q(x)) -> d(e(x)) Open