Term Rewriting System R:
[x, y, l]
+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

+'(s(x), s(y)) -> +'(x, y)
*'(s(x), s(y)) -> +'(*(x, y), +(x, y))
*'(s(x), s(y)) -> *'(x, y)
*'(s(x), s(y)) -> +'(x, y)
SUM(cons(x, l)) -> +'(x, sum(l))
SUM(cons(x, l)) -> SUM(l)
PROD(cons(x, l)) -> *'(x, prod(l))
PROD(cons(x, l)) -> PROD(l)

Furthermore, R contains four SCCs.


   R
DPs
       →DP Problem 1
Forward Instantiation Transformation
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
       →DP Problem 4
FwdInst


Dependency Pair:

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


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




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

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

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

The transformation is resulting in one new DP problem:



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


Dependency Pair:

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


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




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

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

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

The transformation is resulting in one new DP problem:



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


Dependency Pair:

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


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost that need to be oriented.

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

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 5
FwdInst
             ...
               →DP Problem 7
Dependency Graph
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
       →DP Problem 4
FwdInst


Dependency Pair:


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


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
FwdInst
       →DP Problem 4
FwdInst


Dependency Pair:

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


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




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

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

*'(s(s(x'')), s(s(y''))) -> *'(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 8
Forward Instantiation Transformation
       →DP Problem 3
FwdInst
       →DP Problem 4
FwdInst


Dependency Pair:

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


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




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

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

*'(s(s(s(x''''))), s(s(s(y'''')))) -> *'(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 8
FwdInst
             ...
               →DP Problem 9
Polynomial Ordering
       →DP Problem 3
FwdInst
       →DP Problem 4
FwdInst


Dependency Pair:

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


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(*'(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 8
FwdInst
             ...
               →DP Problem 10
Dependency Graph
       →DP Problem 3
FwdInst
       →DP Problem 4
FwdInst


Dependency Pair:


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


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
Forward Instantiation Transformation
       →DP Problem 4
FwdInst


Dependency Pair:

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


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




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

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

SUM(cons(x, cons(x'', l''))) -> SUM(cons(x'', l''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
           →DP Problem 11
Forward Instantiation Transformation
       →DP Problem 4
FwdInst


Dependency Pair:

SUM(cons(x, cons(x'', l''))) -> SUM(cons(x'', l''))


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




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

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

SUM(cons(x, cons(x'''', cons(x''''', l'''')))) -> SUM(cons(x'''', cons(x''''', l'''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
           →DP Problem 11
FwdInst
             ...
               →DP Problem 12
Polynomial Ordering
       →DP Problem 4
FwdInst


Dependency Pair:

SUM(cons(x, cons(x'''', cons(x''''', l'''')))) -> SUM(cons(x'''', cons(x''''', l'''')))


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




The following dependency pair can be strictly oriented:

SUM(cons(x, cons(x'''', cons(x''''', l'''')))) -> SUM(cons(x'''', cons(x''''', l'''')))


There are no usable rules for innermost that need to be oriented.

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

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
           →DP Problem 11
FwdInst
             ...
               →DP Problem 13
Dependency Graph
       →DP Problem 4
FwdInst


Dependency Pair:


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


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
FwdInst
       →DP Problem 4
Forward Instantiation Transformation


Dependency Pair:

PROD(cons(x, l)) -> PROD(l)


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




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

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

PROD(cons(x, cons(x'', l''))) -> PROD(cons(x'', l''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
       →DP Problem 4
FwdInst
           →DP Problem 14
Forward Instantiation Transformation


Dependency Pair:

PROD(cons(x, cons(x'', l''))) -> PROD(cons(x'', l''))


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




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

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

PROD(cons(x, cons(x'''', cons(x''''', l'''')))) -> PROD(cons(x'''', cons(x''''', l'''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
       →DP Problem 4
FwdInst
           →DP Problem 14
FwdInst
             ...
               →DP Problem 15
Polynomial Ordering


Dependency Pair:

PROD(cons(x, cons(x'''', cons(x''''', l'''')))) -> PROD(cons(x'''', cons(x''''', l'''')))


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




The following dependency pair can be strictly oriented:

PROD(cons(x, cons(x'''', cons(x''''', l'''')))) -> PROD(cons(x'''', cons(x''''', l'''')))


There are no usable rules for innermost that need to be oriented.

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

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
       →DP Problem 4
FwdInst
           →DP Problem 14
FwdInst
             ...
               →DP Problem 16
Dependency Graph


Dependency Pair:


Rules:


+(x, 0) -> x
+(0, x) -> x
+(s(x), s(y)) -> s(s(+(x, y)))
*(x, 0) -> 0
*(0, x) -> 0
*(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
sum(nil) -> 0
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> s(0)
prod(cons(x, l)) -> *(x, prod(l))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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