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

Innermost Termination of R to be shown.



   R
Removing Redundant Rules for Innermost Termination



Removing the following rules from R which left hand sides contain non normal subterms

p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)


   R
RRRI
       →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
RRRI
       →TRS2
DPs
           →DP Problem 1
Non-Overlappingness Check
           →DP Problem 2
NOC


Dependency Pair:

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


Rules:


p(0) -> s(s(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))





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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
             ...
               →DP Problem 3
Usable Rules (Innermost)
           →DP Problem 2
NOC


Dependency Pair:

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


Rules:


p(0) -> s(s(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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
             ...
               →DP Problem 4
Size-Change Principle
           →DP Problem 2
NOC


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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
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
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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
NOC
             ...
               →DP Problem 5
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
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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
NOC
             ...
               →DP Problem 6
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(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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
NOC
             ...
               →DP Problem 7
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(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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
NOC
             ...
               →DP Problem 8
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(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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
NOC
             ...
               →DP Problem 9
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(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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
NOC
             ...
               →DP Problem 11
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):
{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.


   R
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
NOC
             ...
               →DP Problem 10
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(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
RRRI
       →TRS2
DPs
           →DP Problem 1
NOC
           →DP Problem 2
NOC
             ...
               →DP Problem 12
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.

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