Term Rewriting System R:
[x, y]
D(t) > 1
D(constant) > 0
D(+(x, y)) > +(D(x), D(y))
D(*(x, y)) > +(*(y, D(x)), *(x, D(y)))
D((x, y)) > (D(x), D(y))
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:
D'(+(x, y)) > D'(x)
D'(+(x, y)) > D'(y)
D'(*(x, y)) > D'(x)
D'(*(x, y)) > D'(y)
D'((x, y)) > D'(x)
D'((x, y)) > D'(y)
Furthermore, R contains one SCC.
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
Dependency Pairs:
D'((x, y)) > D'(y)
D'((x, y)) > D'(x)
D'(*(x, y)) > D'(y)
D'(*(x, y)) > D'(x)
D'(+(x, y)) > D'(y)
D'(+(x, y)) > D'(x)
Rules:
D(t) > 1
D(constant) > 0
D(+(x, y)) > +(D(x), D(y))
D(*(x, y)) > +(*(y, D(x)), *(x, D(y)))
D((x, y)) > (D(x), D(y))
Strategy:
innermost
As we are in the innermost case, we can delete all 5 nonusablerules.
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 2
↳SizeChange Principle
Dependency Pairs:
D'((x, y)) > D'(y)
D'((x, y)) > D'(x)
D'(*(x, y)) > D'(y)
D'(*(x, y)) > D'(x)
D'(+(x, y)) > D'(y)
D'(+(x, y)) > D'(x)
Rule:
none
Strategy:
innermost
We number the DPs as follows:
 D'((x, y)) > D'(y)
 D'((x, y)) > D'(x)
 D'(*(x, y)) > D'(y)
 D'(*(x, y)) > D'(x)
 D'(+(x, y)) > D'(y)
 D'(+(x, y)) > D'(x)
and get the following SizeChange Graph(s): {1, 2, 3, 4, 5, 6}  ,  {1, 2, 3, 4, 5, 6} 

1  >  1 

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

1  >  1 

D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with NonStrict Precedence.
trivial
with Argument Filtering System:
*(x_{1}, x_{2}) > *(x_{1}, x_{2})
(x_{1}, x_{2}) > (x_{1}, x_{2})
+(x_{1}, x_{2}) > +(x_{1}, x_{2})
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes