MAYBE Problem: g(c(),g(a(x),y)) -> g(f(a(b())),g(a(y),x)) f(a(x)) -> c() a(b()) -> d() Proof: DP Processor: DPs: g#(c(),g(a(x),y)) -> a#(y) g#(c(),g(a(x),y)) -> g#(a(y),x) g#(c(),g(a(x),y)) -> a#(b()) g#(c(),g(a(x),y)) -> f#(a(b())) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) TRS: g(c(),g(a(x),y)) -> g(f(a(b())),g(a(y),x)) f(a(x)) -> c() a(b()) -> d() TDG Processor: DPs: g#(c(),g(a(x),y)) -> a#(y) g#(c(),g(a(x),y)) -> g#(a(y),x) g#(c(),g(a(x),y)) -> a#(b()) g#(c(),g(a(x),y)) -> f#(a(b())) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) TRS: g(c(),g(a(x),y)) -> g(f(a(b())),g(a(y),x)) f(a(x)) -> c() a(b()) -> d() graph: g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> f#(a(b())) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> a#(b()) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> g#(a(y),x) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> a#(y) g#(c(),g(a(x),y)) -> g#(a(y),x) -> g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) g#(c(),g(a(x),y)) -> g#(a(y),x) -> g#(c(),g(a(x),y)) -> f#(a(b())) g#(c(),g(a(x),y)) -> g#(a(y),x) -> g#(c(),g(a(x),y)) -> a#(b()) g#(c(),g(a(x),y)) -> g#(a(y),x) -> g#(c(),g(a(x),y)) -> g#(a(y),x) g#(c(),g(a(x),y)) -> g#(a(y),x) -> g#(c(),g(a(x),y)) -> a#(y) CDG Processor: DPs: g#(c(),g(a(x),y)) -> a#(y) g#(c(),g(a(x),y)) -> g#(a(y),x) g#(c(),g(a(x),y)) -> a#(b()) g#(c(),g(a(x),y)) -> f#(a(b())) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) TRS: g(c(),g(a(x),y)) -> g(f(a(b())),g(a(y),x)) f(a(x)) -> c() a(b()) -> d() graph: g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> a#(y) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> g#(a(y),x) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> a#(b()) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> f#(a(b())) g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) -> g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 5/25 DPs: g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) TRS: g(c(),g(a(x),y)) -> g(f(a(b())),g(a(y),x)) f(a(x)) -> c() a(b()) -> d() Open