Term Rewriting System R:
[x, y]
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
p(s(x)) -> x
f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x)))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

-'(s(x), s(y)) -> -'(x, y)
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
F(s(x), y) -> P(-(s(x), y))
F(s(x), y) -> -'(s(x), y)
F(s(x), y) -> P(-(y, s(x)))
F(s(x), y) -> -'(y, s(x))
F(x, s(y)) -> F(p(-(x, s(y))), p(-(s(y), x)))
F(x, s(y)) -> P(-(x, s(y)))
F(x, s(y)) -> -'(x, s(y))
F(x, s(y)) -> P(-(s(y), x))
F(x, s(y)) -> -'(s(y), x)

Furthermore, R contains two SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Usable Rules (Innermost)
       →DP Problem 2
         ↳UsableRules


Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)


Rules:


-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
p(s(x)) -> x
f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x)))


Strategy:

innermost




As we are in the innermost case, we can delete all 5 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 3
             ↳Size-Change Principle
       →DP Problem 2
         ↳UsableRules


Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. -'(s(x), s(y)) -> -'(x, y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

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

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳Usable Rules (Innermost)


Dependency Pairs:

F(x, s(y)) -> F(p(-(x, s(y))), p(-(s(y), x)))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))


Rules:


-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
p(s(x)) -> x
f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x)))


Strategy:

innermost




As we are in the innermost case, we can delete all 2 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 4
             ↳Narrowing Transformation


Dependency Pairs:

F(x, s(y)) -> F(p(-(x, s(y))), p(-(s(y), x)))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))


Rules:


-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Strategy:

innermost




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

F(x, s(y)) -> F(p(-(x, s(y))), p(-(s(y), x)))
three new Dependency Pairs are created:

F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(y''), s(y0)) -> F(p(-(s(y''), s(y0))), p(-(y0, y'')))
F(0, s(y')) -> F(p(-(0, s(y'))), p(s(y')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 4
             ↳Nar
             ...
               →DP Problem 5
                 ↳Rewriting Transformation


Dependency Pairs:

F(s(y''), s(y0)) -> F(p(-(s(y''), s(y0))), p(-(y0, y'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))


Rules:


-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Strategy:

innermost




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

F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
one new Dependency Pair is created:

F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 4
             ↳Nar
             ...
               →DP Problem 6
                 ↳Rewriting Transformation


Dependency Pairs:

F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
F(s(y''), s(y0)) -> F(p(-(s(y''), s(y0))), p(-(y0, y'')))


Rules:


-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Strategy:

innermost




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

F(s(y''), s(y0)) -> F(p(-(s(y''), s(y0))), p(-(y0, y'')))
one new Dependency Pair is created:

F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 4
             ↳Nar
             ...
               →DP Problem 7
                 ↳Narrowing Transformation


Dependency Pairs:

F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))


Rules:


-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Strategy:

innermost




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

F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
three new Dependency Pairs are created:

F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(x''), 0) -> F(p(s(x'')), p(-(0, s(x''))))
F(s(x0), s(x'')) -> F(p(-(s(x0), s(x''))), p(-(x'', x0)))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 4
             ↳Nar
             ...
               →DP Problem 8
                 ↳Rewriting Transformation


Dependency Pairs:

F(s(x0), s(x'')) -> F(p(-(s(x0), s(x''))), p(-(x'', x0)))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))


Rules:


-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Strategy:

innermost




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

F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
one new Dependency Pair is created:

F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 4
             ↳Nar
             ...
               →DP Problem 9
                 ↳Rewriting Transformation


Dependency Pairs:

F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(x0), s(x'')) -> F(p(-(s(x0), s(x''))), p(-(x'', x0)))


Rules:


-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Strategy:

innermost




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

F(s(x0), s(x'')) -> F(p(-(s(x0), s(x''))), p(-(x'', x0)))
one new Dependency Pair is created:

F(s(x0), s(x'')) -> F(p(-(x0, x'')), p(-(x'', x0)))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 4
             ↳Nar
             ...
               →DP Problem 10
                 ↳Negative Polynomial Order


Dependency Pairs:

F(s(x0), s(x'')) -> F(p(-(x0, x'')), p(-(x'', x0)))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))


Rules:


-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Strategy:

innermost




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

F(s(x0), s(x'')) -> F(p(-(x0, x'')), p(-(x'', x0)))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))


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

-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Used ordering:
Polynomial Order with Interpretation:

POL( F(x1, x2) ) = x2

POL( s(x1) ) = x1 + 1

POL( p(x1) ) = x1

POL( -(x1, x2) ) = x1


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 4
             ↳Nar
             ...
               →DP Problem 11
                 ↳Dependency Graph


Dependency Pair:


Rules:


-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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