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: 1 enrichment: match-dp automaton: final states: {1} transitions: f{#,1}(37,42) -> 1* a1() -> 37* f1(37,36) -> 38* f1(37,38) -> 39* f1(37,39) -> 40* f1(37,41) -> 42* f1(35,10) -> 36* f1(35,40) -> 41* b1() -> 35* f40() -> 2* f{#,0}(5,39) -> 1* f{#,0}(5,10) -> 1* f{#,0}(5,38) -> 1* a0() -> 5* f0(5,56) -> 57* f0(5,60) -> 61* f0(3,7) -> 55* f0(5,7) -> 8* f0(3,47) -> 10* f0(5,9) -> 10* f0(3,61) -> 7* f0(5,55) -> 56* f0(5,57) -> 58* f0(5,59) -> 60* f0(3,2) -> 4* f0(3,8) -> 9* f0(3,24) -> 6* f0(5,4) -> 6* f0(5,6) -> 7* f0(5,10) -> 61,24 f0(3,58) -> 59* f0(5,42) -> 47* b0() -> 3* 7 -> 57* 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: 1 enrichment: match-dp automaton: final states: {1} transitions: f{#,1}(22,24) -> 1* f{#,1}(22,23) -> 1* a1() -> 22* f1(20,7) -> 21* f1(22,21) -> 23* f1(22,23) -> 24* b1() -> 20* f140() -> 2* f{#,0}(5,7) -> 1* f{#,0}(5,23) -> 1* f{#,0}(5,6) -> 1* a0() -> 5* f0(3,17) -> 6* f0(3,35) -> 16* f0(3,39) -> 7* f0(5,7) -> 14* f0(5,15) -> 16* f0(5,29) -> 30* f0(5,31) -> 32* f0(5,33) -> 34* f0(5,37) -> 38* f0(3,2) -> 4* f0(3,14) -> 15* f0(3,16) -> 29* f0(3,32) -> 33* f0(3,36) -> 37* f0(5,4) -> 6* f0(5,6) -> 7* f0(5,16) -> 39,17 f0(5,24) -> 36* f0(5,30) -> 31* f0(5,34) -> 35* f0(5,38) -> 39* b0() -> 3* 7 -> 24* 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: 0 enrichment: match-dp automaton: final states: {1} transitions: f{#,0}(5,6) -> 1* a0() -> 5* f0(3,2) -> 4* f0(5,4) -> 6* b0() -> 3* f160() -> 2* 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