YES Problem: f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x))) f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x))) Proof: DP Processor: DPs: f#(a(),f(b(),x)) -> f#(a(),x) f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) f#(b(),f(a(),x)) -> f#(b(),x) f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) TRS: f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x))) f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x))) EDG Processor: DPs: f#(a(),f(b(),x)) -> f#(a(),x) f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) f#(b(),f(a(),x)) -> f#(b(),x) f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) TRS: f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x))) f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x))) graph: f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) -> f#(b(),f(a(),x)) -> f#(b(),x) f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) -> f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) -> f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) -> f#(b(),f(a(),x)) -> f#(b(),x) f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) -> f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) -> f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) f#(b(),f(a(),x)) -> f#(b(),x) -> f#(b(),f(a(),x)) -> f#(b(),x) f#(b(),f(a(),x)) -> f#(b(),x) -> f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) f#(b(),f(a(),x)) -> f#(b(),x) -> f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(b(),x)) -> f#(a(),x) f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) -> f#(a(),f(b(),x)) -> f#(a(),x) f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) -> f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) -> f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(b(),x)) -> f#(a(),x) -> f#(a(),f(b(),x)) -> f#(a(),x) f#(a(),f(b(),x)) -> f#(a(),x) -> f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) f#(a(),f(b(),x)) -> f#(a(),x) -> f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) SCC Processor: #sccs: 2 #rules: 6 #arcs: 18/36 DPs: f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) f#(a(),f(b(),x)) -> f#(a(),x) TRS: f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x))) f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x))) Bounds Processor: bound: 0 enrichment: match automaton: final states: {9,8,7,6,1} transitions: f40() -> 2* f{#,0}(3,5) -> 1* f{#,0}(3,2) -> 7* f{#,0}(3,4) -> 6* a0() -> 3* f0(3,5) -> 8* f0(10,11) -> 12* f0(3,2) -> 4* f0(3,4) -> 5* f0(10,2) -> 11* f0(10,12) -> 9* b0() -> 10* 1 -> 7* 6 -> 7* 8 -> 4* 9 -> 11* problem: DPs: TRS: f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x))) f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x))) Qed DPs: f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) f#(b(),f(a(),x)) -> f#(b(),x) TRS: f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x))) f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x))) Bounds Processor: bound: 0 enrichment: match automaton: final states: {12,8,7,6,1} transitions: f100() -> 2* f{#,0}(3,5) -> 1* f{#,0}(3,2) -> 7* f{#,0}(3,4) -> 6* a0() -> 9* f0(3,5) -> 12* f0(9,2) -> 10* f0(9,10) -> 11* f0(3,2) -> 4* f0(3,4) -> 5* f0(9,11) -> 8* b0() -> 3* 1 -> 7* 6 -> 7* 8 -> 10* 12 -> 4* problem: DPs: TRS: f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x))) f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x))) Qed