YES (VAR X Y DX DY DDX) (RULES din(der(plus(X,Y))) -> u21(din(der(X)),X,Y) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY)) din(der(times(X,Y))) -> u31(din(der(X)),X,Y) u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX))) din(der(der(X))) -> u41(din(der(X)),X) u41(dout(DX),X) -> u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) -> dout(DDX) ) The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting. Proving termination of innermost rewriting for wst99: -> Dependency pairs: nF_din(der(plus(X,Y))) -> nF_u21(din(der(X)),X,Y) nF_din(der(plus(X,Y))) -> nF_din(der(X)) nF_u21(dout(DX),X,Y) -> nF_u22(din(der(Y)),X,Y,DX) nF_u21(dout(DX),X,Y) -> nF_din(der(Y)) nF_din(der(times(X,Y))) -> nF_u31(din(der(X)),X,Y) nF_din(der(times(X,Y))) -> nF_din(der(X)) nF_u31(dout(DX),X,Y) -> nF_u32(din(der(Y)),X,Y,DX) nF_u31(dout(DX),X,Y) -> nF_din(der(Y)) nF_din(der(der(X))) -> nF_u41(din(der(X)),X) nF_din(der(der(X))) -> nF_din(der(X)) nF_u41(dout(DX),X) -> nF_u42(din(der(DX)),X,DX) nF_u41(dout(DX),X) -> nF_din(der(DX)) -> Proof of termination for wst99_1: -> -> Dependency pairs in cycle: nF_din(der(plus(X,Y))) -> nF_u21(din(der(X)),X,Y) nF_u41(dout(DX),X) -> nF_din(der(DX)) nF_din(der(der(X))) -> nF_u41(din(der(X)),X) nF_din(der(der(X))) -> nF_din(der(X)) nF_u31(dout(DX),X,Y) -> nF_din(der(Y)) nF_din(der(times(X,Y))) -> nF_u31(din(der(X)),X,Y) nF_din(der(times(X,Y))) -> nF_din(der(X)) nF_u21(dout(DX),X,Y) -> nF_din(der(Y)) nF_din(der(plus(X,Y))) -> nF_din(der(X)) UsableRules: din(der(plus(X,Y))) -> u21(din(der(X)),X,Y) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY)) din(der(times(X,Y))) -> u31(din(der(X)),X,Y) u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX))) din(der(der(X))) -> u41(din(der(X)),X) u41(dout(DX),X) -> u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) -> dout(DDX) Polynomial Interpretation: [din](X) = 0 [der](X) = 0 [plus](X1,X2) = 0 [u21](X1,X2,X3) = 0 [dout](X) = 1 [u22](X1,X2,X3,X4) = X1 [times](X1,X2) = 0 [u31](X1,X2,X3) = X1 [u32](X1,X2,X3,X4) = 1 [u41](X1,X2) = X1 [u42](X1,X2,X3) = X1 [nF_din](X) = 0 [nF_u41](X1,X2) = 0 [nF_u31](X1,X2,X3) = 0 [nF_u21](X1,X2,X3) = X1 TIME: 0.164394 -> -> Dependency pairs in cycle: nF_u41(dout(DX),X) -> nF_din(der(DX)) nF_din(der(der(X))) -> nF_u41(din(der(X)),X) nF_din(der(plus(X,Y))) -> nF_din(der(X)) nF_din(der(times(X,Y))) -> nF_din(der(X)) nF_u31(dout(DX),X,Y) -> nF_din(der(Y)) nF_din(der(times(X,Y))) -> nF_u31(din(der(X)),X,Y) nF_din(der(der(X))) -> nF_din(der(X)) UsableRules: din(der(plus(X,Y))) -> u21(din(der(X)),X,Y) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY)) din(der(times(X,Y))) -> u31(din(der(X)),X,Y) u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX))) din(der(der(X))) -> u41(din(der(X)),X) u41(dout(DX),X) -> u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) -> dout(DDX) Polynomial Interpretation: [din](X) = X [der](X) = X + 1 [plus](X1,X2) = X1 [u21](X1,X2,X3) = X1 [dout](X) = X + 1 [u22](X1,X2,X3,X4) = X4 + 1 [times](X1,X2) = X1 + X2 [u31](X1,X2,X3) = X2 + X3 + 1 [u32](X1,X2,X3,X4) = X1 + X2 [u41](X1,X2) = X1 [u42](X1,X2,X3) = X1 [nF_u41](X1,X2) = X1 [nF_din](X) = X [nF_u31](X1,X2,X3) = X1 + X3 TIME: 0.196759 -> -> Dependency pairs in cycle: nF_u41(dout(DX),X) -> nF_din(der(DX)) nF_din(der(der(X))) -> nF_u41(din(der(X)),X) nF_u31(dout(DX),X,Y) -> nF_din(der(Y)) nF_din(der(times(X,Y))) -> nF_u31(din(der(X)),X,Y) nF_din(der(times(X,Y))) -> nF_din(der(X)) nF_din(der(plus(X,Y))) -> nF_din(der(X)) UsableRules: din(der(plus(X,Y))) -> u21(din(der(X)),X,Y) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY)) din(der(times(X,Y))) -> u31(din(der(X)),X,Y) u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX))) din(der(der(X))) -> u41(din(der(X)),X) u41(dout(DX),X) -> u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) -> dout(DDX) Polynomial Interpretation: [din](X) = X [der](X) = X [plus](X1,X2) = X1 [u21](X1,X2,X3) = X1 [dout](X) = X + 1 [u22](X1,X2,X3,X4) = X4 + 1 [times](X1,X2) = X1 + X2 + 1 [u31](X1,X2,X3) = X2 + X3 + 1 [u32](X1,X2,X3,X4) = X1 + X2 + 1 [u41](X1,X2) = X1 [u42](X1,X2,X3) = X1 [nF_u41](X1,X2) = X1 [nF_din](X) = X [nF_u31](X1,X2,X3) = X3 TIME: 6.3517e-2 -> -> Dependency pairs in cycle: nF_u41(dout(DX),X) -> nF_din(der(DX)) nF_din(der(der(X))) -> nF_u41(din(der(X)),X) nF_din(der(plus(X,Y))) -> nF_din(der(X)) nF_u31(dout(DX),X,Y) -> nF_din(der(Y)) nF_din(der(times(X,Y))) -> nF_u31(din(der(X)),X,Y) UsableRules: din(der(plus(X,Y))) -> u21(din(der(X)),X,Y) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY)) din(der(times(X,Y))) -> u31(din(der(X)),X,Y) u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX))) din(der(der(X))) -> u41(din(der(X)),X) u41(dout(DX),X) -> u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) -> dout(DDX) Polynomial Interpretation: [din](X) = 0 [der](X) = 1 [plus](X1,X2) = 0 [u21](X1,X2,X3) = 0 [dout](X) = 1 [u22](X1,X2,X3,X4) = X1 [times](X1,X2) = 0 [u31](X1,X2,X3) = X1 [u32](X1,X2,X3,X4) = 1 [u41](X1,X2) = X1 [u42](X1,X2,X3) = X1 [nF_u41](X1,X2) = X1 [nF_din](X) = X [nF_u31](X1,X2,X3) = X1 TIME: 6.5323e-2 -> -> Dependency pairs in cycle: nF_u41(dout(DX),X) -> nF_din(der(DX)) nF_din(der(der(X))) -> nF_u41(din(der(X)),X) nF_din(der(plus(X,Y))) -> nF_din(der(X)) UsableRules: din(der(plus(X,Y))) -> u21(din(der(X)),X,Y) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY)) din(der(times(X,Y))) -> u31(din(der(X)),X,Y) u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX))) din(der(der(X))) -> u41(din(der(X)),X) u41(dout(DX),X) -> u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) -> dout(DDX) Polynomial Interpretation: [din](X) = 0 [der](X) = X [plus](X1,X2) = X1 + 1 [u21](X1,X2,X3) = X1 [dout](X) = X + 1 [u22](X1,X2,X3,X4) = X1 + X4 + 1 [times](X1,X2) = 0 [u31](X1,X2,X3) = X1 [u32](X1,X2,X3,X4) = X1 + 1 [u41](X1,X2) = 0 [u42](X1,X2,X3) = X1 [nF_u41](X1,X2) = X1 [nF_din](X) = X TIME: 6.4404e-2 -> -> Dependency pairs in cycle: nF_u41(dout(DX),X) -> nF_din(der(DX)) nF_din(der(der(X))) -> nF_u41(din(der(X)),X) UsableRules: din(der(plus(X,Y))) -> u21(din(der(X)),X,Y) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY)) din(der(times(X,Y))) -> u31(din(der(X)),X,Y) u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX))) din(der(der(X))) -> u41(din(der(X)),X) u41(dout(DX),X) -> u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) -> dout(DDX) Polynomial Interpretation: [din](X) = 0 [der](X) = X + 1 [plus](X1,X2) = 0 [u21](X1,X2,X3) = 0 [dout](X) = X [u22](X1,X2,X3,X4) = 0 [times](X1,X2) = 0 [u31](X1,X2,X3) = 0 [u32](X1,X2,X3,X4) = 0 [u41](X1,X2) = 0 [u42](X1,X2,X3) = X1 [nF_u41](X1,X2) = X1 + 1 [nF_din](X) = X TIME: 6.1557e-2 SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 1 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic Termination was proved succesfully.