Term Rewriting System R:
[x, y, z]
double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

DOUBLE(s(x)) -> DOUBLE(x)
HALF(s(s(x))) -> HALF(x)
-'(s(x), s(y)) -> -'(x, y)

Furthermore, R contains three SCCs.


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


Dependency Pair:

DOUBLE(s(x)) -> DOUBLE(x)


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


Strategy:

innermost




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

DOUBLE(s(x)) -> DOUBLE(x)
one new Dependency Pair is created:

DOUBLE(s(s(x''))) -> DOUBLE(s(x''))

The transformation is resulting in one new DP problem:



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


Dependency Pair:

DOUBLE(s(s(x''))) -> DOUBLE(s(x''))


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


Strategy:

innermost




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

DOUBLE(s(s(x''))) -> DOUBLE(s(x''))
one new Dependency Pair is created:

DOUBLE(s(s(s(x'''')))) -> DOUBLE(s(s(x'''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 5
Argument Filtering and Ordering
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst


Dependency Pair:

DOUBLE(s(s(s(x'''')))) -> DOUBLE(s(s(x'''')))


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


Strategy:

innermost




The following dependency pair can be strictly oriented:

DOUBLE(s(s(s(x'''')))) -> DOUBLE(s(s(x'''')))


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:
DOUBLE(x1) -> DOUBLE(x1)
s(x1) -> s(x1)


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


Dependency Pair:


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


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


Dependency Pair:

HALF(s(s(x))) -> HALF(x)


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


Strategy:

innermost




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

HALF(s(s(x))) -> HALF(x)
one new Dependency Pair is created:

HALF(s(s(s(s(x''))))) -> HALF(s(s(x'')))

The transformation is resulting in one new DP problem:



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


Dependency Pair:

HALF(s(s(s(s(x''))))) -> HALF(s(s(x'')))


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


Strategy:

innermost




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

HALF(s(s(s(s(x''))))) -> HALF(s(s(x'')))
one new Dependency Pair is created:

HALF(s(s(s(s(s(s(x''''))))))) -> HALF(s(s(s(s(x'''')))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
           →DP Problem 7
FwdInst
             ...
               →DP Problem 8
Argument Filtering and Ordering
       →DP Problem 3
FwdInst


Dependency Pair:

HALF(s(s(s(s(s(s(x''''))))))) -> HALF(s(s(s(s(x'''')))))


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


Strategy:

innermost




The following dependency pair can be strictly oriented:

HALF(s(s(s(s(s(s(x''''))))))) -> HALF(s(s(s(s(x'''')))))


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:
HALF(x1) -> HALF(x1)
s(x1) -> s(x1)


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


Dependency Pair:


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


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


Dependency Pair:

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


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


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


Dependency Pair:

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


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


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 3
FwdInst
           →DP Problem 10
FwdInst
             ...
               →DP Problem 11
Argument Filtering and Ordering


Dependency Pair:

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


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


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 3
FwdInst
           →DP Problem 10
FwdInst
             ...
               →DP Problem 12
Dependency Graph


Dependency Pair:


Rules:


double(0) -> 0
double(s(x)) -> s(s(double(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
half(double(x)) -> x
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
if(0, y, z) -> y
if(s(x), y, z) -> z


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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