YES Problem: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Proof: DP Processor: DPs: +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) TDG Processor: DPs: +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) graph: f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z)) f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z)) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(y,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),b()) -> +#(b(),a()) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(+(x,y),z) -> +#(y,z) -> +#(a(),b()) -> +#(b(),a()) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) -> +#(+(x,y),z) -> +#(y,z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) -> +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(+(x,y),z) -> +#(y,z) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),b()) -> +#(b(),a()) +#(a(),b()) -> +#(b(),a()) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(a(),b()) -> +#(b(),a()) -> +#(+(x,y),z) -> +#(y,z) +#(a(),b()) -> +#(b(),a()) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(a(),b()) -> +#(b(),a()) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),b()) -> +#(b(),a()) -> +#(a(),b()) -> +#(b(),a()) EDG Processor: DPs: +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) graph: f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z)) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z)) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),b()) -> +#(b(),a()) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(y,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) -> +#(a(),b()) -> +#(b(),a()) +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),b()) -> +#(b(),a()) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) CDG Processor: DPs: +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) graph: f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z)) f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z)) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(y,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),b()) -> +#(b(),a()) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(+(x,y),z) -> +#(y,z) -> +#(a(),b()) -> +#(b(),a()) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),b()) -> +#(b(),a()) SCC Processor: #sccs: 3 #rules: 5 #arcs: 23/64 DPs: f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) KBO Processor: argument filtering: pi(a) = [] pi(b) = [] pi(+) = [0,1] pi(f) = 0 pi(f#) = 0 weight function: w0 = 1 w(f#) = w(f) = w(b) = w(a) = 1 w(+) = 0 precedence: f# ~ + ~ a > f ~ b problem: DPs: TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Qed DPs: +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) KBO Processor: argument filtering: pi(a) = [] pi(b) = [] pi(+) = [0,1] pi(f) = 0 pi(+#) = 0 weight function: w0 = 1 w(+#) = w(f) = w(+) = w(b) = w(a) = 1 precedence: +# ~ + ~ a > f ~ b problem: DPs: TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Qed DPs: +#(a(),+(b(),z)) -> +#(a(),z) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) KBO Processor: argument filtering: pi(a) = [] pi(b) = [] pi(+) = [0,1] pi(f) = 0 pi(+#) = 1 weight function: w0 = 1 w(+#) = w(b) = w(a) = 1 w(f) = w(+) = 0 precedence: +# ~ a > f ~ + ~ b problem: DPs: TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Qed