Term Rewriting System R:
[y, x, z]
app(app(le, 0), y) -> true
app(app(le, app(s, x)), 0) -> false
app(app(le, app(s, x)), app(s, y)) -> app(app(le, x), y)
app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, y)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(app(if, true), x), y) -> x
app(app(app(if, false), x), y) -> y
app(minsort, nil) -> nil
app(minsort, app(app(cons, x), y)) -> app(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y))))
app(app(min, x), nil) -> x
app(app(min, x), app(app(cons, y), z)) -> app(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z))
app(app(del, x), nil) -> nil
app(app(del, x), app(app(cons, y), z)) -> app(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z)))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

APP(app(le, app(s, x)), app(s, y)) -> APP(app(le, x), y)
APP(app(le, app(s, x)), app(s, y)) -> APP(le, x)
APP(app(eq, app(s, x)), app(s, y)) -> APP(app(eq, x), y)
APP(app(eq, app(s, x)), app(s, y)) -> APP(eq, x)
APP(minsort, app(app(cons, x), y)) -> APP(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y))))
APP(minsort, app(app(cons, x), y)) -> APP(cons, app(app(min, x), y))
APP(minsort, app(app(cons, x), y)) -> APP(app(min, x), y)
APP(minsort, app(app(cons, x), y)) -> APP(min, x)
APP(minsort, app(app(cons, x), y)) -> APP(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y)))
APP(minsort, app(app(cons, x), y)) -> APP(app(del, app(app(min, x), y)), app(app(cons, x), y))
APP(minsort, app(app(cons, x), y)) -> APP(del, app(app(min, x), y))
APP(app(min, x), app(app(cons, y), z)) -> APP(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z))
APP(app(min, x), app(app(cons, y), z)) -> APP(app(if, app(app(le, x), y)), app(app(min, x), z))
APP(app(min, x), app(app(cons, y), z)) -> APP(if, app(app(le, x), y))
APP(app(min, x), app(app(cons, y), z)) -> APP(app(le, x), y)
APP(app(min, x), app(app(cons, y), z)) -> APP(le, x)
APP(app(min, x), app(app(cons, y), z)) -> APP(app(min, x), z)
APP(app(min, x), app(app(cons, y), z)) -> APP(app(min, y), z)
APP(app(min, x), app(app(cons, y), z)) -> APP(min, y)
APP(app(del, x), app(app(cons, y), z)) -> APP(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z)))
APP(app(del, x), app(app(cons, y), z)) -> APP(app(if, app(app(eq, x), y)), z)
APP(app(del, x), app(app(cons, y), z)) -> APP(if, app(app(eq, x), y))
APP(app(del, x), app(app(cons, y), z)) -> APP(app(eq, x), y)
APP(app(del, x), app(app(cons, y), z)) -> APP(eq, x)
APP(app(del, x), app(app(cons, y), z)) -> APP(app(cons, y), app(app(del, x), z))
APP(app(del, x), app(app(cons, y), z)) -> APP(app(del, x), z)

Furthermore, R contains five SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Usable Rules (Innermost)
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

APP(app(le, app(s, x)), app(s, y)) -> APP(app(le, x), y)


Rules:


app(app(le, 0), y) -> true
app(app(le, app(s, x)), 0) -> false
app(app(le, app(s, x)), app(s, y)) -> app(app(le, x), y)
app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, y)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(app(if, true), x), y) -> x
app(app(app(if, false), x), y) -> y
app(minsort, nil) -> nil
app(minsort, app(app(cons, x), y)) -> app(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y))))
app(app(min, x), nil) -> x
app(app(min, x), app(app(cons, y), z)) -> app(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z))
app(app(del, x), nil) -> nil
app(app(del, x), app(app(cons, y), z)) -> app(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z)))


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 6
             ↳A-Transformation
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

APP(app(le, app(s, x)), app(s, y)) -> APP(app(le, x), y)


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 6
             ↳ATrans
             ...
               →DP Problem 7
                 ↳Size-Change Principle
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳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
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳Usable Rules (Innermost)
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

APP(app(eq, app(s, x)), app(s, y)) -> APP(app(eq, x), y)


Rules:


app(app(le, 0), y) -> true
app(app(le, app(s, x)), 0) -> false
app(app(le, app(s, x)), app(s, y)) -> app(app(le, x), y)
app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, y)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(app(if, true), x), y) -> x
app(app(app(if, false), x), y) -> y
app(minsort, nil) -> nil
app(minsort, app(app(cons, x), y)) -> app(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y))))
app(app(min, x), nil) -> x
app(app(min, x), app(app(cons, y), z)) -> app(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z))
app(app(del, x), nil) -> nil
app(app(del, x), app(app(cons, y), z)) -> app(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z)))


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 8
             ↳A-Transformation
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

APP(app(eq, app(s, x)), app(s, y)) -> APP(app(eq, x), y)


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 8
             ↳ATrans
             ...
               →DP Problem 9
                 ↳Size-Change Principle
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




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


Dependency Pairs:

APP(app(min, x), app(app(cons, y), z)) -> APP(app(min, y), z)
APP(app(min, x), app(app(cons, y), z)) -> APP(app(min, x), z)


Rules:


app(app(le, 0), y) -> true
app(app(le, app(s, x)), 0) -> false
app(app(le, app(s, x)), app(s, y)) -> app(app(le, x), y)
app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, y)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(app(if, true), x), y) -> x
app(app(app(if, false), x), y) -> y
app(minsort, nil) -> nil
app(minsort, app(app(cons, x), y)) -> app(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y))))
app(app(min, x), nil) -> x
app(app(min, x), app(app(cons, y), z)) -> app(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z))
app(app(del, x), nil) -> nil
app(app(del, x), app(app(cons, y), z)) -> app(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z)))


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 10
             ↳A-Transformation
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pairs:

