YES Problem: f(b(a(),z)) -> z b(y,b(a(),z)) -> b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) -> b(f(x),z) Proof: DP Processor: DPs: b#(y,b(a(),z)) -> f#(z) b#(y,b(a(),z)) -> b#(f(z),a()) b#(y,b(a(),z)) -> f#(c(y,y,a())) b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) f#(f(f(c(z,x,a())))) -> f#(x) f#(f(f(c(z,x,a())))) -> b#(f(x),z) TRS: f(b(a(),z)) -> z b(y,b(a(),z)) -> b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) -> b(f(x),z) EDG Processor: DPs: b#(y,b(a(),z)) -> f#(z) b#(y,b(a(),z)) -> b#(f(z),a()) b#(y,b(a(),z)) -> f#(c(y,y,a())) b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) f#(f(f(c(z,x,a())))) -> f#(x) f#(f(f(c(z,x,a())))) -> b#(f(x),z) TRS: f(b(a(),z)) -> z b(y,b(a(),z)) -> b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) -> b(f(x),z) graph: b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) -> b#(y,b(a(),z)) -> f#(z) b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) -> b#(y,b(a(),z)) -> b#(f(z),a()) b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) -> b#(y,b(a(),z)) -> f#(c(y,y,a())) b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) -> b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) b#(y,b(a(),z)) -> f#(z) -> f#(f(f(c(z,x,a())))) -> f#(x) b#(y,b(a(),z)) -> f#(z) -> f#(f(f(c(z,x,a())))) -> b#(f(x),z) f#(f(f(c(z,x,a())))) -> b#(f(x),z) -> b#(y,b(a(),z)) -> f#(z) f#(f(f(c(z,x,a())))) -> b#(f(x),z) -> b#(y,b(a(),z)) -> b#(f(z),a()) f#(f(f(c(z,x,a())))) -> b#(f(x),z) -> b#(y,b(a(),z)) -> f#(c(y,y,a())) f#(f(f(c(z,x,a())))) -> b#(f(x),z) -> b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) f#(f(f(c(z,x,a())))) -> f#(x) -> f#(f(f(c(z,x,a())))) -> f#(x) f#(f(f(c(z,x,a())))) -> f#(x) -> f#(f(f(c(z,x,a())))) -> b#(f(x),z) SCC Processor: #sccs: 1 #rules: 4 #arcs: 12/36 DPs: b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) b#(y,b(a(),z)) -> f#(z) f#(f(f(c(z,x,a())))) -> b#(f(x),z) f#(f(f(c(z,x,a())))) -> f#(x) TRS: f(b(a(),z)) -> z b(y,b(a(),z)) -> b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) -> b(f(x),z) Matrix Interpretation Processor: dimension: 1 interpretation: [b#](x0, x1) = x1 + 1, [f#](x0) = x0 + 1, [c](x0, x1, x2) = x0 + x1 + 1, [f](x0) = x0, [b](x0, x1) = x1, [a] = 0 orientation: b#(y,b(a(),z)) = z + 1 >= 1 = b#(f(c(y,y,a())),b(f(z),a())) b#(y,b(a(),z)) = z + 1 >= z + 1 = f#(z) f#(f(f(c(z,x,a())))) = x + z + 2 >= z + 1 = b#(f(x),z) f#(f(f(c(z,x,a())))) = x + z + 2 >= x + 1 = f#(x) f(b(a(),z)) = z >= z = z b(y,b(a(),z)) = z >= 0 = b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) = x + z + 1 >= z = b(f(x),z) problem: DPs: b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) b#(y,b(a(),z)) -> f#(z) TRS: f(b(a(),z)) -> z b(y,b(a(),z)) -> b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) -> b(f(x),z) Matrix Interpretation Processor: dimension: 1 interpretation: [b#](x0, x1) = 1, [f#](x0) = 0, [c](x0, x1, x2) = x0, [f](x0) = x0, [b](x0, x1) = x1, [a] = 0 orientation: b#(y,b(a(),z)) = 1 >= 1 = b#(f(c(y,y,a())),b(f(z),a())) b#(y,b(a(),z)) = 1 >= 0 = f#(z) f(b(a(),z)) = z >= z = z b(y,b(a(),z)) = z >= 0 = b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) = z >= z = b(f(x),z) problem: DPs: b#(y,b(a(),z)) -> b#(f(c(y,y,a())),b(f(z),a())) TRS: f(b(a(),z)) -> z b(y,b(a(),z)) -> b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) -> b(f(x),z) Bounds Processor: bound: 1 enrichment: top-dp automaton: final states: {6} transitions: c0(14,16,15) -> 14* c0(18,12,14) -> 14* c0(14,18,15) -> 14* c0(18,14,14) -> 14* c0(18,16,14) -> 14* c0(15,11,18) -> 14* c0(18,18,14) -> 14* c0(14,12,12) -> 16* c0(14,14,12) -> 16* c0(15,15,18) -> 14* c0(16,11,16) -> 14* c0(14,11,17) -> 14* c0(14,16,12) -> 16* c0(18,12,11) -> 14* c0(15,17,18) -> 14* c0(11,11,16) -> 14* c0(14,18,12) -> 16* c0(18,14,11) -> 14* c0(16,15,16) -> 14* c0(14,15,17) -> 14* c0(18,16,11) -> 14* c0(11,15,16) -> 14* c0(15,11,15) -> 14* c0(16,17,16) -> 14* c0(14,17,17) -> 14* c0(18,18,11) -> 14* c0(11,17,16) -> 14* c0(15,15,15) -> 14* c0(14,11,14) -> 14* c0(15,17,15) -> 14* c0(14,15,14) -> 14* c0(15,11,12) -> 16* c0(16,12,18) -> 14* c0(14,17,14) -> 14* c0(11,12,18) -> 14* c0(16,14,18) -> 14* c0(11,14,18) -> 14* c0(15,15,12) -> 16* c0(16,16,18) -> 14* c0(14,11,11) -> 14* c0(11,16,18) -> 14* c0(17,12,16) -> 14* c0(15,12,17) -> 14* c0(15,17,12) -> 16* c0(16,18,18) -> 14* c0(12,12,16) -> 14* c0(17,14,16) -> 14* c0(11,18,18) -> 14* c0(15,14,17) -> 14* c0(12,14,16) -> 14* c0(14,15,11) -> 14* c0(17,16,16) -> 14* c0(15,16,17) -> 14* c0(12,16,16) -> 14* c0(16,12,15) -> 14* c0(14,17,11) -> 14* c0(17,18,16) -> 14* c0(15,18,17) -> 14* c0(11,12,15) -> 14* c0(12,18,16) -> 14* c0(16,14,15) -> 14* c0(11,14,15) -> 14* c0(16,16,15) -> 14* c0(11,16,15) -> 14* c0(15,12,14) -> 14* c0(16,18,15) -> 14* c0(11,18,15) -> 14* c0(15,14,14) -> 14* c0(17,11,18) -> 14* c0(15,16,14) -> 14* c0(12,11,18) -> 14* c0(16,12,12) -> 16* c0(15,18,14) -> 14* c0(11,12,12) -> 16* c0(16,14,12) -> 16* c0(17,15,18) -> 14* c0(11,14,12) -> 16* c0(12,15,18) -> 14* c0(18,11,16) -> 14* c0(16,11,17) -> 14* c0(16,16,12) -> 16* c0(17,17,18) -> 14* c0(11,11,17) -> 14* c0(11,16,12) -> 16* c0(15,12,11) -> 14* c0(12,17,18) -> 14* c0(16,18,12) -> 16* c0(11,18,12) -> 16* c0(15,14,11) -> 14* c0(18,15,16) -> 14* c0(16,15,17) -> 14* c0(11,15,17) -> 14* c0(17,11,15) -> 14* c0(15,16,11) -> 14* c0(18,17,16) -> 14* c0(16,17,17) -> 14* c0(12,11,15) -> 14* c0(11,17,17) -> 14* c0(15,18,11) -> 14* c0(17,15,15) -> 14* c0(12,15,15) -> 14* c0(16,11,14) -> 14* c0(17,17,15) -> 14* c0(11,11,14) -> 14* c0(12,17,15) -> 14* c0(16,15,14) -> 14* c0(17,11,12) -> 16* c0(11,15,14) -> 14* c0(18,12,18) -> 14* c0(16,17,14) -> 14* c0(12,11,12) -> 16* c0(11,17,14) -> 14* c0(18,14,18) -> 14* c0(17,15,12) -> 16* c0(18,16,18) -> 14* c0(12,15,12) -> 16* c0(16,11,11) -> 14* c0(17,12,17) -> 14* c0(17,17,12) -> 16* c0(11,11,11) -> 14* c0(18,18,18) -> 14* c0(14,12,16) -> 14* c0(12,12,17) -> 14* c0(12,17,12) -> 16* c0(17,14,17) -> 14* c0(14,14,16) -> 14* c0(12,14,17) -> 14* c0(16,15,11) -> 14* c0(17,16,17) -> 14* c0(11,15,11) -> 14* c0(14,16,16) -> 14* c0(12,16,17) -> 14* c0(18,12,15) -> 14* c0(16,17,11) -> 14* c0(17,18,17) -> 14* c0(11,17,11) -> 14* c0(14,18,16) -> 14* c0(18,14,15) -> 14* c0(12,18,17) -> 14* c0(18,16,15) -> 14* c0(17,12,14) -> 14* c0(18,18,15) -> 14* c0(12,12,14) -> 14* c0(17,14,14) -> 14* c0(12,14,14) -> 14* c0(17,16,14) -> 14* c0(14,11,18) -> 14* c0(18,12,12) -> 16* c0(12,16,14) -> 14* c0(17,18,14) -> 14* c0(18,14,12) -> 16* c0(12,18,14) -> 14* c0(14,15,18) -> 14* c0(18,11,17) -> 14* c0(18,16,12) -> 16* c0(15,11,16) -> 14* c0(17,12,11) -> 14* c0(14,17,18) -> 14* c0(18,18,12) -> 16* c0(12,12,11) -> 14* c0(17,14,11) -> 14* c0(18,15,17) -> 14* c0(12,14,11) -> 14* c0(15,15,16) -> 14* c0(17,16,11) -> 14* c0(18,17,17) -> 14* c0(14,11,15) -> 14* c0(12,16,11) -> 14* c0(15,17,16) -> 14* c0(17,18,11) -> 14* c0(12,18,11) -> 14* c0(14,15,15) -> 14* c0(18,11,14) -> 14* c0(14,17,15) -> 14* c0(18,15,14) -> 14* c0(18,17,14) -> 14* c0(14,11,12) -> 16* c0(15,12,18) -> 14* c0(15,14,18) -> 14* c0(14,15,12) -> 16* c0(18,11,11) -> 14* c0(15,16,18) -> 14* c0(16,12,16) -> 14* c0(14,12,17) -> 14* c0(14,17,12) -> 16* c0(15,18,18) -> 14* c0(11,12,16) -> 14* c0(16,14,16) -> 14* c0(14,14,17) -> 14* c0(18,15,11) -> 14* c0(11,14,16) -> 14* c0(16,16,16) -> 14* c0(14,16,17) -> 14* c0(18,17,11) -> 14* c0(11,16,16) -> 14* c0(15,12,15) -> 14* c0(16,18,16) -> 14* c0(14,18,17) -> 14* c0(11,18,16) -> 14* c0(15,14,15) -> 14* c0(15,16,15) -> 14* c0(14,12,14) -> 14* c0(15,18,15) -> 14* c0(14,14,14) -> 14* c0(16,11,18) -> 14* c0(14,16,14) -> 14* c0(11,11,18) -> 14* c0(15,12,12) -> 16* c0(14,18,14) -> 14* c0(15,14,12) -> 16* c0(16,15,18) -> 14* c0(17,11,16) -> 14* c0(11,15,18) -> 14* c0(15,11,17) -> 14* c0(15,16,12) -> 16* c0(16,17,18) -> 14* c0(12,11,16) -> 14* c0(14,12,11) -> 14* c0(11,17,18) -> 14* c0(15,18,12) -> 16* c0(14,14,11) -> 14* c0(17,15,16) -> 14* c0(15,15,17) -> 14* c0(12,15,16) -> 14* c0(16,11,15) -> 14* c0(14,16,11) -> 14* c0(17,17,16) -> 14* c0(15,17,17) -> 14* c0(11,11,15) -> 14* c0(12,17,16) -> 14* c0(14,18,11) -> 14* c0(16,15,15) -> 14* c0(11,15,15) -> 14* c0(15,11,14) -> 14* c0(16,17,15) -> 14* c0(11,17,15) -> 14* c0(15,15,14) -> 14* c0(16,11,12) -> 16* c0(17,12,18) -> 14* c0(15,17,14) -> 14* c0(11,11,12) -> 16* c0(12,12,18) -> 14* c0(17,14,18) -> 14* c0(12,14,18) -> 14* c0(16,15,12) -> 16* c0(17,16,18) -> 14* c0(11,15,12) -> 16* c0(15,11,11) -> 14* c0(12,16,18) -> 14* c0(18,12,16) -> 14* c0(16,12,17) -> 14* c0(16,17,12) -> 16* c0(17,18,18) -> 14* c0(11,12,17) -> 14* c0(11,17,12) -> 16* c0(12,18,18) -> 14* c0(18,14,16) -> 14* c0(16,14,17) -> 14* c0(11,14,17) -> 14* c0(15,15,11) -> 14* c0(18,16,16) -> 14* c0(16,16,17) -> 14* c0(17,12,15) -> 14* c0(11,16,17) -> 14* c0(15,17,11) -> 14* c0(18,18,16) -> 14* c0(16,18,17) -> 14* c0(12,12,15) -> 14* c0(17,14,15) -> 14* c0(11,18,17) -> 14* c0(12,14,15) -> 14* c0(17,16,15) -> 14* c0(12,16,15) -> 14* c0(16,12,14) -> 14* c0(17,18,15) -> 14* c0(11,12,14) -> 14* c0(12,18,15) -> 14* c0(16,14,14) -> 14* c0(11,14,14) -> 14* c0(18,11,18) -> 14* c0(16,16,14) -> 14* c0(17,12,12) -> 16* c0(11,16,14) -> 14* c0(16,18,14) -> 14* c0(12,12,12) -> 16* c0(17,14,12) -> 16* c0(11,18,14) -> 14* c0(18,15,18) -> 14* c0(12,14,12) -> 16* c0(17,11,17) -> 14* c0(17,16,12) -> 16* c0(18,17,18) -> 14* c0(14,11,16) -> 14* c0(12,11,17) -> 14* c0(12,16,12) -> 16* c0(16,12,11) -> 14* c0(17,18,12) -> 16* c0(11,12,11) -> 14* c0(12,18,12) -> 16* c0(16,14,11) -> 14* c0(17,15,17) -> 14* c0(11,14,11) -> 14* c0(14,15,16) -> 14* c0(18,11,15) -> 14* c0(12,15,17) -> 14* c0(16,16,11) -> 14* c0(17,17,17) -> 14* c0(11,16,11) -> 14* c0(14,17,16) -> 14* c0(12,17,17) -> 14* c0(16,18,11) -> 14* c0(11,18,11) -> 14* c0(18,15,15) -> 14* c0(17,11,14) -> 14* c0(18,17,15) -> 14* c0(12,11,14) -> 14* c0(17,15,14) -> 14* c0(18,11,12) -> 16* c0(12,15,14) -> 14* c0(17,17,14) -> 14* c0(14,12,18) -> 14* c0(12,17,14) -> 14* c0(14,14,18) -> 14* c0(18,15,12) -> 16* c0(17,11,11) -> 14* c0(14,16,18) -> 14* c0(18,12,17) -> 14* c0(18,17,12) -> 16* c0(12,11,11) -> 14* c0(15,12,16) -> 14* c0(14,18,18) -> 14* c0(18,14,17) -> 14* c0(15,14,16) -> 14* c0(17,15,11) -> 14* c0(18,16,17) -> 14* c0(12,15,11) -> 14* c0(15,16,16) -> 14* c0(17,17,11) -> 14* c0(18,18,17) -> 14* c0(14,12,15) -> 14* c0(12,17,11) -> 14* c0(15,18,16) -> 14* c0(14,14,15) -> 14* b{#,1}(23,21) -> 6* f1(22) -> 23* f1(12) -> 20* c1(18,18,19) -> 22* a1() -> 19* b1(20,19) -> 21* b{#,0}(18,17) -> 6* b0(12,14) -> 11* b0(17,16) -> 11* b0(12,16) -> 11* b0(17,18) -> 11* b0(12,18) -> 11* b0(18,11) -> 11* b0(18,15) -> 11* b0(18,17) -> 11* b0(14,12) -> 11* b0(14,14) -> 11* b0(14,16) -> 11* b0(14,18) -> 11* b0(15,11) -> 11* b0(15,15) -> 11* b0(15,17) -> 11* b0(16,12) -> 11* b0(11,12) -> 11* b0(16,14) -> 11* b0(11,14) -> 11* b0(16,16) -> 11* b0(11,16) -> 11* b0(16,18) -> 11* b0(11,18) -> 11* b0(17,11) -> 11* b0(12,11) -> 11* b0(17,15) -> 11* b0(12,15) -> 11* b0(17,17) -> 11* b0(12,17) -> 11* b0(18,12) -> 17* b0(18,14) -> 11* b0(18,16) -> 11* b0(18,18) -> 11* b0(14,11) -> 11* b0(14,15) -> 11* b0(14,17) -> 11* b0(15,12) -> 17* b0(15,14) -> 11* b0(15,16) -> 11* b0(15,18) -> 11* b0(16,11) -> 11* b0(11,11) -> 11* b0(16,15) -> 11* b0(11,15) -> 11* b0(16,17) -> 11* b0(11,17) -> 11* b0(17,12) -> 11* b0(12,12) -> 11* b0(17,14) -> 11* a0() -> 12* f0(15) -> 15* f0(17) -> 15* f0(12) -> 15* f0(14) -> 15* f0(16) -> 18* f0(11) -> 15* f0(18) -> 15* 11 -> 15* 12 -> 15* 14 -> 15* 16 -> 15* 17 -> 15* 18 -> 15* problem: DPs: TRS: f(b(a(),z)) -> z b(y,b(a(),z)) -> b(f(c(y,y,a())),b(f(z),a())) f(f(f(c(z,x,a())))) -> b(f(x),z) Qed