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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(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()))) plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(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()))) plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(x,s(0()))) graph: plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(x,s(0()))) -> plus#(s(x),y) -> plus#(x,y) plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(x,s(0()))) -> plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(x,s(0()))) -> plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(x,s(0()))) 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#(s(x),y) -> plus#(x,y) -> plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(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()))) plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) -> plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(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: 5 #arcs: 13/36 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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) = x + y + z + 3 >= x + y + z + 3 = plus(plus(y,s(s(z))),plus(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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(x,s(0()))) Qed DPs: plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(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) 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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(x,s(0()))) Matrix Interpretation Processor: dimension: 1 interpretation: [plus#](x0, x1) = x0 + x1, [plus](x0, x1) = x0 + x1, [quot](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [minus](x0, x1) = x0, [0] = 0 orientation: plus#(plus(x,s(0())),plus(y,s(s(z)))) = x + y + z + 3 >= x + y + z + 3 = plus#(plus(y,s(s(z))),plus(x,s(0()))) plus#(minus(x,s(0())),minus(y,s(s(z)))) = x + y >= x + y = plus#(minus(y,s(s(z))),minus(x,s(0()))) plus#(s(x),y) = x + y + 1 >= x + y = plus#(x,y) 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 >= 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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) = x + y + z + 3 >= x + y + z + 3 = plus(plus(y,s(s(z))),plus(x,s(0()))) problem: DPs: plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(x,s(0()))) 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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(x,s(0()))) Usable Rule Processor: DPs: plus#(plus(x,s(0())),plus(y,s(s(z)))) -> plus#(plus(y,s(s(z))),plus(x,s(0()))) plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) TRS: 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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(x,s(0()))) minus(s(x),s(y)) -> minus(x,y) minus(x,0()) -> x Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: plus{#,0}(8,5) -> 1* plus0(4,3) -> 5* plus0(4,7) -> 8* s0(5) -> 5* s0(2) -> 3* s0(4) -> 6* s0(6) -> 7* s0(8) -> 8* 00() -> 2* f80() -> 4* 3 -> 5* 7 -> 8* problem: DPs: plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) TRS: 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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(x,s(0()))) minus(s(x),s(y)) -> minus(x,y) minus(x,0()) -> x Restore Modifier: 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()))) plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(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: 0 enrichment: match-dp automaton: final states: {1} transitions: plus{#,0}(8,5) -> 1* s0(2) -> 3* s0(4) -> 6* s0(6) -> 7* 00() -> 2* minus0(4,2) -> 5* minus0(4,4) -> 8* minus0(4,6) -> 8* minus0(4,3) -> 5* minus0(4,7) -> 8* f150() -> 4* 4 -> 8,5 problem: DPs: TRS: minus(s(x),s(y)) -> minus(x,y) minus(x,0()) -> x Qed