MAYBE Problem: f(X,g(X),Y) -> f(Y,Y,Y) g(b()) -> c() b() -> c() Proof: DP Processor: DPs: f#(X,g(X),Y) -> f#(Y,Y,Y) TRS: f(X,g(X),Y) -> f(Y,Y,Y) g(b()) -> c() b() -> c() Usable Rule Processor: DPs: f#(X,g(X),Y) -> f#(Y,Y,Y) TRS: f7(x,y) -> x f7(x,y) -> y Restore Modifier: DPs: f#(X,g(X),Y) -> f#(Y,Y,Y) TRS: f(X,g(X),Y) -> f(Y,Y,Y) g(b()) -> c() b() -> c() SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: f#(X,g(X),Y) -> f#(Y,Y,Y) TRS: f(X,g(X),Y) -> f(Y,Y,Y) g(b()) -> c() b() -> c() Open