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. 



   R
     ↳Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost. 


   R
     ↳OC
       →TRS2
         ↳Dependency Pair Analysis



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(times(X, Y))) -> U31(din(der(X)), X, Y)
DIN(der(times(X, Y))) -> DIN(der(X))
DIN(der(der(X))) -> U41(din(der(X)), X)
DIN(der(der(X))) -> DIN(der(X))
U21(dout(DX), X, Y) -> U22(din(der(Y)), X, Y, DX)
U21(dout(DX), X, Y) -> DIN(der(Y))
U31(dout(DX), X, Y) -> U32(din(der(Y)), X, Y, DX)
U31(dout(DX), X, Y) -> DIN(der(Y))
U41(dout(DX), X) -> U42(din(der(DX)), X, DX)
U41(dout(DX), X) -> DIN(der(DX))

Furthermore, R contains one SCC. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Negative Polynomial Order


Dependency Pairs:

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(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(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)


Rules:


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)


Strategy:

innermost




The following Dependency Pair can be strictly oriented using the given order.

U41(dout(DX), X) -> DIN(der(DX))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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


Used ordering:
Polynomial Order with Interpretation:

POL( U41(x1, x2) ) = x1

POL( dout(x1) ) = 1

POL( DIN(x1) ) = 0

POL( U31(x1, ..., x3) ) = 0

POL( U21(x1, ..., x3) ) = 0

POL( din(x1) ) = 0

POL( u41(x1, x2) ) = 0

POL( u42(x1, ..., x3) ) = x1

POL( u21(x1, ..., x3) ) = 0

POL( u31(x1, ..., x3) ) = 0

POL( u32(x1, ..., x4) ) = x1

POL( u22(x1, ..., x4) ) = x1


This results in one new DP problem. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Neg POLO
             ...
               →DP Problem 2
                 ↳Dependency Graph


Dependency Pairs:

DIN(der(der(X))) -> DIN(der(X))
DIN(der(der(X))) -> U41(din(der(X)), X)
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(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)


Rules:


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)


Strategy:

innermost




Using the Dependency Graph the DP problem was split into 1 DP problems.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Neg POLO
             ...
               →DP Problem 3
                 ↳Negative Polynomial Order


Dependency Pairs:

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(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))


Rules:


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)


Strategy:

innermost




The following Dependency Pairs can be strictly oriented using the given order.

DIN(der(times(X, Y))) -> DIN(der(X))
DIN(der(times(X, Y))) -> U31(din(der(X)), X, Y)


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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


Used ordering:
Polynomial Order with Interpretation:

POL( DIN(x1) ) = x1

POL( der(x1) ) = x1

POL( times(x1, x2) ) = x1 + x2 + 1

POL( U31(x1, ..., x3) ) = x3

POL( plus(x1, x2) ) = x1 + x2

POL( U21(x1, ..., x3) ) = x3

POL( u41(x1, x2) ) = 0

POL( u42(x1, ..., x3) ) = 0

POL( din(x1) ) = 0

POL( u21(x1, ..., x3) ) = 0

POL( dout(x1) ) = 0

POL( u31(x1, ..., x3) ) = 0

POL( u32(x1, ..., x4) ) = 0

POL( u22(x1, ..., x4) ) = 0


This results in one new DP problem. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Neg POLO
             ...
               →DP Problem 4
                 ↳Dependency Graph


Dependency Pairs:

U31(dout(DX), X, Y) -> DIN(der(Y))
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))


Rules:


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)


Strategy:

innermost




Using the Dependency Graph the DP problem was split into 1 DP problems.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Neg POLO
             ...
               →DP Problem 5
                 ↳Negative Polynomial Order


Dependency Pairs:

DIN(der(der(X))) -> 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)


Rules:


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)


Strategy:

innermost




The following Dependency Pair can be strictly oriented using the given order.

DIN(der(der(X))) -> DIN(der(X))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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


Used ordering:
Polynomial Order with Interpretation:

POL( DIN(x1) ) = x1

POL( der(x1) ) = x1 + 1

POL( plus(x1, x2) ) = x1 + x2

POL( U21(x1, ..., x3) ) = x3 + 1

POL( u41(x1, x2) ) = 0

POL( u42(x1, ..., x3) ) = 0

POL( din(x1) ) = 0

POL( u21(x1, ..., x3) ) = 0

POL( dout(x1) ) = 0

POL( u31(x1, ..., x3) ) = 0

POL( u32(x1, ..., x4) ) = 0

POL( u22(x1, ..., x4) ) = 0


This results in one new DP problem. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Neg POLO
             ...
               →DP Problem 6
                 ↳Size-Change Principle


Dependency Pairs:

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)


Rules:


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)


Strategy:

innermost




We number the DPs as follows:
  1. DIN(der(plus(X, Y))) -> DIN(der(X))
  2. U21(dout(DX), X, Y) -> DIN(der(Y))
  3. DIN(der(plus(X, Y))) -> U21(din(der(X)), X, Y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
{2} , {2}
3=1
{3} , {3}
1>2
1>3

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
{2} , {3}
3>2
3>3
{3} , {2}
1>1
{3} , {1}
1>1
{1} , {2}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
der(x1) -> x1
plus(x1, x2) -> plus(x1, x2)
dout(x1) -> dout(x1)

We obtain no new DP problems.

Termination of R successfully shown.
Duration:
0:02 minutes