YES Problem: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Proof: DP Processor: DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) EDG Processor: DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) graph: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 27/81 DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Bounds Processor: bound: 2 enrichment: match-dp automaton: final states: {6} transitions: f{#,1}(32,56) -> 4,6,5 f{#,1}(32,37) -> 6,4,5 f{#,1}(32,57) -> 4,6,5 a1() -> 32* f1(32,34) -> 81,35 f1(32,36) -> 37* f1(30,84) -> 34* f1(32,60) -> 77* f1(30,1) -> 31* f1(30,3) -> 31* f1(32,78) -> 79* f1(32,80) -> 81* f1(32,82) -> 83* f1(30,35) -> 36* f1(32,31) -> 33* f1(32,33) -> 80,34 f1(32,37) -> 84,52 f1(30,77) -> 37* f1(30,81) -> 82* f1(30,2) -> 31* f1(30,4) -> 31* f1(32,79) -> 80* f1(32,83) -> 84* f1(30,34) -> 78* f1(30,52) -> 33* b1() -> 30* f{#,2}(55,60) -> 4,5,6 f{#,0}(3,1) -> 4* f{#,0}(3,3) -> 4* f{#,0}(4,2) -> 4* f{#,0}(4,4) -> 4* f{#,0}(1,2) -> 4* f{#,0}(1,4) -> 4* f{#,0}(2,1) -> 4* f{#,0}(2,3) -> 4* f{#,0}(3,2) -> 6,4 f{#,0}(3,4) -> 4* f{#,0}(3,12) -> 6* f{#,0}(4,1) -> 4* f{#,0}(4,3) -> 4* f{#,0}(1,1) -> 4* f{#,0}(1,3) -> 4* f{#,0}(2,2) -> 4* f{#,0}(2,4) -> 4* a2() -> 55* a0() -> 3* f2(53,37) -> 54* f2(55,57) -> 58* f2(55,59) -> 60* f2(53,58) -> 59* f2(55,54) -> 56* f2(55,56) -> 57* f0(3,1) -> 2* f0(3,3) -> 2* f0(3,7) -> 8* f0(3,9) -> 10* f0(3,11) -> 12* f0(4,2) -> 2* f0(4,4) -> 2* f0(1,2) -> 2* f0(1,4) -> 2* f0(1,10) -> 11* f0(2,1) -> 2* f0(2,3) -> 2* f0(3,2) -> 10,9,2 f0(3,4) -> 2* f0(3,8) -> 9* f0(4,1) -> 2* f0(4,3) -> 2* f0(1,1) -> 2* f0(1,3) -> 2* f0(1,5) -> 7* f0(2,2) -> 2* f0(2,4) -> 2* b2() -> 53* b0() -> 1* 1 -> 5* 2 -> 5* 3 -> 5* 4 -> 5* problem: DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Bounds Processor: bound: 2 enrichment: match-dp automaton: final states: {6} transitions: f{#,1}(20,21) -> 6,4 f{#,1}(20,22) -> 6,4,5 f{#,1}(20,36) -> 4,5,6 a1() -> 20* f1(18,1) -> 19* f1(18,3) -> 19* f1(18,29) -> 30* f1(18,31) -> 42* f1(18,45) -> 46* f1(18,49) -> 50* f1(20,19) -> 21* f1(20,21) -> 37,22 f1(20,31) -> 52,32 f1(20,37) -> 49* f1(20,43) -> 44* f1(20,47) -> 48* f1(20,51) -> 52* f1(18,2) -> 19* f1(18,4) -> 19* f1(18,32) -> 21* f1(18,48) -> 31* f1(18,52) -> 22* f1(20,22) -> 49,29 f1(20,30) -> 31* f1(20,42) -> 43* f1(20,44) -> 45* f1(20,46) -> 47* f1(20,50) -> 51* b1() -> 18* f{#,2}(35,37) -> 4,5,6 f{#,2}(35,36) -> 6,4 f{#,0}(3,1) -> 4* f{#,0}(3,3) -> 4* f{#,0}(3,9) -> 6* f{#,0}(4,2) -> 4* f{#,0}(4,4) -> 4* f{#,0}(1,2) -> 4* f{#,0}(1,4) -> 4* f{#,0}(2,1) -> 4* f{#,0}(2,3) -> 4* f{#,0}(3,2) -> 4* f{#,0}(3,4) -> 4* f{#,0}(4,1) -> 4* f{#,0}(4,3) -> 4* f{#,0}(1,1) -> 4* f{#,0}(1,3) -> 4* f{#,0}(2,2) -> 4* f{#,0}(2,4) -> 4* a2() -> 35* a0() -> 3* f2(33,22) -> 34* f2(35,34) -> 36* f2(35,36) -> 37* f0(3,1) -> 2* f0(3,3) -> 2* f0(3,7) -> 8* f0(4,2) -> 2* f0(4,4) -> 2* f0(1,2) -> 2* f0(1,4) -> 2* f0(2,1) -> 2* f0(2,3) -> 2* f0(3,2) -> 9,2 f0(3,4) -> 2* f0(3,8) -> 9* f0(4,1) -> 2* f0(4,3) -> 2* f0(1,1) -> 2* f0(1,3) -> 2* f0(1,5) -> 7* f0(2,2) -> 2* f0(2,4) -> 2* b2() -> 33* b0() -> 1* 1 -> 5* 2 -> 5* 3 -> 5* 4 -> 5* problem: DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {5} transitions: f{#,1}(10,11) -> 5* a1() -> 10* f1(8,1) -> 9* f1(8,3) -> 9* f1(10,9) -> 11* f1(8,2) -> 9* b1() -> 8* f{#,0}(3,7) -> 5* a0() -> 3* f0(3,1) -> 2* f0(3,3) -> 2* f0(1,2) -> 2* f0(1,4) -> 6* f0(2,1) -> 2* f0(2,3) -> 2* f0(3,2) -> 2* f0(3,6) -> 7* f0(1,1) -> 2* f0(1,3) -> 2* f0(2,2) -> 2* b0() -> 1* 1 -> 4* 2 -> 4* 3 -> 4* problem: DPs: TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Qed