YES Problem: g(g(a())) -> f(h(g(f(c(),c()))),f(f(g(c()),a()),g(f(a(),a())))) f(x,y) -> f(y,x) c() -> f(a(),h(b())) f(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) -> c() Proof: AT confluence processor Complete TRS T' of input TRS: g(g(a())) -> f(h(g(f(c(),c()))),f(f(g(c()),a()),g(f(a(),a())))) c() -> f(a(),h(b())) f(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) -> c() f(h(f(h(a()),f(a(),a()))),g(f(x,g(b())))) -> f(h(b()),a()) f(h(f(h(a()),f(a(),a()))),g(f(g(b()),x))) -> f(h(b()),a()) f(h(f(f(a(),a()),h(a()))),g(f(g(b()),x))) -> f(h(b()),a()) f(g(f(x519,g(b()))),h(f(f(a(),a()),h(a())))) -> f(h(b()),a()) f(g(f(x521,g(b()))),h(f(h(a()),f(a(),a())))) -> f(a(),h(b())) f(g(f(g(b()),x523)),h(f(h(a()),f(a(),a())))) -> f(a(),h(b())) f(g(f(g(b()),x525)),h(f(f(a(),a()),h(a())))) -> f(a(),h(b())) f(x,y) -> f(y,x) T' = (P union S) with TRS P:f(x,y) -> f(y,x) TRS S:g(g(a())) -> f(h(g(f(c(),c()))),f(f(g(c()),a()),g(f(a(),a())))) c() -> f(a(),h(b())) f(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) -> c() f(h(f(h(a()),f(a(),a()))),g(f(x,g(b())))) -> f(h(b()),a()) f(h(f(h(a()),f(a(),a()))),g(f(g(b()),x))) -> f(h(b()),a()) f(h(f(f(a(),a()),h(a()))),g(f(g(b()),x))) -> f(h(b()),a()) f(g(f(x519,g(b()))),h(f(f(a(),a()),h(a())))) -> f(h(b()),a()) f(g(f(x521,g(b()))),h(f(h(a()),f(a(),a())))) -> f(a(),h(b())) f(g(f(g(b()),x523)),h(f(h(a()),f(a(),a())))) -> f(a(),h(b())) f(g(f(g(b()),x525)),h(f(f(a(),a()),h(a())))) -> f(a(),h(b())) S is left-linear and P is reversible. CP(S,S) = c() = f(h(b()),a()), f(h(b()),a()) = f(h(b()),a()), f(h(b()),a()) = c(), f(h(b()),a()) = f(a(),h(b())), f(a(),h(b())) = f(a(),h(b())), f(a(),h(b())) = f(h(b()),a()) CP(S,P union P^-1) = c() = f(g(f(x2927,g(b()))),h(f(f(a(),a()),h(a())))), c() = f(g(f(x2928,g(b()))), h(f(f(a(),a()),h(a())))), f(h(b()),a()) = f(g(f(x2929,g(b()))),h(f(h(a()),f(a(),a())))), f(h(b()),a()) = f(g(f(x2930,g(b()))),h(f(h(a()),f(a(),a())))), f(h(b()),a()) = f(g(f(g(b()),x2931)), h(f(h(a()),f(a(),a())))), f(h(b()),a()) = f(g(f(g(b()),x2932)),h(f(h(a()),f(a(),a())))), f(h(b()),a()) = f(g(f(g(b()),x2933)),h(f(f(a(),a()),h(a())))), f(h(b()),a()) = f(g(f(g(b()),x2934)), h(f(f(a(),a()),h(a())))), f(h(b()),a()) = f(h(f(f(a(),a()),h(a()))),g(f(x2935,g(b())))), f(h(b()),a()) = f(h(f(f(a(),a()),h(a()))),g(f(x2936,g(b())))), f(a(),h(b())) = f(h(f(h(a()),f(a(),a()))), g(f(x2937,g(b())))), f(a(),h(b())) = f(h(f(h(a()),f(a(),a()))),g(f(x2938,g(b())))), f(a(),h(b())) = f(h(f(h(a()),f(a(),a()))),g(f(g(b()),x2939))), f(a(),h(b())) = f(h(f(h(a()),f(a(),a()))), g(f(g(b()),x2940))), f(a(),h(b())) = f(h(f(f(a(),a()),h(a()))),g(f(g(b()),x2941))), f(a(),h(b())) = f(h(f(f(a(),a()),h(a()))),g(f(g(b()),x2942))) PCP_in(P union P^-1,S) = f(h(f(h(a()),f(a(),a()))),g(f(x,g(b())))) = c(), f(h(f(h(a()),f(a(),a()))),g(f(g(b()),x))) = c(), f(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) = c(), f(h(f(f(a(),a()),h(a()))),g(f(g(b()),x))) = c(), f(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) = f(h(b()),a()), f(h(f(f(a(),a()),h(a()))), g (f(g(b()),x))) = f(h(b()),a()), f(h(f(h(a()),f(a(),a()))),g(f(x,g(b())))) = f(h(b()),a()), f(h(f(h(a()),f(a(),a()))),g(f(g(b()),x))) = f(h(b()),a()), f(g(f(g(b()),x519)), h(f(f(a(),a()),h(a())))) = f(h(b()),a()), f(g(f(g(b()),x519)),h(f(h(a()),f(a(),a())))) = f(h(b()),a()), f(g(f(x519,g(b()))),h(f(h(a()),f(a(),a())))) = f(h(b()),a()), f(g(f(x519,g(b()))), h(f(f(a(),a()),h(a())))) = f(h(b()),a()), f(g(f(g(b()),x521)),h(f(h(a()),f(a(),a())))) = f(a(),h(b())), f(g(f(g(b()),x521)),h(f(f(a(),a()),h(a())))) = f(a(),h(b())), f(g(f(x521,g(b()))), h(f(f(a(),a()),h(a())))) = f(a(),h(b())), f(g(f(x521,g(b()))),h(f(h(a()),f(a(),a())))) = f(a(),h(b())), f(g(f(x523,g(b()))),h(f(h(a()),f(a(),a())))) = f(a(),h(b())), f(g(f(x523,g(b()))), h(f(f(a(),a()),h(a())))) = f(a(),h(b())), f(g(f(g(b()),x523)),h(f(f(a(),a()),h(a())))) = f(a(),h(b())), f(g(f(g(b()),x523)),h(f(h(a()),f(a(),a())))) = f(a(),h(b())), f(g(f(x525,g(b()))), h(f(f(a(),a()),h(a())))) = f(a(),h(b())), f(g(f(x525,g(b()))),h(f(h(a()),f(a(),a())))) = f(a(),h(b())), f(g(f(g(b()),x525)),h(f(h(a()),f(a(),a())))) = f(a(),h(b())), f(g(f(g(b()),x525)), h(f(f(a(),a()),h(a())))) = f(a(),h(b())) We have to check termination of S: DP Processor: DPs: g#(g(a())) -> f#(a(),a()) g#(g(a())) -> g#(f(a(),a())) g#(g(a())) -> g#(c()) g#(g(a())) -> f#(g(c()),a()) g#(g(a())) -> f#(f(g(c()),a()),g(f(a(),a()))) g#(g(a())) -> c#() g#(g(a())) -> f#(c(),c()) g#(g(a())) -> g#(f(c(),c())) g#(g(a())) -> f#(h(g(f(c(),c()))),f(f(g(c()),a()),g(f(a(),a())))) c#() -> f#(a(),h(b())) f#(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) -> c#() f#(h(f(h(a()),f(a(),a()))),g(f(x,g(b())))) -> f#(h(b()),a()) f#(h(f(h(a()),f(a(),a()))),g(f(g(b()),x))) -> f#(h(b()),a()) f#(h(f(f(a(),a()),h(a()))),g(f(g(b()),x))) -> f#(h(b()),a()) f#(g(f(x519,g(b()))),h(f(f(a(),a()),h(a())))) -> f#(h(b()),a()) f#(g(f(x521,g(b()))),h(f(h(a()),f(a(),a())))) -> f#(a(),h(b())) f#(g(f(g(b()),x523)),h(f(h(a()),f(a(),a())))) -> f#(a(),h(b())) f#(g(f(g(b()),x525)),h(f(f(a(),a()),h(a())))) -> f#(a(),h(b())) TRS: g(g(a())) -> f(h(g(f(c(),c()))),f(f(g(c()),a()),g(f(a(),a())))) c() -> f(a(),h(b())) f(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) -> c() f(h(f(h(a()),f(a(),a()))),g(f(x,g(b())))) -> f(h(b()),a()) f(h(f(h(a()),f(a(),a()))),g(f(g(b()),x))) -> f(h(b()),a()) f(h(f(f(a(),a()),h(a()))),g(f(g(b()),x))) -> f(h(b()),a()) f(g(f(x519,g(b()))),h(f(f(a(),a()),h(a())))) -> f(h(b()),a()) f(g(f(x521,g(b()))),h(f(h(a()),f(a(),a())))) -> f(a(),h(b())) f(g(f(g(b()),x523)),h(f(h(a()),f(a(),a())))) -> f(a(),h(b())) f(g(f(g(b()),x525)),h(f(f(a(),a()),h(a())))) -> f(a(),h(b())) EDG Processor: DPs: g#(g(a())) -> f#(a(),a()) g#(g(a())) -> g#(f(a(),a())) g#(g(a())) -> g#(c()) g#(g(a())) -> f#(g(c()),a()) g#(g(a())) -> f#(f(g(c()),a()),g(f(a(),a()))) g#(g(a())) -> c#() g#(g(a())) -> f#(c(),c()) g#(g(a())) -> g#(f(c(),c())) g#(g(a())) -> f#(h(g(f(c(),c()))),f(f(g(c()),a()),g(f(a(),a())))) c#() -> f#(a(),h(b())) f#(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) -> c#() f#(h(f(h(a()),f(a(),a()))),g(f(x,g(b())))) -> f#(h(b()),a()) f#(h(f(h(a()),f(a(),a()))),g(f(g(b()),x))) -> f#(h(b()),a()) f#(h(f(f(a(),a()),h(a()))),g(f(g(b()),x))) -> f#(h(b()),a()) f#(g(f(x519,g(b()))),h(f(f(a(),a()),h(a())))) -> f#(h(b()),a()) f#(g(f(x521,g(b()))),h(f(h(a()),f(a(),a())))) -> f#(a(),h(b())) f#(g(f(g(b()),x523)),h(f(h(a()),f(a(),a())))) -> f#(a(),h(b())) f#(g(f(g(b()),x525)),h(f(f(a(),a()),h(a())))) -> f#(a(),h(b())) TRS: g(g(a())) -> f(h(g(f(c(),c()))),f(f(g(c()),a()),g(f(a(),a())))) c() -> f(a(),h(b())) f(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) -> c() f(h(f(h(a()),f(a(),a()))),g(f(x,g(b())))) -> f(h(b()),a()) f(h(f(h(a()),f(a(),a()))),g(f(g(b()),x))) -> f(h(b()),a()) f(h(f(f(a(),a()),h(a()))),g(f(g(b()),x))) -> f(h(b()),a()) f(g(f(x519,g(b()))),h(f(f(a(),a()),h(a())))) -> f(h(b()),a()) f(g(f(x521,g(b()))),h(f(h(a()),f(a(),a())))) -> f(a(),h(b())) f(g(f(g(b()),x523)),h(f(h(a()),f(a(),a())))) -> f(a(),h(b())) f(g(f(g(b()),x525)),h(f(f(a(),a()),h(a())))) -> f(a(),h(b())) graph: f#(h(f(f(a(),a()),h(a()))),g(f(x,g(b())))) -> c#() -> c#() -> f#(a(),h(b())) g#(g(a())) -> c#() -> c#() -> f#(a(),h(b())) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/324