YES Problem: a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x)))) a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x)))) Proof: DP Processor: DPs: a#(f(),a(g(),a(f(),x))) -> a#(g(),a(g(),a(f(),x))) a#(f(),a(g(),a(f(),x))) -> a#(f(),a(g(),a(g(),a(f(),x)))) a#(g(),a(f(),a(g(),x))) -> a#(f(),a(f(),a(g(),x))) a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) TRS: a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x)))) a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x)))) EDG Processor: DPs: a#(f(),a(g(),a(f(),x))) -> a#(g(),a(g(),a(f(),x))) a#(f(),a(g(),a(f(),x))) -> a#(f(),a(g(),a(g(),a(f(),x)))) a#(g(),a(f(),a(g(),x))) -> a#(f(),a(f(),a(g(),x))) a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) TRS: a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x)))) a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x)))) graph: a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) -> a#(g(),a(f(),a(g(),x))) -> a#(f(),a(f(),a(g(),x))) a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) -> a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) a#(g(),a(f(),a(g(),x))) -> a#(f(),a(f(),a(g(),x))) -> a#(f(),a(g(),a(f(),x))) -> a#(g(),a(g(),a(f(),x))) a#(g(),a(f(),a(g(),x))) -> a#(f(),a(f(),a(g(),x))) -> a#(f(),a(g(),a(f(),x))) -> a#(f(),a(g(),a(g(),a(f(),x)))) a#(f(),a(g(),a(f(),x))) -> a#(g(),a(g(),a(f(),x))) -> a#(g(),a(f(),a(g(),x))) -> a#(f(),a(f(),a(g(),x))) a#(f(),a(g(),a(f(),x))) -> a#(g(),a(g(),a(f(),x))) -> a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) a#(f(),a(g(),a(f(),x))) -> a#(f(),a(g(),a(g(),a(f(),x)))) -> a#(f(),a(g(),a(f(),x))) -> a#(g(),a(g(),a(f(),x))) a#(f(),a(g(),a(f(),x))) -> a#(f(),a(g(),a(g(),a(f(),x)))) -> a#(f(),a(g(),a(f(),x))) -> a#(f(),a(g(),a(g(),a(f(),x)))) Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {6} transitions: a{#,1}(37,38) -> 4,5 g1() -> 37* a1(37,36) -> 38* a1(37,38) -> 1* a1(35,1) -> 1,36 a1(35,3) -> 36* a1(37,1) -> 55,38 a1(37,3) -> 38* a1(35,55) -> 1* a1(35,2) -> 36* a1(35,4) -> 36* a1(35,38) -> 1* a1(37,2) -> 55* a1(37,4) -> 55* f1() -> 35* a{#,0}(3,1) -> 4* a{#,0}(3,3) -> 4* a{#,0}(4,2) -> 4* a{#,0}(4,4) -> 4* a{#,0}(1,2) -> 4* a{#,0}(1,4) -> 4* a{#,0}(1,8) -> 6* a{#,0}(2,1) -> 4* a{#,0}(2,3) -> 4* a{#,0}(3,2) -> 4* a{#,0}(3,4) -> 4* a{#,0}(4,1) -> 4* a{#,0}(4,3) -> 4* a{#,0}(1,1) -> 4* a{#,0}(1,3) -> 4* a{#,0}(2,2) -> 4* a{#,0}(2,4) -> 4* f0() -> 3* a0(3,1) -> 2* a0(3,3) -> 2* a0(3,5) -> 7* a0(4,2) -> 2* a0(4,4) -> 2* a0(1,2) -> 2* a0(1,4) -> 2* a0(2,1) -> 2* a0(2,3) -> 2* a0(3,2) -> 2* a0(3,4) -> 2* a0(4,1) -> 2* a0(4,3) -> 2* a0(1,1) -> 2* a0(1,3) -> 2* a0(1,7) -> 8* a0(2,2) -> 2* a0(2,4) -> 2* g0() -> 1* 1 -> 5* 2 -> 5* 3 -> 5* 4 -> 5* problem: DPs: a#(f(),a(g(),a(f(),x))) -> a#(f(),a(g(),a(g(),a(f(),x)))) a#(g(),a(f(),a(g(),x))) -> a#(f(),a(f(),a(g(),x))) a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) TRS: a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x)))) a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x)))) Matrix Interpretation Processor: dimension: 1 interpretation: [a#](x0, x1) = x0 + 1, [a](x0, x1) = 0, [g] = 1, [f] = 0 orientation: a#(f(),a(g(),a(f(),x))) = 1 >= 1 = a#(f(),a(g(),a(g(),a(f(),x)))) a#(g(),a(f(),a(g(),x))) = 2 >= 1 = a#(f(),a(f(),a(g(),x))) a#(g(),a(f(),a(g(),x))) = 2 >= 2 = a#(g(),a(f(),a(f(),a(g(),x)))) a(f(),a(g(),a(f(),x))) = 0 >= 0 = a(f(),a(g(),a(g(),a(f(),x)))) a(g(),a(f(),a(g(),x))) = 0 >= 0 = a(g(),a(f(),a(f(),a(g(),x)))) problem: DPs: a#(f(),a(g(),a(f(),x))) -> a#(f(),a(g(),a(g(),a(f(),x)))) a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) TRS: a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x)))) a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x)))) Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {6} transitions: a{#,1}(19,23) -> 4,5 g1() -> 21* a1(19,2) -> 20* a1(19,4) -> 20* a1(19,22) -> 1* a1(19,30) -> 1* a1(21,2) -> 30* a1(21,4) -> 30* a1(21,20) -> 30,22 a1(21,22) -> 23* a1(19,1) -> 20* a1(19,3) -> 20* a1(19,23) -> 1,20 a1(21,1) -> 22* a1(21,3) -> 22* f1() -> 19* a{#,0}(3,1) -> 4* a{#,0}(3,3) -> 4* a{#,0}(3,9) -> 6* a{#,0}(4,2) -> 4* a{#,0}(4,4) -> 4* a{#,0}(1,2) -> 4* a{#,0}(1,4) -> 4* a{#,0}(2,1) -> 4* a{#,0}(2,3) -> 4* a{#,0}(3,2) -> 4* a{#,0}(3,4) -> 4* a{#,0}(4,1) -> 4* a{#,0}(4,3) -> 4* a{#,0}(1,1) -> 4* a{#,0}(1,3) -> 4* a{#,0}(2,2) -> 4* a{#,0}(2,4) -> 4* f0() -> 3* a0(3,1) -> 2* a0(3,3) -> 2* a0(3,5) -> 7* a0(4,2) -> 2* a0(4,4) -> 2* a0(1,2) -> 2* a0(1,4) -> 2* a0(1,8) -> 9* a0(2,1) -> 2* a0(2,3) -> 2* a0(3,2) -> 2* a0(3,4) -> 2* a0(4,1) -> 2* a0(4,3) -> 2* a0(1,1) -> 2* a0(1,3) -> 2* a0(1,7) -> 8* a0(2,2) -> 2* a0(2,4) -> 2* g0() -> 1* 1 -> 5* 2 -> 5* 3 -> 5* 4 -> 5* problem: DPs: a#(g(),a(f(),a(g(),x))) -> a#(g(),a(f(),a(f(),a(g(),x)))) TRS: a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x)))) a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x)))) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {5} transitions: a{#,0}(3,8) -> 5* f0() -> 1* a0(3,1) -> 2* a0(3,3) -> 2* a0(1,2) -> 2* a0(1,6) -> 7* a0(2,1) -> 2* a0(2,3) -> 2* a0(3,2) -> 2* a0(3,4) -> 6* a0(1,1) -> 2* a0(1,3) -> 2* a0(1,7) -> 8* a0(2,2) -> 2* g0() -> 3* 1 -> 4* 2 -> 4* 3 -> 4* problem: DPs: TRS: a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x)))) a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x)))) Qed