Term Rewriting System R:
[X, Y, X1, X2]
f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(g(X), Y) -> F(X, nf(ng(X), activate(Y)))
F(g(X), Y) -> ACTIVATE(Y)
ACTIVATE(nf(X1, X2)) -> F(activate(X1), X2)
ACTIVATE(nf(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(ng(X)) -> G(activate(X))
ACTIVATE(ng(X)) -> ACTIVATE(X)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Forward Instantiation Transformation


Dependency Pairs:

ACTIVATE(ng(X)) -> ACTIVATE(X)
ACTIVATE(nf(X1, X2)) -> ACTIVATE(X1)


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




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

ACTIVATE(nf(X1, X2)) -> ACTIVATE(X1)
two new Dependency Pairs are created:

ACTIVATE(nf(nf(X1'', X2''), X2)) -> ACTIVATE(nf(X1'', X2''))
ACTIVATE(nf(ng(X''), X2)) -> ACTIVATE(ng(X''))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

ACTIVATE(nf(ng(X''), X2)) -> ACTIVATE(ng(X''))
ACTIVATE(nf(nf(X1'', X2''), X2)) -> ACTIVATE(nf(X1'', X2''))
ACTIVATE(ng(X)) -> ACTIVATE(X)


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




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

ACTIVATE(ng(X)) -> ACTIVATE(X)
three new Dependency Pairs are created:

ACTIVATE(ng(ng(X''))) -> ACTIVATE(ng(X''))
ACTIVATE(ng(nf(nf(X1'''', X2''''), X2''))) -> ACTIVATE(nf(nf(X1'''', X2''''), X2''))
ACTIVATE(ng(nf(ng(X''''), X2''))) -> ACTIVATE(nf(ng(X''''), X2''))

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:

ACTIVATE(ng(nf(ng(X''''), X2''))) -> ACTIVATE(nf(ng(X''''), X2''))
ACTIVATE(nf(nf(X1'', X2''), X2)) -> ACTIVATE(nf(X1'', X2''))
ACTIVATE(ng(nf(nf(X1'''', X2''''), X2''))) -> ACTIVATE(nf(nf(X1'''', X2''''), X2''))
ACTIVATE(ng(ng(X''))) -> ACTIVATE(ng(X''))
ACTIVATE(nf(ng(X''), X2)) -> ACTIVATE(ng(X''))


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




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

ACTIVATE(nf(nf(X1'', X2''), X2)) -> ACTIVATE(nf(X1'', X2''))
two new Dependency Pairs are created:

ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))
ACTIVATE(nf(nf(ng(X''''), X2'''), X2)) -> ACTIVATE(nf(ng(X''''), X2'''))

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:

ACTIVATE(nf(nf(ng(X''''), X2'''), X2)) -> ACTIVATE(nf(ng(X''''), X2'''))
ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))
ACTIVATE(ng(nf(nf(X1'''', X2''''), X2''))) -> ACTIVATE(nf(nf(X1'''', X2''''), X2''))
ACTIVATE(ng(ng(X''))) -> ACTIVATE(ng(X''))
ACTIVATE(nf(ng(X''), X2)) -> ACTIVATE(ng(X''))
ACTIVATE(ng(nf(ng(X''''), X2''))) -> ACTIVATE(nf(ng(X''''), X2''))


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




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

ACTIVATE(nf(ng(X''), X2)) -> ACTIVATE(ng(X''))
three new Dependency Pairs are created:

ACTIVATE(nf(ng(ng(X'''')), X2)) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(nf(ng(nf(nf(X1'''''', X2''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(nf(ng(nf(ng(X''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

ACTIVATE(nf(ng(nf(ng(X''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))
ACTIVATE(nf(ng(nf(nf(X1'''''', X2''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(ng(nf(ng(X''''), X2''))) -> ACTIVATE(nf(ng(X''''), X2''))
ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))
ACTIVATE(ng(nf(nf(X1'''', X2''''), X2''))) -> ACTIVATE(nf(nf(X1'''', X2''''), X2''))
ACTIVATE(ng(ng(X''))) -> ACTIVATE(ng(X''))
ACTIVATE(nf(ng(ng(X'''')), X2)) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(nf(nf(ng(X''''), X2'''), X2)) -> ACTIVATE(nf(ng(X''''), X2'''))


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




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

ACTIVATE(ng(ng(X''))) -> ACTIVATE(ng(X''))
three new Dependency Pairs are created:

ACTIVATE(ng(ng(ng(X'''')))) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(ng(ng(nf(nf(X1'''''', X2''''''), X2'''')))) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(ng(ng(nf(ng(X''''''), X2'''')))) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

ACTIVATE(ng(ng(nf(ng(X''''''), X2'''')))) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))
ACTIVATE(nf(ng(nf(nf(X1'''''', X2''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(nf(nf(ng(X''''), X2'''), X2)) -> ACTIVATE(nf(ng(X''''), X2'''))
ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))
ACTIVATE(ng(nf(nf(X1'''', X2''''), X2''))) -> ACTIVATE(nf(nf(X1'''', X2''''), X2''))
ACTIVATE(ng(ng(nf(nf(X1'''''', X2''''''), X2'''')))) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(ng(ng(ng(X'''')))) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(nf(ng(ng(X'''')), X2)) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(ng(nf(ng(X''''), X2''))) -> ACTIVATE(nf(ng(X''''), X2''))
ACTIVATE(nf(ng(nf(ng(X''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




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

ACTIVATE(ng(nf(nf(X1'''', X2''''), X2''))) -> ACTIVATE(nf(nf(X1'''', X2''''), X2''))
two new Dependency Pairs are created:

ACTIVATE(ng(nf(nf(nf(X1'''''', X2'''''''), X2'''''), X2'''))) -> ACTIVATE(nf(nf(nf(X1'''''', X2'''''''), X2'''''), X2'''))
ACTIVATE(ng(nf(nf(ng(X''''''), X2''''''), X2'''))) -> ACTIVATE(nf(nf(ng(X''''''), X2''''''), X2'''))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

ACTIVATE(nf(ng(nf(ng(X''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))
ACTIVATE(ng(nf(nf(ng(X''''''), X2''''''), X2'''))) -> ACTIVATE(nf(nf(ng(X''''''), X2''''''), X2'''))
ACTIVATE(nf(ng(nf(nf(X1'''''', X2''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(nf(nf(ng(X''''), X2'''), X2)) -> ACTIVATE(nf(ng(X''''), X2'''))
ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))
ACTIVATE(ng(nf(nf(nf(X1'''''', X2'''''''), X2'''''), X2'''))) -> ACTIVATE(nf(nf(nf(X1'''''', X2'''''''), X2'''''), X2'''))
ACTIVATE(ng(ng(nf(nf(X1'''''', X2''''''), X2'''')))) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(ng(ng(ng(X'''')))) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(nf(ng(ng(X'''')), X2)) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(ng(nf(ng(X''''), X2''))) -> ACTIVATE(nf(ng(X''''), X2''))
ACTIVATE(ng(ng(nf(ng(X''''''), X2'''')))) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




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

ACTIVATE(ng(nf(ng(X''''), X2''))) -> ACTIVATE(nf(ng(X''''), X2''))
three new Dependency Pairs are created:

ACTIVATE(ng(nf(ng(ng(X'''''')), X2'''))) -> ACTIVATE(nf(ng(ng(X'''''')), X2'''))
ACTIVATE(ng(nf(ng(nf(nf(X1'''''''', X2''''''''), X2'''''')), X2'''))) -> ACTIVATE(nf(ng(nf(nf(X1'''''''', X2''''''''), X2'''''')), X2'''))
ACTIVATE(ng(nf(ng(nf(ng(X''''''''), X2'''''')), X2'''))) -> ACTIVATE(nf(ng(nf(ng(X''''''''), X2'''''')), X2'''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 8
                 ↳Polynomial Ordering


Dependency Pairs:

ACTIVATE(ng(nf(ng(nf(ng(X''''''''), X2'''''')), X2'''))) -> ACTIVATE(nf(ng(nf(ng(X''''''''), X2'''''')), X2'''))
ACTIVATE(ng(nf(ng(nf(nf(X1'''''''', X2''''''''), X2'''''')), X2'''))) -> ACTIVATE(nf(ng(nf(nf(X1'''''''', X2''''''''), X2'''''')), X2'''))
ACTIVATE(ng(ng(nf(ng(X''''''), X2'''')))) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))
ACTIVATE(ng(nf(nf(ng(X''''''), X2''''''), X2'''))) -> ACTIVATE(nf(nf(ng(X''''''), X2''''''), X2'''))
ACTIVATE(nf(ng(nf(nf(X1'''''', X2''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(nf(nf(ng(X''''), X2'''), X2)) -> ACTIVATE(nf(ng(X''''), X2'''))
ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))
ACTIVATE(ng(nf(nf(nf(X1'''''', X2'''''''), X2'''''), X2'''))) -> ACTIVATE(nf(nf(nf(X1'''''', X2'''''''), X2'''''), X2'''))
ACTIVATE(ng(ng(nf(nf(X1'''''', X2''''''), X2'''')))) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(ng(ng(ng(X'''')))) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(nf(ng(ng(X'''')), X2)) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(ng(nf(ng(ng(X'''''')), X2'''))) -> ACTIVATE(nf(ng(ng(X'''''')), X2'''))
ACTIVATE(nf(ng(nf(ng(X''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




The following dependency pairs can be strictly oriented:

ACTIVATE(ng(nf(ng(nf(ng(X''''''''), X2'''''')), X2'''))) -> ACTIVATE(nf(ng(nf(ng(X''''''''), X2'''''')), X2'''))
ACTIVATE(ng(nf(ng(nf(nf(X1'''''''', X2''''''''), X2'''''')), X2'''))) -> ACTIVATE(nf(ng(nf(nf(X1'''''''', X2''''''''), X2'''''')), X2'''))
ACTIVATE(ng(ng(nf(ng(X''''''), X2'''')))) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))
ACTIVATE(ng(nf(nf(ng(X''''''), X2''''''), X2'''))) -> ACTIVATE(nf(nf(ng(X''''''), X2''''''), X2'''))
ACTIVATE(ng(nf(nf(nf(X1'''''', X2'''''''), X2'''''), X2'''))) -> ACTIVATE(nf(nf(nf(X1'''''', X2'''''''), X2'''''), X2'''))
ACTIVATE(ng(ng(nf(nf(X1'''''', X2''''''), X2'''')))) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(ng(ng(ng(X'''')))) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(ng(nf(ng(ng(X'''''')), X2'''))) -> ACTIVATE(nf(ng(ng(X'''''')), X2'''))


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(n__f(x1, x2))=  x1  
  POL(n__g(x1))=  1 + x1  
  POL(ACTIVATE(x1))=  1 + x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 9
                 ↳Dependency Graph


Dependency Pairs:

ACTIVATE(nf(ng(nf(nf(X1'''''', X2''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(nf(X1'''''', X2''''''), X2'''')))
ACTIVATE(nf(nf(ng(X''''), X2'''), X2)) -> ACTIVATE(nf(ng(X''''), X2'''))
ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))
ACTIVATE(nf(ng(ng(X'''')), X2)) -> ACTIVATE(ng(ng(X'''')))
ACTIVATE(nf(ng(nf(ng(X''''''), X2'''')), X2)) -> ACTIVATE(ng(nf(ng(X''''''), X2'''')))


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 10
                 ↳Polynomial Ordering


Dependency Pair:

ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




The following dependency pair can be strictly oriented:

ACTIVATE(nf(nf(nf(X1'''', X2'''''), X2''''), X2)) -> ACTIVATE(nf(nf(X1'''', X2'''''), X2''''))


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(n__f(x1, x2))=  1 + x1  
  POL(ACTIVATE(x1))=  1 + x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 11
                 ↳Dependency Graph


Dependency Pair:


Rules:


f(g(X), Y) -> f(X, nf(ng(X), activate(Y)))
f(X1, X2) -> nf(X1, X2)
g(X) -> ng(X)
activate(nf(X1, X2)) -> f(activate(X1), X2)
activate(ng(X)) -> g(activate(X))
activate(X) -> X


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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