Term Rewriting System R:
[x, y, z, k, l]
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

MINUS(s(x), s(y)) -> MINUS(x, y)
MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
MINUS(minus(x, y), z) -> PLUS(y, z)
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) -> MINUS(x, y)
PLUS(s(x), y) -> PLUS(x, y)
APP(cons(x, l), k) -> APP(l, k)
SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))
SUM(cons(x, cons(y, l))) -> PLUS(x, y)
SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))
SUM(app(l, cons(x, cons(y, k)))) -> APP(l, sum(cons(x, cons(y, k))))
SUM(app(l, cons(x, cons(y, k)))) -> SUM(cons(x, cons(y, k)))

Furthermore, R contains six SCCs.


   R
DPs
       →DP Problem 1
Forward Instantiation Transformation
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

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


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

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

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 7
Forward Instantiation Transformation
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

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


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

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

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 7
FwdInst
             ...
               →DP Problem 8
Polynomial Ordering
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

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


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(PLUS(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 7
FwdInst
             ...
               →DP Problem 9
Dependency Graph
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Forward Instantiation Transformation
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

APP(cons(x, l), k) -> APP(l, k)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

APP(cons(x, l), k) -> APP(l, k)
one new Dependency Pair is created:

APP(cons(x, cons(x'', l'')), k'') -> APP(cons(x'', l''), k'')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
           →DP Problem 10
Forward Instantiation Transformation
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

APP(cons(x, cons(x'', l'')), k'') -> APP(cons(x'', l''), k'')


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

APP(cons(x, cons(x'', l'')), k'') -> APP(cons(x'', l''), k'')
one new Dependency Pair is created:

APP(cons(x, cons(x'''', cons(x''''', l''''))), k'''') -> APP(cons(x'''', cons(x''''', l'''')), k'''')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
           →DP Problem 10
FwdInst
             ...
               →DP Problem 11
Polynomial Ordering
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

APP(cons(x, cons(x'''', cons(x''''', l''''))), k'''') -> APP(cons(x'''', cons(x''''', l'''')), k'''')


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




The following dependency pair can be strictly oriented:

APP(cons(x, cons(x'''', cons(x''''', l''''))), k'''') -> APP(cons(x'''', cons(x''''', l'''')), k'''')


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(cons(x1, x2))=  1 + x2  
  POL(APP(x1, x2))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
           →DP Problem 10
FwdInst
             ...
               →DP Problem 12
Dependency Graph
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Narrowing Transformation
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pairs:

MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
MINUS(s(x), s(y)) -> MINUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
one new Dependency Pair is created:

MINUS(minus(x, s(x'')), z') -> MINUS(x, s(plus(x'', z')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
           →DP Problem 13
Forward Instantiation Transformation
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

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


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

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

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
           →DP Problem 13
FwdInst
             ...
               →DP Problem 14
Forward Instantiation Transformation
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))
one new Dependency Pair is created:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
           →DP Problem 13
FwdInst
             ...
               →DP Problem 15
Polynomial Ordering
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




The following dependency pair can be strictly oriented:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(MINUS(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
           →DP Problem 13
FwdInst
             ...
               →DP Problem 16
Dependency Graph
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polynomial Ordering
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




The following dependency pair can be strictly oriented:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(plus(x1, x2))=  0  
  POL(0)=  0  
  POL(SUM(x1))=  x1  
  POL(cons(x1, x2))=  1 + x2  
  POL(s(x1))=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
           →DP Problem 17
Dependency Graph
       →DP Problem 5
Nar
       →DP Problem 6
Nar


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Narrowing Transformation
       →DP Problem 6
Nar


Dependency Pair:

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


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
three new Dependency Pairs are created:

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))
QUOT(s(minus(x'', y'')), s(y0)) -> QUOT(minus(x'', plus(y'', y0)), s(y0))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
           →DP Problem 18
Narrowing Transformation
       →DP Problem 6
Nar


Dependency Pairs:

QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))
QUOT(s(minus(x'', y'')), s(y0)) -> QUOT(minus(x'', plus(y'', y0)), s(y0))
QUOT(s(x''), s(0)) -> QUOT(x'', s(0))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))
three new Dependency Pairs are created:

QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
           →DP Problem 18
Nar
             ...
               →DP Problem 19
Narrowing Transformation
       →DP Problem 6
Nar


Dependency Pairs:

QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))
QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
QUOT(s(minus(x'', y'')), s(y0)) -> QUOT(minus(x'', plus(y'', y0)), s(y0))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

QUOT(s(minus(x'', y'')), s(y0)) -> QUOT(minus(x'', plus(y'', y0)), s(y0))
one new Dependency Pair is created:

QUOT(s(minus(x'', s(x'))), s(y0')) -> QUOT(minus(x'', s(plus(x', y0'))), s(y0'))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
           →DP Problem 18
Nar
             ...
               →DP Problem 20
Forward Instantiation Transformation
       →DP Problem 6
Nar


Dependency Pairs:

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
QUOT(s(minus(x'', s(x'))), s(y0')) -> QUOT(minus(x'', s(plus(x', y0'))), s(y0'))
QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
two new Dependency Pairs are created:

QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))
QUOT(s(s(minus(x'''', s(x'0')))), s(0)) -> QUOT(s(minus(x'''', s(x'0'))), s(0))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
           →DP Problem 18
Nar
             ...
               →DP Problem 21
Polynomial Ordering
       →DP Problem 6
Nar


Dependency Pairs:

QUOT(s(s(minus(x'''', s(x'0')))), s(0)) -> QUOT(s(minus(x'''', s(x'0'))), s(0))
QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))
QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(minus(x'', s(x'))), s(y0')) -> QUOT(minus(x'', s(plus(x', y0'))), s(y0'))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

QUOT(s(s(minus(x'''', s(x'0')))), s(0)) -> QUOT(s(minus(x'''', s(x'0'))), s(0))
QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))
QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(minus(x'', s(x'))), s(y0')) -> QUOT(minus(x'', s(plus(x', y0'))), s(y0'))


Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(plus(x1, x2))=  1 + x1  
  POL(QUOT(x1, x2))=  x1 + x2  
  POL(0)=  1  
  POL(minus(x1, x2))=  x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
           →DP Problem 18
Nar
             ...
               →DP Problem 22
Dependency Graph
       →DP Problem 6
Nar


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Narrowing Transformation


Dependency Pair:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))
one new Dependency Pair is created:

SUM(app(l, cons(x'', cons(y'', k')))) -> SUM(app(l, sum(cons(plus(x'', y''), k'))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar
           →DP Problem 23
Narrowing Transformation


Dependency Pair:

SUM(app(l, cons(x'', cons(y'', k')))) -> SUM(app(l, sum(cons(plus(x'', y''), k'))))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




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

SUM(app(l, cons(x'', cons(y'', k')))) -> SUM(app(l, sum(cons(plus(x'', y''), k'))))
four new Dependency Pairs are created:

SUM(app(l, cons(x''', cons(y''', nil)))) -> SUM(app(l, cons(plus(x''', y'''), nil)))
SUM(app(l, cons(x''', cons(y''', cons(y', l''))))) -> SUM(app(l, sum(cons(plus(plus(x''', y'''), y'), l''))))
SUM(app(l, cons(0, cons(y''', k')))) -> SUM(app(l, sum(cons(y''', k'))))
SUM(app(l, cons(s(x'), cons(y''', k')))) -> SUM(app(l, sum(cons(s(plus(x', y''')), k'))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar
           →DP Problem 23
Nar
             ...
               →DP Problem 24
Polynomial Ordering


Dependency Pairs:

SUM(app(l, cons(s(x'), cons(y''', k')))) -> SUM(app(l, sum(cons(s(plus(x', y''')), k'))))
SUM(app(l, cons(0, cons(y''', k')))) -> SUM(app(l, sum(cons(y''', k'))))
SUM(app(l, cons(x''', cons(y''', cons(y', l''))))) -> SUM(app(l, sum(cons(plus(plus(x''', y'''), y'), l''))))
SUM(app(l, cons(x''', cons(y''', nil)))) -> SUM(app(l, cons(plus(x''', y'''), nil)))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




The following dependency pair can be strictly oriented:

SUM(app(l, cons(0, cons(y''', k')))) -> SUM(app(l, sum(cons(y''', k'))))


Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(plus(x1, x2))=  x2  
  POL(0)=  1  
  POL(SUM(x1))=  1 + x1  
  POL(cons(x1, x2))=  x1 + x2  
  POL(nil)=  0  
  POL(s(x1))=  0  
  POL(sum(x1))=  x1  
  POL(app(x1, x2))=  x1 + x2  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar
           →DP Problem 23
Nar
             ...
               →DP Problem 25
Polynomial Ordering


Dependency Pairs:

SUM(app(l, cons(s(x'), cons(y''', k')))) -> SUM(app(l, sum(cons(s(plus(x', y''')), k'))))
SUM(app(l, cons(x''', cons(y''', cons(y', l''))))) -> SUM(app(l, sum(cons(plus(plus(x''', y'''), y'), l''))))
SUM(app(l, cons(x''', cons(y''', nil)))) -> SUM(app(l, cons(plus(x''', y'''), nil)))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

SUM(app(l, cons(s(x'), cons(y''', k')))) -> SUM(app(l, sum(cons(s(plus(x', y''')), k'))))
SUM(app(l, cons(x''', cons(y''', cons(y', l''))))) -> SUM(app(l, sum(cons(plus(plus(x''', y'''), y'), l''))))
SUM(app(l, cons(x''', cons(y''', nil)))) -> SUM(app(l, cons(plus(x''', y'''), nil)))


Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(plus(x1, x2))=  0  
  POL(0)=  1  
  POL(SUM(x1))=  x1  
  POL(cons(x1, x2))=  1 + x2  
  POL(nil)=  0  
  POL(s(x1))=  0  
  POL(sum(x1))=  1  
  POL(app(x1, x2))=  x1 + x2  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
Nar
       →DP Problem 4
Polo
       →DP Problem 5
Nar
       →DP Problem 6
Nar
           →DP Problem 23
Nar
             ...
               →DP Problem 26
Dependency Graph


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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