Term Rewriting System R:
[X, Y, N, M]
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

EQ(s(X), s(Y)) -> EQ(X, Y)
RM(N, add(M, X)) -> IFRM(eq(N, M), N, add(M, X))
RM(N, add(M, X)) -> EQ(N, M)
IFRM(true, N, add(M, X)) -> RM(N, X)
IFRM(false, N, add(M, X)) -> RM(N, X)
PURGE(add(N, X)) -> PURGE(rm(N, X))
PURGE(add(N, X)) -> RM(N, X)

Furthermore, R contains three SCCs. 


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


Dependency Pair:

EQ(s(X), s(Y)) -> EQ(X, Y)


Rules:


eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))


Strategy:

innermost




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


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


Dependency Pair:

EQ(s(X), s(Y)) -> EQ(X, Y)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. EQ(s(X), s(Y)) -> EQ(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)
       →DP Problem 3
         ↳UsableRules


Dependency Pairs:

IFRM(false, N, add(M, X)) -> RM(N, X)
IFRM(true, N, add(M, X)) -> RM(N, X)
RM(N, add(M, X)) -> IFRM(eq(N, M), N, add(M, X))


Rules:


eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))


Strategy:

innermost




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


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


Dependency Pairs:

IFRM(false, N, add(M, X)) -> RM(N, X)
IFRM(true, N, add(M, X)) -> RM(N, X)
RM(N, add(M, X)) -> IFRM(eq(N, M), N, add(M, X))


Rules:


eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), s(Y)) -> eq(X, Y)
eq(s(X), 0) -> false


Strategy:

innermost




We number the DPs as follows:
  1. IFRM(false, N, add(M, X)) -> RM(N, X)
  2. IFRM(true, N, add(M, X)) -> RM(N, X)
  3. RM(N, add(M, X)) -> IFRM(eq(N, M), N, add(M, X))
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
2=1
3>2
{3} , {3}
1=2
2=3

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

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
add(x1, x2) -> add(x1, x2)

We obtain no new DP problems. 


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


Dependency Pair:

PURGE(add(N, X)) -> PURGE(rm(N, X))


Rules:


eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, 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 3
         ↳UsableRules
           →DP Problem 6
             ↳Negative Polynomial Order


Dependency Pair:

PURGE(add(N, X)) -> PURGE(rm(N, X))


Rules:


eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), s(Y)) -> eq(X, Y)
eq(s(X), 0) -> false
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))


Strategy:

innermost




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

PURGE(add(N, X)) -> PURGE(rm(N, X))


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

eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), s(Y)) -> eq(X, Y)
eq(s(X), 0) -> false
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))


Used ordering:
Polynomial Order with Interpretation:

POL( PURGE(x1) ) = x1

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

POL( rm(x1, x2) ) = x2

POL( eq(x1, x2) ) = 0

POL( true ) = 0

POL( false ) = 0

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

POL( nil ) = 0


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 6
             ↳Neg POLO
             ...
               →DP Problem 7
                 ↳Dependency Graph


Dependency Pair:


Rules:


eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), s(Y)) -> eq(X, Y)
eq(s(X), 0) -> false
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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