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) SCC Processor: #sccs: 1 #rules: 2 #arcs: 10/25 DPs: g#(c(),g(a(x),y)) -> g#(f(a(b())),g(a(y),x)) g#(c(),g(a(x),y)) -> 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() Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0, x1) = x0, [d] = 0, [f](x0) = 1, [b] = 0, [g](x0, x1) = 1, [a](x0) = 0, [c] = 1 orientation: g#(c(),g(a(x),y)) = 1 >= 1 = g#(f(a(b())),g(a(y),x)) g#(c(),g(a(x),y)) = 1 >= 0 = g#(a(y),x) g(c(),g(a(x),y)) = 1 >= 1 = g(f(a(b())),g(a(y),x)) f(a(x)) = 1 >= 1 = c() a(b()) = 0 >= 0 = d() problem: 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