Term Rewriting System R:
[x, y]
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

P(p(s(x))) -> P(x)
LE(p(s(x)), x) -> LE(x, x)
LE(s(x), s(y)) -> LE(x, y)
MINUS(x, y) -> IF(le(x, y), x, y)
MINUS(x, y) -> LE(x, y)
IF(false, x, y) -> MINUS(p(x), y)
IF(false, x, y) -> P(x)

Furthermore, R contains three SCCs. 


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


Dependency Pair:

P(p(s(x))) -> P(x)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))





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

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

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)
p(x1) -> p(x1)

We obtain no new DP problems. 


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


Dependency Pairs:

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


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))





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

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

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳Non-Overlappingness Check


Dependency Pairs:

IF(false, x, y) -> MINUS(p(x), y)
MINUS(x, y) -> IF(le(x, y), x, y)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))





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
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳NOC
           →DP Problem 4
             ↳Usable Rules (Innermost)


Dependency Pairs:

IF(false, x, y) -> MINUS(p(x), y)
MINUS(x, y) -> IF(le(x, y), x, y)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳NOC
           →DP Problem 4
             ↳UsableRules
             ...
               →DP Problem 5
                 ↳Narrowing Transformation


Dependency Pairs:

IF(false, x, y) -> MINUS(p(x), y)
MINUS(x, y) -> IF(le(x, y), x, y)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
le(s(x), s(y)) -> le(x, y)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false


Strategy:

innermost




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

MINUS(x, y) -> IF(le(x, y), x, y)
three new Dependency Pairs are created:

MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
MINUS(0, y'') -> IF(true, 0, y'')
MINUS(s(x''), 0) -> IF(false, s(x''), 0)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳NOC
           →DP Problem 4
             ↳UsableRules
             ...
               →DP Problem 6
                 ↳Narrowing Transformation


Dependency Pairs:

MINUS(s(x''), 0) -> IF(false, s(x''), 0)
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
IF(false, x, y) -> MINUS(p(x), y)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
le(s(x), s(y)) -> le(x, y)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false


Strategy:

innermost




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

IF(false, x, y) -> MINUS(p(x), y)
two new Dependency Pairs are created:

IF(false, 0, y) -> MINUS(s(s(0)), y)
IF(false, s(x''), y) -> MINUS(x'', y)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳NOC
           →DP Problem 4
             ↳UsableRules
             ...
               →DP Problem 7
                 ↳Instantiation Transformation


Dependency Pairs:

MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
IF(false, s(x''), y) -> MINUS(x'', y)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
le(s(x), s(y)) -> le(x, y)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false


Strategy:

innermost




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

IF(false, s(x''), y) -> MINUS(x'', y)
two new Dependency Pairs are created:

IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
IF(false, s(x''''), 0) -> MINUS(x'''', 0)

The transformation is resulting in two new DP problems: 



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳NOC
           →DP Problem 4
             ↳UsableRules
             ...
               →DP Problem 8
                 ↳Usable Rules (Innermost)


Dependency Pairs:

IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
le(s(x), s(y)) -> le(x, y)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳NOC
           →DP Problem 4
             ↳UsableRules
             ...
               →DP Problem 10
                 ↳Size-Change Principle


Dependency Pairs:

IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))


Rules:


le(s(x), s(y)) -> le(x, y)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false


Strategy:

innermost




We number the DPs as follows:
  1. IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
  2. MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(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. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳NOC
           →DP Problem 4
             ↳UsableRules
             ...
               →DP Problem 9
                 ↳Usable Rules (Innermost)


Dependency Pairs:

IF(false, s(x''''), 0) -> MINUS(x'''', 0)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
le(s(x), s(y)) -> le(x, y)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳NOC
           →DP Problem 4
             ↳UsableRules
             ...
               →DP Problem 11
                 ↳Size-Change Principle


Dependency Pairs:

IF(false, s(x''''), 0) -> MINUS(x'''', 0)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. IF(false, s(x''''), 0) -> MINUS(x'''', 0)
  2. MINUS(s(x''), 0) -> IF(false, s(x''), 0)
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):
{1} , {2}
2>2
3=3
{2} , {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.

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