YES Problem: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) Proof: DP Processor: DPs: minus#(s(x),s(y)) -> minus#(x,y) quot#(s(x),s(y)) -> minus#(x,y) quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) plus#(s(x),y) -> plus#(x,y) plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) EDG Processor: DPs: minus#(s(x),s(y)) -> minus#(x,y) quot#(s(x),s(y)) -> minus#(x,y) quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) plus#(s(x),y) -> plus#(x,y) plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) graph: plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y) plus#(s(x),y) -> plus#(x,y) -> plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) -> plus#(s(x),y) -> plus#(x,y) plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) -> plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) -> quot#(s(x),s(y)) -> minus#(x,y) quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) -> quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) quot#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y) minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y) SCC Processor: #sccs: 3 #rules: 4 #arcs: 8/25 DPs: quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) Matrix Interpretation Processor: dimension: 1 interpretation: [quot#](x0, x1) = x0, [plus](x0, x1) = x0 + x1, [quot](x0, x1) = x0, [s](x0) = x0 + 1, [minus](x0, x1) = x0, [0] = 0 orientation: quot#(s(x),s(y)) = x + 1 >= x = quot#(minus(x,y),s(y)) minus(x,0()) = x >= x = x minus(s(x),s(y)) = x + 1 >= x = minus(x,y) quot(0(),s(y)) = 0 >= 0 = 0() quot(s(x),s(y)) = x + 1 >= x + 1 = s(quot(minus(x,y),s(y))) plus(0(),y) = y >= y = y plus(s(x),y) = x + y + 1 >= x + y + 1 = s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) = x + y >= x + y = plus(minus(y,s(s(z))),minus(x,s(0()))) problem: DPs: TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) Qed DPs: minus#(s(x),s(y)) -> minus#(x,y) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) Subterm Criterion Processor: simple projection: pi(minus#) = 1 problem: DPs: TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) Qed DPs: plus#(s(x),y) -> plus#(x,y) plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) Matrix Interpretation Processor: dimension: 1 interpretation: [plus#](x0, x1) = x0 + x1, [plus](x0, x1) = x0 + x1 + 1, [quot](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [minus](x0, x1) = x0, [0] = 0 orientation: plus#(s(x),y) = x + y + 1 >= x + y = plus#(x,y) plus#(minus(x,s(0())),minus(y,s(s(z)))) = x + y >= x + y = plus#(minus(y,s(s(z))),minus(x,s(0()))) minus(x,0()) = x >= x = x minus(s(x),s(y)) = x + 1 >= x = minus(x,y) quot(0(),s(y)) = y + 1 >= 0 = 0() quot(s(x),s(y)) = x + y + 2 >= x + y + 2 = s(quot(minus(x,y),s(y))) plus(0(),y) = y + 1 >= y = y plus(s(x),y) = x + y + 2 >= x + y + 2 = s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) = x + y + 1 >= x + y + 1 = plus(minus(y,s(s(z))),minus(x,s(0()))) problem: DPs: plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0()))) Usable Rule Processor: DPs: plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) TRS: minus(s(x),s(y)) -> minus(x,y) minus(x,0()) -> x Bounds Processor: bound: 1 enrichment: match automaton: final states: {6} transitions: plus{#,0}(5,5) -> 6* minus0(5,5) -> 5* s0(5) -> 5* 00() -> 5* minus1(5,5) -> 18,5 minus1(5,13) -> 15* minus1(5,17) -> 18* minus1(5,14) -> 15* minus1(5,16) -> 18* plus{#,1}(18,15) -> 6* s1(5) -> 16* s1(16) -> 17* s1(13) -> 14* 01() -> 13* 5 -> 18,15 problem: DPs: TRS: minus(s(x),s(y)) -> minus(x,y) minus(x,0()) -> x Qed