YES Problem: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) Proof: DP Processor: DPs: g#(x,x) -> g#(a(),b()) g#(c(),g(c(),x)) -> g#(d(),x) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(d(),g(d(),x)) -> g#(e(),x) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(e(),g(e(),x)) -> g#(c(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) f#(g(x,y)) -> f#(x) f#(g(x,y)) -> f#(f(x)) f#(g(x,y)) -> g#(f(f(x)),a()) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) TDG Processor: DPs: g#(x,x) -> g#(a(),b()) g#(c(),g(c(),x)) -> g#(d(),x) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(d(),g(d(),x)) -> g#(e(),x) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(e(),g(e(),x)) -> g#(c(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) f#(g(x,y)) -> f#(x) f#(g(x,y)) -> f#(f(x)) f#(g(x,y)) -> g#(f(f(x)),a()) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) graph: f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> g#(y,g(f(f(x)),a())) f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> g#(f(f(x)),a()) f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> f#(f(x)) f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> f#(x) f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> g#(y,g(f(f(x)),a())) f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> g#(f(f(x)),a()) f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> f#(f(x)) f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> f#(x) f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(e(),g(e(),x)) -> g#(c(),x) f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(d(),g(d(),x)) -> g#(e(),x) f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(c(),g(c(),x)) -> g#(d(),x) f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(x,x) -> g#(a(),b()) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(e(),g(e(),x)) -> g#(c(),x) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(d(),g(d(),x)) -> g#(e(),x) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(c(),g(c(),x)) -> g#(d(),x) f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(x,x) -> g#(a(),b()) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(x,x) -> g#(a(),b()) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(x,x) -> g#(a(),b()) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(x,x) -> g#(a(),b()) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(x,x) -> g#(a(),b()) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(x,x) -> g#(a(),b()) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(x,x) -> g#(a(),b()) g#(x,x) -> g#(a(),b()) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(x,x) -> g#(a(),b()) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(x,x) -> g#(a(),b()) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(x,x) -> g#(a(),b()) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(x,x) -> g#(a(),b()) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(x,x) -> g#(a(),b()) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(x,x) -> g#(a(),b()) -> g#(x,x) -> g#(a(),b()) SCC Processor: #sccs: 2 #rules: 9 #arcs: 71/121 DPs: f#(g(x,y)) -> f#(f(x)) f#(g(x,y)) -> f#(x) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {1} transitions: f{#,1}(17) -> 1* f{#,1}(16) -> 1* f{#,1}(18) -> 1* f1(2) -> 17*,3,16 f1(6) -> 18*,2,16 f1(18) -> 17* f90() -> 2* f{#,0}(17) -> 1* f{#,0}(2) -> 1* f{#,0}(14) -> 1* f{#,0}(6) -> 1* f{#,0}(18) -> 1* f{#,0}(3) -> 1* f0(17) -> 7* f0(14) -> 7* f0(3) -> 7* g0(2,14) -> 3* g0(18,15) -> 3* g0(8,15) -> 7* g0(14,6) -> 15*,13,8 g0(14,8) -> 7* g0(14,14) -> 7* g0(15,15) -> 7* g0(11,14) -> 7* g0(2,15) -> 3* g0(18,8) -> 3* g0(3,6) -> 13* g0(8,8) -> 7* g0(18,14) -> 3* g0(8,14) -> 7* g0(14,15) -> 7* g0(15,8) -> 7* g0(15,14) -> 7* g0(6,11) -> 14*,13,7,8,3 g0(11,13) -> 7* g0(11,15) -> 7* g0(17,6) -> 13* g0(7,6) -> 8* g0(2,8) -> 3* a0() -> 6* b0() -> 11* problem: DPs: f#(g(x,y)) -> f#(x) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: f210() -> 2* f{#,0}(2) -> 1* problem: DPs: TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) Qed DPs: g#(x,x) -> g#(a(),b()) g#(c(),g(c(),x)) -> g#(d(),x) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(d(),g(d(),x)) -> g#(e(),x) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(e(),g(e(),x)) -> g#(c(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) EDG Processor: DPs: g#(x,x) -> g#(a(),b()) g#(c(),g(c(),x)) -> g#(d(),x) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(d(),g(d(),x)) -> g#(e(),x) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(e(),g(e(),x)) -> g#(c(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) graph: g#(d(),g(d(),x)) -> g#(e(),x) -> g#(x,x) -> g#(a(),b()) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(d(),g(d(),x)) -> g#(e(),x) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(x,x) -> g#(a(),b()) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(x,x) -> g#(a(),b()) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(x,x) -> g#(a(),b()) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(c(),g(c(),x)) -> g#(d(),x) g#(e(),g(e(),x)) -> g#(c(),x) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(x,x) -> g#(a(),b()) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(d(),g(d(),x)) -> g#(e(),x) g#(c(),g(c(),x)) -> g#(d(),x) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(x,x) -> g#(a(),b()) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(e(),g(e(),x)) -> g#(c(),x) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) SCC Processor: #sccs: 1 #rules: 6 #arcs: 18/49 DPs: g#(d(),g(d(),x)) -> g#(e(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(e(),g(e(),x)) -> g#(c(),x) g#(c(),g(c(),x)) -> g#(d(),x) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) Usable Rule Processor: DPs: g#(d(),g(d(),x)) -> g#(e(),x) g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) g#(e(),g(e(),x)) -> g#(c(),x) g#(c(),g(c(),x)) -> g#(d(),x) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) Arctic Interpretation Processor: dimension: 1 usable rules: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) interpretation: [g#](x0, x1) = x1, [d] = 1, [e] = 0, [c] = 1, [b] = 0, [a] = 1, [g](x0, x1) = x0 + 1x1 + 1 orientation: g#(d(),g(d(),x)) = 1x + 1 >= x = g#(e(),x) g#(e(),g(e(),x)) = 1x + 1 >= 1x + 1 = g#(d(),g(c(),x)) g#(d(),g(d(),x)) = 1x + 1 >= 1x + 1 = g#(c(),g(e(),x)) g#(c(),g(c(),x)) = 1x + 1 >= 1x + 1 = g#(e(),g(d(),x)) g#(e(),g(e(),x)) = 1x + 1 >= x = g#(c(),x) g#(c(),g(c(),x)) = 1x + 1 >= x = g#(d(),x) g(x,x) = 1x + 1 >= 1 = g(a(),b()) g(c(),g(c(),x)) = 2x + 2 >= 2x + 2 = g(e(),g(d(),x)) g(e(),g(e(),x)) = 2x + 2 >= 2x + 2 = g(d(),g(c(),x)) g(d(),g(d(),x)) = 2x + 2 >= 2x + 2 = g(c(),g(e(),x)) problem: DPs: g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) Restore Modifier: DPs: g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {9,6,1} transitions: d0() -> 5* c0() -> 3* e0() -> 7* f230() -> 2* g{#,0}(7,10) -> 9* g{#,0}(7,14) -> 9* g{#,0}(3,8) -> 6* g{#,0}(3,14) -> 6* g{#,0}(5,4) -> 1* g{#,0}(5,14) -> 1* g0(7,14) -> 4* g0(12,11) -> 14*,4,8,10 g0(3,2) -> 4* g0(3,8) -> 10* g0(3,14) -> 10* g0(5,2) -> 10* g0(5,4) -> 8* g0(5,14) -> 8* g0(7,2) -> 8* g0(7,10) -> 4* a0() -> 12* b0() -> 11* problem: DPs: TRS: g(x,x) -> g(a(),b()) g(c(),g(c(),x)) -> g(e(),g(d(),x)) g(d(),g(d(),x)) -> g(c(),g(e(),x)) g(e(),g(e(),x)) -> g(d(),g(c(),x)) f(g(x,y)) -> g(y,g(f(f(x)),a())) Qed