Term Rewriting System R:
[x, y]
app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

APP(D, app(app(+, x), y)) -> APP(app(+, app(D, x)), app(D, y))
APP(D, app(app(+, x), y)) -> APP(+, app(D, x))
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
APP(D, app(app(*, x), y)) -> APP(+, app(app(*, y), app(D, x)))
APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
APP(D, app(app(*, x), y)) -> APP(*, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(app(*, x), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
APP(D, app(app(-, x), y)) -> APP(-, app(D, x))
APP(D, app(app(-, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, y)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Forward Instantiation Transformation


Dependency Pairs:

APP(D, app(app(-, x), y)) -> APP(D, y)
APP(D, app(app(-, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
APP(D, app(app(*, x), y)) -> APP(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(app(+, app(D, x)), app(D, y))


Rules:


app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(D, app(app(+, x), y)) -> APP(app(+, app(D, x)), app(D, y))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 2
Forward Instantiation Transformation


Dependency Pairs:

APP(D, app(app(-, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
APP(D, app(app(*, x), y)) -> APP(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, y)


Rules:


app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(D, app(app(*, x), y)) -> APP(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 2
FwdInst
             ...
               →DP Problem 3
Forward Instantiation Transformation


Dependency Pairs:

APP(D, app(app(-, x), y)) -> APP(D, y)
APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, x)


Rules:


app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 2
FwdInst
             ...
               →DP Problem 4
Forward Instantiation Transformation


Dependency Pairs:

APP(D, app(app(-, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, y)


Rules:


app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 2
FwdInst
             ...
               →DP Problem 5
Polynomial Ordering


Dependency Pairs:

APP(D, app(app(-, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, x)


Rules:


app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

APP(D, app(app(-, x), y)) -> APP(D, y)
APP(D, app(app(-, x), y)) -> APP(D, x)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(*)=  0  
  POL(D)=  0  
  POL(-)=  1  
  POL(APP(x1, x2))=  1 + x2  
  POL(app(x1, x2))=  x1 + x2  
  POL(+)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 2
FwdInst
             ...
               →DP Problem 6
Polynomial Ordering


Dependency Pairs:

APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)


Rules:


app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(*)=  1  
  POL(D)=  0  
  POL(APP(x1, x2))=  1 + x2  
  POL(app(x1, x2))=  x1 + x2  
  POL(+)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 2
FwdInst
             ...
               →DP Problem 7
Polynomial Ordering


Dependency Pairs:

APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)


Rules:


app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(D)=  0  
  POL(APP(x1, x2))=  1 + x2  
  POL(app(x1, x2))=  x1 + x2  
  POL(+)=  1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 2
FwdInst
             ...
               →DP Problem 8
Dependency Graph


Dependency Pair:


Rules:


app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:05 minutes