YES Problem: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) Proof: DP Processor: DPs: le#(s(X),s(Y)) -> le#(X,Y) minus#(s(X),Y) -> le#(s(X),Y) minus#(s(X),Y) -> ifMinus#(le(s(X),Y),s(X),Y) ifMinus#(false(),s(X),Y) -> minus#(X,Y) quot#(s(X),s(Y)) -> minus#(X,Y) quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) TDG Processor: DPs: le#(s(X),s(Y)) -> le#(X,Y) minus#(s(X),Y) -> le#(s(X),Y) minus#(s(X),Y) -> ifMinus#(le(s(X),Y),s(X),Y) ifMinus#(false(),s(X),Y) -> minus#(X,Y) quot#(s(X),s(Y)) -> minus#(X,Y) quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) graph: 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)) -> quot#(minus(X,Y),s(Y)) -> quot#(s(X),s(Y)) -> minus#(X,Y) quot#(s(X),s(Y)) -> minus#(X,Y) -> minus#(s(X),Y) -> ifMinus#(le(s(X),Y),s(X),Y) quot#(s(X),s(Y)) -> minus#(X,Y) -> minus#(s(X),Y) -> le#(s(X),Y) ifMinus#(false(),s(X),Y) -> minus#(X,Y) -> minus#(s(X),Y) -> ifMinus#(le(s(X),Y),s(X),Y) ifMinus#(false(),s(X),Y) -> minus#(X,Y) -> minus#(s(X),Y) -> le#(s(X),Y) minus#(s(X),Y) -> ifMinus#(le(s(X),Y),s(X),Y) -> ifMinus#(false(),s(X),Y) -> minus#(X,Y) minus#(s(X),Y) -> le#(s(X),Y) -> le#(s(X),s(Y)) -> le#(X,Y) le#(s(X),s(Y)) -> le#(X,Y) -> le#(s(X),s(Y)) -> le#(X,Y) SCC Processor: #sccs: 3 #rules: 4 #arcs: 9/36 DPs: quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) KBO Processor: argument filtering: pi(0) = [] pi(le) = 0 pi(true) = [] pi(s) = [0] pi(false) = [] pi(minus) = 0 pi(ifMinus) = 1 pi(quot) = [0] pi(quot#) = 0 weight function: w0 = 1 w(quot#) = w(quot) = w(false) = w(s) = w(true) = w(0) = 1 w(ifMinus) = w(minus) = w(le) = 0 precedence: 0 > quot > quot# ~ ifMinus ~ minus ~ false ~ s ~ true ~ le problem: DPs: TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) Qed DPs: minus#(s(X),Y) -> ifMinus#(le(s(X),Y),s(X),Y) ifMinus#(false(),s(X),Y) -> minus#(X,Y) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) Matrix Interpretation Processor: dim=1 interpretation: [ifMinus#](x0, x1, x2) = 4x1 + 4x2, [minus#](x0, x1) = 6x0 + 4x1 + 1, [quot](x0, x1) = x0, [ifMinus](x0, x1, x2) = x1, [minus](x0, x1) = x0, [false] = 0, [s](x0) = 3x0 + 4, [true] = 1, [le](x0, x1) = 4x1 + 1, [0] = 1 orientation: minus#(s(X),Y) = 18X + 4Y + 25 >= 12X + 4Y + 16 = ifMinus#(le(s(X),Y),s(X),Y) ifMinus#(false(),s(X),Y) = 12X + 4Y + 16 >= 6X + 4Y + 1 = minus#(X,Y) le(0(),Y) = 4Y + 1 >= 1 = true() le(s(X),0()) = 5 >= 0 = false() le(s(X),s(Y)) = 12Y + 17 >= 4Y + 1 = le(X,Y) minus(0(),Y) = 1 >= 1 = 0() minus(s(X),Y) = 3X + 4 >= 3X + 4 = ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) = 3X + 4 >= 1 = 0() ifMinus(false(),s(X),Y) = 3X + 4 >= 3X + 4 = s(minus(X,Y)) quot(0(),s(Y)) = 1 >= 1 = 0() quot(s(X),s(Y)) = 3X + 4 >= 3X + 4 = s(quot(minus(X,Y),s(Y))) problem: DPs: TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) Qed DPs: le#(s(X),s(Y)) -> le#(X,Y) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) KBO Processor: argument filtering: pi(0) = [] pi(le) = [1] pi(true) = [] pi(s) = [0] pi(false) = [] pi(minus) = 0 pi(ifMinus) = 1 pi(quot) = 0 pi(le#) = 1 weight function: w0 = 1 w(le#) = w(ifMinus) = w(minus) = w(false) = w(s) = w(true) = w( le) = w(0) = 1 w(quot) = 0 precedence: le# ~ quot ~ ifMinus ~ minus ~ false ~ s ~ true ~ le ~ 0 problem: DPs: TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) ifMinus(true(),s(X),Y) -> 0() ifMinus(false(),s(X),Y) -> s(minus(X,Y)) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) Qed