Term Rewriting System R:
[x, y, z]
p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x), y) -> PLUS(p(s(x)), y)
PLUS(s(x), y) -> P(s(x))
PLUS(x, s(y)) -> PLUS(x, p(s(y)))
PLUS(x, s(y)) -> P(s(y))
TIMES(s(x), y) -> PLUS(y, times(x, y))
TIMES(s(x), y) -> TIMES(x, y)
DIV(x, y) -> QUOT(x, y, y)
DIV(div(x, y), z) -> DIV(x, times(y, z))
DIV(div(x, y), z) -> TIMES(y, z)
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
QUOT(x, 0, s(z)) -> DIV(x, s(z))
EQ(s(x), s(y)) -> EQ(x, y)
DIVIDES(y, x) -> EQ(x, times(div(x, y), y))
DIVIDES(y, x) -> TIMES(div(x, y), y)
DIVIDES(y, x) -> DIV(x, y)
PRIME(s(s(x))) -> PR(s(s(x)), s(x))
PR(x, s(s(y))) -> IF(divides(s(s(y)), x), x, s(y))
PR(x, s(s(y))) -> DIVIDES(s(s(y)), x)
IF(false, x, y) -> PR(x, y)

Furthermore, R contains five SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Modular Removal of Rules
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
       →DP Problem 5
         ↳SCP


Dependency Pairs:

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


Rules:


p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)





We have the following set of usable rules:

p(s(x)) -> x
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(PLUS(x1, x2))=  1 + x1 + x2  
  POL(s(x1))=  x1  
  POL(p(x1))=  x1  

We have the following set D of usable symbols: {PLUS, s, p}
No Dependency Pairs can be deleted.
24 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 6
             ↳Modular Removal of Rules
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
       →DP Problem 5
         ↳SCP


Dependency Pairs:

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


Rule:


p(s(x)) -> x





We have the following set of usable rules:

p(s(x)) -> x
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(PLUS(x1, x2))=  1 + x1 + x2  
  POL(s(x1))=  1 + x1  
  POL(p(x1))=  x1  

We have the following set D of usable symbols: {PLUS, s, p}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

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

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

p(s(x)) -> x


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 6
             ↳MRR
             ...
               →DP Problem 7
                 ↳Dependency Graph
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
       →DP Problem 5
         ↳SCP


Dependency Pairs:

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


Rule:

none





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


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 6
             ↳MRR
             ...
               →DP Problem 8
                 ↳Non-Overlappingness Check
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
       →DP Problem 5
         ↳SCP


Dependency Pairs:

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


Rule:

none





R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle: 


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 6
             ↳MRR
             ...
               →DP Problem 9
                 ↳Instantiation Transformation
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
       →DP Problem 5
         ↳SCP


Dependency Pairs:

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


Rule:

none


Strategy:

innermost




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

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

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

The transformation is resulting in no new DP problems. 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳Size-Change Principle
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
       →DP Problem 5
         ↳SCP


Dependency Pair:

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


Rules:


p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)





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
         ↳MRR
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳Size-Change Principle
       →DP Problem 4
         ↳AFS
       →DP Problem 5
         ↳SCP


Dependency Pair:

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


Rules:


p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)





We number the DPs as follows:
  1. TIMES(s(x), y) -> TIMES(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
         ↳MRR
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳Argument Filtering and Ordering
       →DP Problem 5
         ↳SCP


Dependency Pairs:

DIV(div(x, y), z) -> DIV(x, times(y, z))
QUOT(x, 0, s(z)) -> DIV(x, s(z))
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
DIV(x, y) -> QUOT(x, y, y)


Rules:


p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)





The following dependency pair can be strictly oriented:

QUOT(s(x), s(y), z) -> QUOT(x, y, z)


There are no usable rules w.r.t. the AFS that need to be oriented.
Used ordering: Lexicographic Path Order with Precedence:
trivial

resulting in one new DP problem.
Used Argument Filtering System:
DIV(x1, x2) -> x1
div(x1, x2) -> x1
QUOT(x1, x2, x3) -> x1
s(x1) -> s(x1)


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
           →DP Problem 10
             ↳Argument Filtering and Ordering
       →DP Problem 5
         ↳SCP


Dependency Pairs:

DIV(div(x, y), z) -> DIV(x, times(y, z))
QUOT(x, 0, s(z)) -> DIV(x, s(z))
DIV(x, y) -> QUOT(x, y, y)


Rules:


p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)





The following dependency pair can be strictly oriented:

DIV(div(x, y), z) -> DIV(x, times(y, z))


There are no usable rules w.r.t. the AFS that need to be oriented.
Used ordering: Lexicographic Path Order with Precedence:
trivial

resulting in one new DP problem.
Used Argument Filtering System:
DIV(x1, x2) -> x1
div(x1, x2) -> div(x1, x2)
QUOT(x1, x2, x3) -> x1


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
           →DP Problem 10
             ↳AFS
             ...
               →DP Problem 11
                 ↳Instantiation Transformation
       →DP Problem 5
         ↳SCP


Dependency Pairs:

QUOT(x, 0, s(z)) -> DIV(x, s(z))
DIV(x, y) -> QUOT(x, y, y)


Rules:


p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)





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

DIV(x, y) -> QUOT(x, y, y)
one new Dependency Pair is created:

DIV(x'', s(z'')) -> QUOT(x'', s(z''), s(z''))

The transformation is resulting in no new DP problems. 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳AFS
       →DP Problem 5
         ↳Size-Change Principle


Dependency Pairs:

IF(false, x, y) -> PR(x, y)
PR(x, s(s(y))) -> IF(divides(s(s(y)), x), x, s(y))


Rules:


p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)





We number the DPs as follows:
  1. IF(false, x, y) -> PR(x, y)
  2. PR(x, s(s(y))) -> IF(divides(s(s(y)), x), x, s(y))
and get the following Size-Change Graph(s):
{1} , {1}
2=1
3=2
{2} , {2}
1=2
2>3

which lead(s) to this/these maximal multigraph(s):
{2} , {1}
1=1
2>2
{1} , {2}
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:
s(x1) -> s(x1)

We obtain no new DP problems.

Termination of R successfully shown.
Duration:
0:02 minutes