YES Problem: f(f(f(a(),b()),c()),x) -> f(b(),f(a(),f(c(),f(b(),x)))) f(x,f(y,z)) -> f(f(x,y),z) Proof: DP Processor: DPs: f#(f(f(a(),b()),c()),x) -> f#(b(),x) f#(f(f(a(),b()),c()),x) -> f#(c(),f(b(),x)) f#(f(f(a(),b()),c()),x) -> f#(a(),f(c(),f(b(),x))) f#(f(f(a(),b()),c()),x) -> f#(b(),f(a(),f(c(),f(b(),x)))) f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) TRS: f(f(f(a(),b()),c()),x) -> f(b(),f(a(),f(c(),f(b(),x)))) f(x,f(y,z)) -> f(f(x,y),z) EDG Processor: DPs: f#(f(f(a(),b()),c()),x) -> f#(b(),x) f#(f(f(a(),b()),c()),x) -> f#(c(),f(b(),x)) f#(f(f(a(),b()),c()),x) -> f#(a(),f(c(),f(b(),x))) f#(f(f(a(),b()),c()),x) -> f#(b(),f(a(),f(c(),f(b(),x)))) f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) TRS: f(f(f(a(),b()),c()),x) -> f(b(),f(a(),f(c(),f(b(),x)))) f(x,f(y,z)) -> f(f(x,y),z) graph: f#(f(f(a(),b()),c()),x) -> f#(c(),f(b(),x)) -> f#(x,f(y,z)) -> f#(x,y) f#(f(f(a(),b()),c()),x) -> f#(c(),f(b(),x)) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(f(f(a(),b()),c()),x) -> f#(b(),f(a(),f(c(),f(b(),x)))) -> f#(x,f(y,z)) -> f#(x,y) f#(f(f(a(),b()),c()),x) -> f#(b(),f(a(),f(c(),f(b(),x)))) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(f(f(a(),b()),c()),x) -> f#(b(),x) -> f#(x,f(y,z)) -> f#(x,y) f#(f(f(a(),b()),c()),x) -> f#(b(),x) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(f(f(a(),b()),c()),x) -> f#(a(),f(c(),f(b(),x))) -> f#(x,f(y,z)) -> f#(x,y) f#(f(f(a(),b()),c()),x) -> f#(a(),f(c(),f(b(),x))) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(f(f(a(),b()),c()),x) -> f#(b(),x) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(f(f(a(),b()),c()),x) -> f#(c(),f(b(),x)) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(f(f(a(),b()),c()),x) -> f#(a(),f(c(),f(b(),x))) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(f(f(a(),b()),c()),x) -> f#(b(),f(a(),f(c(),f(b(),x)))) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(x,f(y,z)) -> f#(x,y) -> f#(f(f(a(),b()),c()),x) -> f#(b(),x) f#(x,f(y,z)) -> f#(x,y) -> f#(f(f(a(),b()),c()),x) -> f#(c(),f(b(),x)) f#(x,f(y,z)) -> f#(x,y) -> f#(f(f(a(),b()),c()),x) -> f#(a(),f(c(),f(b(),x))) f#(x,f(y,z)) -> f#(x,y) -> f#(f(f(a(),b()),c()),x) -> f#(b(),f(a(),f(c(),f(b(),x)))) f#(x,f(y,z)) -> f#(x,y) -> f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(x,y) -> f#(x,f(y,z)) -> f#(f(x,y),z) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0 + x1, [c] = 1, [f](x0, x1) = x0 + x1, [b] = 0, [a] = 1 orientation: f#(f(f(a(),b()),c()),x) = x + 2 >= x = f#(b(),x) f#(f(f(a(),b()),c()),x) = x + 2 >= x + 1 = f#(c(),f(b(),x)) f#(f(f(a(),b()),c()),x) = x + 2 >= x + 2 = f#(a(),f(c(),f(b(),x))) f#(f(f(a(),b()),c()),x) = x + 2 >= x + 2 = f#(b(),f(a(),f(c(),f(b(),x)))) f#(x,f(y,z)) = x + y + z >= x + y = f#(x,y) f#(x,f(y,z)) = x + y + z >= x + y + z = f#(f(x,y),z) f(f(f(a(),b()),c()),x) = x + 2 >= x + 2 = f(b(),f(a(),f(c(),f(b(),x)))) f(x,f(y,z)) = x + y + z >= x + y + z = f(f(x,y),z) problem: DPs: f#(f(f(a(),b()),c()),x) -> f#(a(),f(c(),f(b(),x))) f#(f(f(a(),b()),c()),x) -> f#(b(),f(a(),f(c(),f(b(),x)))) f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) TRS: f(f(f(a(),b()),c()),x) -> f(b(),f(a(),f(c(),f(b(),x)))) f(x,f(y,z)) -> f(f(x,y),z) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0, [c] = 0, [f](x0, x1) = x0, [b] = 0, [a] = 1 orientation: f#(f(f(a(),b()),c()),x) = 1 >= 1 = f#(a(),f(c(),f(b(),x))) f#(f(f(a(),b()),c()),x) = 1 >= 0 = f#(b(),f(a(),f(c(),f(b(),x)))) f#(x,f(y,z)) = x >= x = f#(x,y) f#(x,f(y,z)) = x >= x = f#(f(x,y),z) f(f(f(a(),b()),c()),x) = 1 >= 0 = f(b(),f(a(),f(c(),f(b(),x)))) f(x,f(y,z)) = x >= x = f(f(x,y),z) problem: DPs: f#(f(f(a(),b()),c()),x) -> f#(a(),f(c(),f(b(),x))) f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) TRS: f(f(f(a(),b()),c()),x) -> f(b(),f(a(),f(c(),f(b(),x)))) f(x,f(y,z)) -> f(f(x,y),z) Bounds Processor: bound: 3 enrichment: match automaton: final states: {13,11,9,8,1} transitions: f1(23,3) -> 24,30 f1(3,7) -> 32* f1(7,34) -> 26* f1(34,2) -> 34,6 f1(29,4) -> 30,11 f1(14,4) -> 12,26 f1(19,6) -> 30* f1(5,3) -> 34* f1(26,2) -> 26,12 f1(32,5) -> 23* f1(7,5) -> 14* f1(32,17) -> 30,24 f1(7,17) -> 26* f1(23,4) -> 11,13,10,30 f1(3,12) -> 30* f1(3,14) -> 29* f1(29,3) -> 30,24 f1(3,20) -> 30* f1(14,3) -> 20,26 f1(19,5) -> 29* f1(19,17) -> 30* f1(40,2) -> 11,13,10 f1(30,2) -> 30,11 f1(5,4) -> 34* f1(32,6) -> 30,11 f1(7,6) -> 26* f{#,1}(7,34) -> 1,9,8 f{#,1}(14,4) -> 1,9,8 f{#,1}(26,2) -> 1,9,8 f{#,1}(7,5) -> 1,9,8 f{#,1}(7,17) -> 1,9,8 f{#,1}(14,3) -> 1,9,8 f{#,1}(7,6) -> 1,9,8 f2(38,3) -> 40,30 f2(3,7) -> 44* f2(32,34) -> 43* f2(7,34) -> 37* f2(44,6) -> 40* f2(44,34) -> 40* f2(19,34) -> 40* f2(51,4) -> 43* f2(46,4) -> 26,37 f2(32,5) -> 51* f2(7,5) -> 46* f2(43,2) -> 43,30,11,13,10 f2(38,4) -> 40,30 f2(3,14) -> 38* f2(44,5) -> 38,29 f2(19,5) -> 38* f2(3,26) -> 40* f2(44,17) -> 40* f2(40,2) -> 40,30 f2(51,3) -> 43* f2(46,3) -> 26,37 f2(37,2) -> 37,26 f{#,2}(7,34) -> 1,9,8 f{#,2}(46,4) -> 1,9,8 f{#,2}(7,5) -> 1,9,8 f{#,2}(46,3) -> 1,9,8 f{#,2}(37,2) -> 1,9,8 f3(53,3) -> 49,40 f3(3,7) -> 55* f3(49,2) -> 49,40 f3(55,5) -> 53* f3(3,37) -> 49* f3(53,4) -> 49,40 f3(3,46) -> 53* f3(55,34) -> 49* f50() -> 2* f{#,0}(14,4) -> 1* f{#,0}(7,5) -> 1* f{#,0}(7,17) -> 1* f{#,0}(13,2) -> 9* f{#,0}(14,3) -> 1* f{#,0}(20,2) -> 1* f{#,0}(10,2) -> 9* f{#,0}(12,2) -> 1* f{#,0}(2,2) -> 8* f{#,0}(7,6) -> 1* a0() -> 7* f0(23,3) -> 24* f0(3,7) -> 19* f0(24,2) -> 11* f0(4,2) -> 4* f0(14,4) -> 12* f0(19,6) -> 11* f0(5,3) -> 17* f0(11,2) -> 11* f0(6,2) -> 6* f0(7,5) -> 14* f0(7,17) -> 20* f0(13,2) -> 13* f0(23,4) -> 11* f0(3,2) -> 4* f0(3,12) -> 11* f0(3,14) -> 23* f0(3,20) -> 24* f0(14,3) -> 20* f0(19,5) -> 23* f0(19,17) -> 24* f0(20,2) -> 12* f0(10,2) -> 13* f0(5,4) -> 6* f0(17,2) -> 6* f0(12,2) -> 12* f0(2,2) -> 10* f0(7,6) -> 12* c0() -> 5* b0() -> 3* 1 -> 8,9 9 -> 8* 11 -> 10,13 13 -> 10* problem: DPs: TRS: f(f(f(a(),b()),c()),x) -> f(b(),f(a(),f(c(),f(b(),x)))) f(x,f(y,z)) -> f(f(x,y),z) Qed