MAYBE Problem: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Proof: DP Processor: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(s(f(x))) -> g#(f(x)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Usable Rule Processor: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(s(f(x))) -> g#(f(x)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) ADG Processor: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(s(f(x))) -> g#(f(x)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) graph: g#(c(x,s(y))) -> g#(c(s(x),y)) -> g#(c(x,s(y))) -> g#(c(s(x),y)) f#(c(s(x),y)) -> f#(c(x,s(y))) -> f#(c(s(x),y)) -> f#(c(x,s(y))) Restore Modifier: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(s(f(x))) -> g#(f(x)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) SCC Processor: #sccs: 2 #rules: 2 #arcs: 2/9 DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Open DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Open