Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
    ↳5 QDP
        ↳6 QDPSizeChangeProof (⇔)
        ↳7 TRUE
    ↳8 QDP
        ↳9 QDPSizeChangeProof (⇔)
        ↳10 TRUE
    ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 TRUE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following 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)))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 2 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EQ(s(X), s(Y)) → EQ(X, Y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPSizeChangeProof (EQUIVALENT transformation)

We used the following order and afs together with the size-change analysis [AAECC05] to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
s(x1)  =  s(x1)

From the DPs we obtained the following set of size-change graphs:

  • EQ(s(X), s(Y)) → EQ(X, Y) (allowed arguments on rhs = {1, 2})
    The graph contains the following edges 1 > 1, 2 > 2

We oriented the following set of usable rules [AAECC05,FROCOS05]. none

(7) TRUE

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)) → RM(N, X)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(9) QDPSizeChangeProof (EQUIVALENT transformation)

We used the following order and afs together with the size-change analysis [AAECC05] to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
true  =  true
false  =  false
add(x1, x2)  =  add(x2)

From the DPs we obtained the following set of size-change graphs:

  • RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X)) (allowed arguments on rhs = {2, 3})
    The graph contains the following edges 1 >= 2, 2 >= 3

  • IFRM(true, N, add(M, X)) → RM(N, X) (allowed arguments on rhs = {1, 2})
    The graph contains the following edges 2 >= 1, 3 > 2

  • IFRM(false, N, add(M, X)) → RM(N, X) (allowed arguments on rhs = {1, 2})
    The graph contains the following edges 2 >= 1, 3 > 2

We oriented the following set of usable rules [AAECC05,FROCOS05]. none

(10) TRUE

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PURGE(add(N, X)) → PURGE(rm(N, X))

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

We used the following order together with the size-change analysis [AAECC05] to show that there are no infinite chains for this DP problem.

Order:Polynomial interpretation [POLO]:


POL(0) = 0   
POL(add(x1, x2)) = 1 + x2   
POL(eq(x1, x2)) = 0   
POL(false) = 0   
POL(ifrm(x1, x2, x3)) = x3   
POL(nil) = 0   
POL(rm(x1, x2)) = x2   
POL(s(x1)) = 0   
POL(true) = 0   

From the DPs we obtained the following set of size-change graphs:

  • PURGE(add(N, X)) → PURGE(rm(N, X)) (allowed arguments on rhs = {1})
    The graph contains the following edges 1 > 1

We oriented the following set of usable rules [AAECC05,FROCOS05].


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))

(13) TRUE