Term Rewriting System R:
[x, y]
p(0) -> 0
p(s(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
Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.


   R
OC
       →TRS2
Dependency Pair Analysis



R contains the following Dependency Pairs:

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 two SCCs.


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


Dependency Pair:

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


Rules:


p(0) -> 0
p(s(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 8 non-usable-rules.


   R
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
             ...
               →DP Problem 3
Size-Change Principle
           →DP Problem 2
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. LE(s(x), s(y)) -> LE(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
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
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) -> 0
p(s(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 3 non-usable-rules.


   R
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
             ...
               →DP Problem 4
Narrowing Transformation


Dependency Pairs:

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


Rules:


p(s(x)) -> x
p(0) -> 0
le(s(x), s(y)) -> le(x, y)
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
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
             ...
               →DP Problem 5
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(s(x)) -> x
p(0) -> 0
le(s(x), s(y)) -> le(x, y)
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, s(x''), y) -> MINUS(x'', y)
IF(false, 0, y) -> MINUS(0, y)

The transformation is resulting in one new DP problem:



   R
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
             ...
               →DP Problem 6
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(s(x)) -> x
p(0) -> 0
le(s(x), s(y)) -> le(x, y)
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
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
             ...
               →DP Problem 7
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(s(x)) -> x
p(0) -> 0
le(s(x), s(y)) -> le(x, y)
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
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
             ...
               →DP Problem 9
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(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
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
             ...
               →DP Problem 8
Usable Rules (Innermost)


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




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


   R
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
             ...
               →DP Problem 10
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