Term Rewriting System R:

   [X, Y, DX, DY, DDX]
   din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
   din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
   din(der(der(X))) -> u41(din(der(X)), X)
   u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
   u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
   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)))
   u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
   u42(dout(DDX), X, DX) -> dout(DDX)

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   DIN(der(plus(X, Y))) -> U21(din(der(X)), X, Y)
   DIN(der(plus(X, Y))) -> DIN(der(X))
   DIN(der(der(X))) -> U41(din(der(X)), X)
   DIN(der(der(X))) -> DIN(der(X))
   DIN(der(times(X, Y))) -> U31(din(der(X)), X, Y)
   DIN(der(times(X, Y))) -> DIN(der(X))
   U21(dout(DX), X, Y) -> U22(din(der(Y)), X, Y, DX)
   U21(dout(DX), X, Y) -> DIN(der(Y))
   U41(dout(DX), X) -> U42(din(der(DX)), X, DX)
   U41(dout(DX), X) -> DIN(der(DX))
   U31(dout(DX), X, Y) -> U32(din(der(Y)), X, Y, DX)
   U31(dout(DX), X, Y) -> DIN(der(Y))

Furthermore, R contains one SCC.


SCC1:

DIN(der(times(X, Y))) -> DIN(der(X))
U31(dout(DX), X, Y) -> DIN(der(Y))
DIN(der(times(X, Y))) -> U31(din(der(X)), X, Y)
DIN(der(der(X))) -> DIN(der(X))
U41(dout(DX), X) -> DIN(der(DX))
DIN(der(der(X))) -> U41(din(der(X)), X)
DIN(der(plus(X, Y))) -> DIN(der(X))
U21(dout(DX), X, Y) -> DIN(der(Y))
DIN(der(plus(X, Y))) -> U21(din(der(X)), X, Y)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
   din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
   din(der(der(X))) -> u41(din(der(X)), X)
   din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
   u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
   u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
   u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
   u42(dout(DDX), X, DX) -> dout(DDX)
   u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(U41(x_1, x_2)) = 0
POL(U21(x_1, x_2, x_3)) = 0
POL(plus(x_1, x_2)) = 0
POL(u41(x_1, x_2)) = 0
POL(u21(x_1, x_2, x_3)) = 0
POL(der(x_1)) = 0
POL(DIN(x_1)) = 0
POL(din(x_1)) = 0
POL(times(x_1, x_2)) = 0
POL(u42(x_1, x_2, x_3)) = x_1
POL(U31(x_1, x_2, x_3)) = x_1
POL(dout(x_1)) = 1
POL(u22(x_1, x_2, x_3, x_4)) = x_1
POL(u31(x_1, x_2, x_3)) = 0
POL(u32(x_1, x_2, x_3, x_4)) = x_1

 resulting in one subcycle.


SCC1.Polo1:

DIN(der(der(X))) -> DIN(der(X))
U41(dout(DX), X) -> DIN(der(DX))
DIN(der(der(X))) -> U41(din(der(X)), X)
DIN(der(plus(X, Y))) -> DIN(der(X))
U21(dout(DX), X, Y) -> DIN(der(Y))
DIN(der(plus(X, Y))) -> U21(din(der(X)), X, Y)
DIN(der(times(X, Y))) -> DIN(der(X))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
   din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
   din(der(der(X))) -> u41(din(der(X)), X)
   din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
   u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
   u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
   u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
   u42(dout(DDX), X, DX) -> dout(DDX)
   u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(U41(x_1, x_2)) = x_1
POL(U21(x_1, x_2, x_3)) = 0
POL(plus(x_1, x_2)) = 0
POL(u41(x_1, x_2)) = 0
POL(u21(x_1, x_2, x_3)) = 0
POL(der(x_1)) = 0
POL(DIN(x_1)) = 0
POL(din(x_1)) = 0
POL(times(x_1, x_2)) = 0
POL(u42(x_1, x_2, x_3)) = x_1
POL(dout(x_1)) = 1
POL(u22(x_1, x_2, x_3, x_4)) = x_1
POL(u31(x_1, x_2, x_3)) = 0
POL(u32(x_1, x_2, x_3, x_4)) = x_1

 resulting in one subcycle.


SCC1.Polo1.Polo1:

DIN(der(times(X, Y))) -> DIN(der(X))
DIN(der(plus(X, Y))) -> DIN(der(X))
U21(dout(DX), X, Y) -> DIN(der(Y))
DIN(der(plus(X, Y))) -> U21(din(der(X)), X, Y)
DIN(der(der(X))) -> DIN(der(X))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
   din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
   din(der(der(X))) -> u41(din(der(X)), X)
   din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
   u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
   u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
   u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
   u42(dout(DDX), X, DX) -> dout(DDX)
   u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(plus(x_1, x_2)) = 1 + x_1 + x_2
POL(U21(x_1, x_2, x_3)) = 1 + x_1 + x_3
POL(u41(x_1, x_2)) = 0
POL(u21(x_1, x_2, x_3)) = 0
POL(der(x_1)) = 1 + x_1
POL(DIN(x_1)) = x_1
POL(din(x_1)) = 0
POL(times(x_1, x_2)) = 1 + x_1
POL(u42(x_1, x_2, x_3)) = x_1
POL(dout(x_1)) = 1
POL(u22(x_1, x_2, x_3, x_4)) = x_1
POL(u31(x_1, x_2, x_3)) = 0
POL(u32(x_1, x_2, x_3, x_4)) = x_1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 9.572 seconds.