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
Argument Filtering and 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 w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
+'(x1, x2) -> +'(x1, x2)
s(x1) -> s(x1)


   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
Argument Filtering and 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 w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
*'(x1, x2) -> *'(x1, x2)
s(x1) -> s(x1)


   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
Argument Filtering and 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 w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
SUM(x1) -> SUM(x1)
cons(x1, x2) -> cons(x1, x2)


   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
Argument Filtering and 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 w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
PROD(x1) -> PROD(x1)
cons(x1, x2) -> cons(x1, x2)


   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