APP(app(min, x), app(app(cons, y), z)) -> APP(app(min, y), z)
APP(app(min, x), app(app(cons, y), z)) -> APP(app(min, x), z)


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 10
             ↳ATrans
             ...
               →DP Problem 11
                 ↳Size-Change Principle
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pairs:

MIN(x, cons(y, z)) -> MIN(y, z)
MIN(x, cons(y, z)) -> MIN(x, z)


Rule:

none


Strategy:

innermost




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

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

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳Usable Rules (Innermost)
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

APP(app(del, x), app(app(cons, y), z)) -> APP(app(del, x), z)


Rules:


app(app(le, 0), y) -> true
app(app(le, app(s, x)), 0) -> false
app(app(le, app(s, x)), app(s, y)) -> app(app(le, x), y)
app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, y)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(app(if, true), x), y) -> x
app(app(app(if, false), x), y) -> y
app(minsort, nil) -> nil
app(minsort, app(app(cons, x), y)) -> app(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y))))
app(app(min, x), nil) -> x
app(app(min, x), app(app(cons, y), z)) -> app(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z))
app(app(del, x), nil) -> nil
app(app(del, x), app(app(cons, y), z)) -> app(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z)))


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
           →DP Problem 12
             ↳A-Transformation
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

APP(app(del, x), app(app(cons, y), z)) -> APP(app(del, x), z)


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
           →DP Problem 12
             ↳ATrans
             ...
               →DP Problem 13
                 ↳Size-Change Principle
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

DEL(x, cons(y, z)) -> DEL(x, z)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. DEL(x, cons(y, z)) -> DEL(x, z)
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:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳Usable Rules (Innermost)


Dependency Pair:

APP(minsort, app(app(cons, x), y)) -> APP(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y)))


Rules:


app(app(le, 0), y) -> true
app(app(le, app(s, x)), 0) -> false
app(app(le, app(s, x)), app(s, y)) -> app(app(le, x), y)
app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, y)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(app(if, true), x), y) -> x
app(app(app(if, false), x), y) -> y
app(minsort, nil) -> nil
app(minsort, app(app(cons, x), y)) -> app(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y))))
app(app(min, x), nil) -> x
app(app(min, x), app(app(cons, y), z)) -> app(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z))
app(app(del, x), nil) -> nil
app(app(del, x), app(app(cons, y), z)) -> app(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z)))


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules
           →DP Problem 14
             ↳A-Transformation


Dependency Pair:

APP(minsort, app(app(cons, x), y)) -> APP(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y)))


Rules:


app(app(del, x), app(app(cons, y), z)) -> app(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z)))
app(app(le, app(s, x)), 0) -> false
app(app(le, 0), y) -> true
app(app(min, x), nil) -> x
app(app(eq, 0), app(s, y)) -> false
app(app(le, app(s, x)), app(s, y)) -> app(app(le, x), y)
app(app(min, x), app(app(cons, y), z)) -> app(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z))
app(app(eq, 0), 0) -> true
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(app(if, false), x), y) -> y
app(app(app(if, true), x), y) -> x
app(app(eq, app(s, x)), 0) -> false
app(app(del, x), nil) -> nil


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules
           →DP Problem 14
             ↳ATrans
             ...
               →DP Problem 15
                 ↳Narrowing Transformation


Dependency Pair:

MINSORT(cons(x, y)) -> MINSORT(del(min(x, y), cons(x, y)))


Rules:


del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))
del(x, nil) -> nil
if(false, x, y) -> y
if(true, x, y) -> x
eq(0, s(y)) -> false
eq(0, 0) -> true
eq(s(x), s(y)) -> eq(x, y)
eq(s(x), 0) -> false
le(s(x), 0) -> false
le(0, y) -> true
le(s(x), s(y)) -> le(x, y)
min(x, nil) -> x
min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z))


Strategy:

innermost




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

MINSORT(cons(x, y)) -> MINSORT(del(min(x, y), cons(x, y)))
three new Dependency Pairs are created:

MINSORT(cons(x'', y'')) -> MINSORT(if(eq(min(x'', y''), x''), y'', cons(x'', del(min(x'', y''), y''))))
MINSORT(cons(x'', nil)) -> MINSORT(del(x'', cons(x'', nil)))
MINSORT(cons(x'', cons(y'', z'))) -> MINSORT(del(if(le(x'', y''), min(x'', z'), min(y'', z')), cons(x'', cons(y'', z'))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules
           →DP Problem 14
             ↳ATrans
             ...
               →DP Problem 16
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

MINSORT(cons(x'', cons(y'', z'))) -> MINSORT(del(if(le(x'', y''), min(x'', z'), min(y'', z')), cons(x'', cons(y'', z'))))
MINSORT(cons(x'', nil)) -> MINSORT(del(x'', cons(x'', nil)))
MINSORT(cons(x'', y'')) -> MINSORT(if(eq(min(x'', y''), x''), y'', cons(x'', del(min(x'', y''), y''))))


Rules:


del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))
del(x, nil) -> nil
if(false, x, y) -> y
if(true, x, y) -> x
eq(0, s(y)) -> false
eq(0, 0) -> true
eq(s(x), s(y)) -> eq(x, y)
eq(s(x), 0) -> false
le(s(x), 0) -> false
le(0, y) -> true
le(s(x), s(y)) -> le(x, y)
min(x, nil) -> x
min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z))


Strategy:

innermost



The Proof could not be continued due to a Timeout.
Innermost Termination of R could not be shown.
Duration:
1:00 minutes