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: 1 enrichment: match-dp automaton: final states: {7} transitions: s0(10) -> 11* s0(5) -> 2* s0(12) -> 12* s0(2) -> 2* s0(9) -> 9* s0(4) -> 2* s0(6) -> 10* s0(1) -> 8,2 s0(3) -> 2* 00() -> 1* minus0(3,1) -> 5* minus0(3,3) -> 5* minus0(3,5) -> 5* minus0(4,2) -> 5* minus0(4,4) -> 5* minus0(5,1) -> 5* minus0(5,3) -> 5* minus0(5,5) -> 5* minus0(1,2) -> 5* minus0(1,4) -> 5* minus0(2,1) -> 5* minus0(2,3) -> 5* minus0(2,5) -> 5* minus0(3,2) -> 5* minus0(3,4) -> 5* minus0(4,1) -> 5* minus0(4,3) -> 5* minus0(4,5) -> 5* minus0(5,2) -> 5* minus0(5,4) -> 5* minus0(1,1) -> 5* minus0(1,3) -> 5* minus0(1,5) -> 5* minus0(2,2) -> 5* minus0(2,4) -> 5* plus{#,1}(30,27) -> 4,6 plus1(2,26) -> 27* plus1(3,29) -> 30* plus1(4,26) -> 27* plus1(5,29) -> 30* plus1(1,26) -> 27* plus1(2,29) -> 30* plus1(3,26) -> 27* plus1(4,29) -> 30* plus1(5,26) -> 27* plus1(1,29) -> 30* s1(30) -> 30* s1(25) -> 26* s1(5) -> 28* s1(27) -> 27* s1(2) -> 28* s1(4) -> 28* s1(1) -> 28* s1(28) -> 29* s1(3) -> 28* 01() -> 25* plus{#,0}(3,1) -> 4* plus{#,0}(3,3) -> 4* plus{#,0}(3,5) -> 4* plus{#,0}(4,2) -> 4* plus{#,0}(4,4) -> 4* plus{#,0}(5,1) -> 4* plus{#,0}(5,3) -> 4* plus{#,0}(5,5) -> 4* plus{#,0}(1,2) -> 4* plus{#,0}(1,4) -> 4* plus{#,0}(2,1) -> 4* plus{#,0}(2,3) -> 4* plus{#,0}(2,5) -> 4* plus{#,0}(12,9) -> 7* plus{#,0}(3,2) -> 4* plus{#,0}(3,4) -> 4* plus{#,0}(4,1) -> 4* plus{#,0}(4,3) -> 4* plus{#,0}(4,5) -> 4* plus{#,0}(5,2) -> 4* plus{#,0}(5,4) -> 4* plus{#,0}(1,1) -> 4* plus{#,0}(1,3) -> 4* plus{#,0}(1,5) -> 4* plus{#,0}(2,2) -> 4* plus{#,0}(2,4) -> 4* plus0(3,1) -> 3* plus0(3,3) -> 3* plus0(3,5) -> 3* plus0(4,2) -> 3* plus0(4,4) -> 3* plus0(5,1) -> 3* plus0(5,3) -> 3* plus0(5,5) -> 3* plus0(1,2) -> 3* plus0(1,4) -> 3* plus0(6,8) -> 9* plus0(2,1) -> 3* plus0(2,3) -> 3* plus0(2,5) -> 3* plus0(3,2) -> 3* plus0(3,4) -> 3* plus0(4,1) -> 3* plus0(4,3) -> 3* plus0(4,5) -> 3* plus0(5,2) -> 3* plus0(5,4) -> 3* plus0(1,1) -> 3* plus0(1,3) -> 3* plus0(1,5) -> 3* plus0(6,11) -> 12* plus0(2,2) -> 3* plus0(2,4) -> 3* 1 -> 5,3,6 2 -> 5,3,6 3 -> 5,6 4 -> 5,3,6 5 -> 3,6 8 -> 9* 11 -> 12* 26 -> 27* 29 -> 30* 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: 1 enrichment: match-dp automaton: final states: {5} transitions: plus{#,0}(10,7) -> 5* s0(2) -> 2* s0(4) -> 8* s0(1) -> 6,2 s0(8) -> 9* s0(3) -> 2* 00() -> 1* minus0(3,1) -> 7,3 minus0(3,3) -> 3* minus0(4,6) -> 7* minus0(1,2) -> 3* minus0(1,8) -> 10* minus0(2,1) -> 7,3 minus0(2,3) -> 3* minus0(3,2) -> 3* minus0(3,4) -> 10* minus0(3,8) -> 10* minus0(4,9) -> 10* minus0(1,1) -> 7,3 minus0(1,3) -> 3* minus0(2,2) -> 3* minus0(2,8) -> 10* plus{#,1}(22,19) -> 5* s1(20) -> 21* s1(17) -> 18* s1(2) -> 20* s1(1) -> 20* s1(3) -> 20* 01() -> 17* minus1(2,20) -> 22* minus1(3,3) -> 22* minus1(3,17) -> 19* minus1(3,21) -> 22* minus1(1,18) -> 19* minus1(1,20) -> 22* minus1(2,17) -> 19* minus1(3,18) -> 19* minus1(3,20) -> 22* minus1(1,17) -> 19* 1 -> 19,7,3,4 2 -> 19,7,3,4 3 -> 22,19,10,7,4 problem: DPs: TRS: minus(s(x),s(y)) -> minus(x,y) minus(x,0()) -> x Qed