YES Problem: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) Proof: DP Processor: DPs: b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) c#(f(c(a(),y,a())),x,z) -> b#(x,a()) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) c#(f(c(a(),y,a())),x,z) -> b#(z,z) c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) TRS: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) TDG Processor: DPs: b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) c#(f(c(a(),y,a())),x,z) -> b#(x,a()) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) c#(f(c(a(),y,a())),x,z) -> b#(z,z) c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) TRS: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) graph: f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) -> f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) -> f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) -> f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> b#(z,z) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> b#(x,a()) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) -> f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) -> f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) -> f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) -> f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) -> f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) -> f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) c#(f(c(a(),y,a())),x,z) -> b#(z,z) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) c#(f(c(a(),y,a())),x,z) -> b#(z,z) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) c#(f(c(a(),y,a())),x,z) -> b#(z,z) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) c#(f(c(a(),y,a())),x,z) -> b#(x,a()) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) c#(f(c(a(),y,a())),x,z) -> b#(x,a()) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) c#(f(c(a(),y,a())),x,z) -> b#(x,a()) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> b#(z,z) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> b#(x,a()) b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) EDG Processor: DPs: b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) c#(f(c(a(),y,a())),x,z) -> b#(x,a()) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) c#(f(c(a(),y,a())),x,z) -> b#(z,z) c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) TRS: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) graph: f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) -> f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) -> f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) -> f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> b#(x,a()) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> b#(z,z) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) -> c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) -> b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) -> b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a())) c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) -> b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> b#(x,a()) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a()))) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> b#(z,z) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a())))) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) -> c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a()))))) SCC Processor: #sccs: 2 #rules: 3 #arcs: 21/144 DPs: f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) TRS: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) Matrix Interpretation Processor: dim=2 usable rules: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) interpretation: [f#](x0) = [2 0]x0 + [1], [0] [f](x0) = [0], [0 0] [0 2] [b](x0, x1) = [0 1]x0 + [0 2]x1, [0 0] [0 1] [0 2] [c](x0, x1, x2) = [1 2]x0 + [1 1]x1 + [1 2]x2, [0] [a] = [1] orientation: f#(c(a(),b(b(z,a()),y),x)) = [0 4]x + [0 4]y + [0 2]z + [5] >= [0 4]x + [0 4]y + [0 2]z + [1] = f#(c(x,b(z,x),y)) [2 2] [2 4] [2 4] [4] [0 2] [0 0] [0 0] [0] b(a(),b(c(z,x,y),a())) = [2 2]x + [2 4]y + [2 4]z + [5] >= [0 2]x + [2 4]y + [2 3]z + [4] = b(b(z,c(y,z,a())),x) [0] [0] f(c(a(),b(b(z,a()),y),x)) = [0] >= [0] = f(c(x,b(z,x),y)) [0 1] [0 2] [0] c(f(c(a(),y,a())),x,z) = [1 1]x + [1 2]z >= [0] = f(b(b(z,z),f(b(y,b(x,a()))))) problem: DPs: TRS: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) Qed DPs: c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) TRS: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) Usable Rule Processor: DPs: c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) TRS: Semantic Labeling Processor: dimension: 1 usable rules: interpretation: [f](x0) = 0, [b](x0, x1) = 0, [c](x0, x1, x2) = x0 + 1, [a] = 1 labeled: usable (for model): argument filtering: pi(a) = [] pi(c) = [0] pi(b) = 0 pi(f) = 0 pi(b#) = 1 pi(c#) = 1 precedence: c# ~ b# ~ f ~ b ~ c ~ a problem: DPs: c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) TRS: Restore Modifier: DPs: c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) TRS: b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x) f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y)) c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a()))))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1