Termination Proof using AProVE

Term Rewriting System R:
[x, y]
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
min(x, 0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
twice(0) -> 0
twice(s(x)) -> s(s(twice(x)))
f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))
f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y))))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

-'(s(x), s(y)) -> -'(x, y)
MIN(s(x), s(y)) -> MIN(x, y)
TWICE(s(x)) -> TWICE(x)
F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))
F(s(x), s(y)) -> -'(y, min(x, y))
F(s(x), s(y)) -> MIN(x, y)
F(s(x), s(y)) -> TWICE(min(x, y))
F(s(x), s(y)) -> F(-(x, min(x, y)), s(twice(min(x, y))))
F(s(x), s(y)) -> -'(x, min(x, y))

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Usable Rules (Innermost)

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

Dependency Pair:

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

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
min(x, 0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
twice(0) -> 0
twice(s(x)) -> s(s(twice(x)))
f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))
f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y))))

Strategy:

innermost

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

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 5

             ↳Size-Change Principle

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

-'(s(x), s(y)) -> -'(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

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳Usable Rules (Innermost)

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

Dependency Pair:

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

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
min(x, 0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
twice(0) -> 0
twice(s(x)) -> s(s(twice(x)))
f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))
f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y))))

Strategy:

innermost

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

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

           →DP Problem 6

             ↳Size-Change Principle

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

MIN(s(x), s(y)) -> MIN(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

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳Usable Rules (Innermost)

       →DP Problem 4

         ↳UsableRules

Dependency Pair:

TWICE(s(x)) -> TWICE(x)

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
min(x, 0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
twice(0) -> 0
twice(s(x)) -> s(s(twice(x)))
f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))
f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y))))

Strategy:

innermost

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

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

           →DP Problem 7

             ↳Size-Change Principle

       →DP Problem 4

         ↳UsableRules

Dependency Pair:

TWICE(s(x)) -> TWICE(x)

Rule:

none

Strategy:

innermost

We number the DPs as follows:

TWICE(s(x)) -> TWICE(x)

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳Usable Rules (Innermost)

Dependency Pairs:

F(s(x), s(y)) -> F(-(x, min(x, y)), s(twice(min(x, y))))
F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
min(x, 0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
twice(0) -> 0
twice(s(x)) -> s(s(twice(x)))
f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))
f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y))))

Strategy:

innermost

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

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Narrowing Transformation

Dependency Pairs:

F(s(x), s(y)) -> F(-(x, min(x, y)), s(twice(min(x, y))))
F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(x), s(y)) -> F(-(x, min(x, y)), s(twice(min(x, y))))

six new Dependency Pairs are created:

F(s(0), s(y'')) -> F(-(0, 0), s(twice(min(0, y''))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x''), s(0)) -> F(-(x'', 0), s(twice(min(x'', 0))))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(twice(0)))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(twice(0)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 9

                 ↳Rewriting Transformation

Dependency Pairs:

F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(twice(0)))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(twice(0)))
F(s(x''), s(0)) -> F(-(x'', 0), s(twice(min(x'', 0))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(0), s(y'')) -> F(-(0, 0), s(twice(min(0, y''))))
F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(0), s(y'')) -> F(-(0, 0), s(twice(min(0, y''))))

one new Dependency Pair is created:

F(s(0), s(y'')) -> F(0, s(twice(min(0, y''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 10

                 ↳Rewriting Transformation

Dependency Pairs:

F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(twice(0)))
F(s(x''), s(0)) -> F(-(x'', 0), s(twice(min(x'', 0))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(twice(0)))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(x''), s(0)) -> F(-(x'', 0), s(twice(min(x'', 0))))

one new Dependency Pair is created:

F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 11

                 ↳Rewriting Transformation

Dependency Pairs:

F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(twice(0)))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(twice(0)))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(twice(0)))

one new Dependency Pair is created:

F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 12

                 ↳Rewriting Transformation

Dependency Pairs:

F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(0))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(twice(0)))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))
F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(twice(0)))

one new Dependency Pair is created:

F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 13

                 ↳Narrowing Transformation

Dependency Pairs:

F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(0))
F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(0))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(x), s(y)) -> F(-(y, min(x, y)), s(twice(min(x, y))))

six new Dependency Pairs are created:

F(s(0), s(y'')) -> F(-(y'', 0), s(twice(min(0, y''))))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x''), s(0)) -> F(-(0, 0), s(twice(min(x'', 0))))
F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(twice(0)))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(x''), s(0)) -> F(-(0, min(x'', 0)), s(twice(0)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 14

                 ↳Rewriting Transformation

Dependency Pairs:

F(s(x''), s(0)) -> F(-(0, min(x'', 0)), s(twice(0)))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(twice(0)))
F(s(x''), s(0)) -> F(-(0, 0), s(twice(min(x'', 0))))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(0), s(y'')) -> F(-(y'', 0), s(twice(min(0, y''))))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(0))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(0))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(0), s(y'')) -> F(-(y'', 0), s(twice(min(0, y''))))

one new Dependency Pair is created:

F(s(0), s(y'')) -> F(y'', s(twice(min(0, y''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 15

                 ↳Rewriting Transformation

Dependency Pairs:

F(s(0), s(y'')) -> F(y'', s(twice(min(0, y''))))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(twice(0)))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x''), s(0)) -> F(-(0, 0), s(twice(min(x'', 0))))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(0))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(0))
F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x''), s(0)) -> F(-(0, min(x'', 0)), s(twice(0)))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(x''), s(0)) -> F(-(0, 0), s(twice(min(x'', 0))))

one new Dependency Pair is created:

F(s(x''), s(0)) -> F(0, s(twice(min(x'', 0))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 16

                 ↳Rewriting Transformation

Dependency Pairs:

F(s(x''), s(0)) -> F(-(0, min(x'', 0)), s(twice(0)))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(twice(0)))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(0))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(0))
F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(0), s(y'')) -> F(y'', s(twice(min(0, y''))))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(twice(0)))

one new Dependency Pair is created:

F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 17

                 ↳Rewriting Transformation

Dependency Pairs:

F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(0))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(0), s(y'')) -> F(y'', s(twice(min(0, y''))))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(0))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(0))
F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x''), s(0)) -> F(-(0, min(x'', 0)), s(twice(0)))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

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

F(s(x''), s(0)) -> F(-(0, min(x'', 0)), s(twice(0)))

one new Dependency Pair is created:

F(s(x''), s(0)) -> F(-(0, min(x'', 0)), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 18

                 ↳Semantic Labelling

Dependency Pairs:

F(s(x''), s(0)) -> F(-(0, min(x'', 0)), s(0))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(0), s(y'')) -> F(y'', s(twice(min(0, y''))))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(0))
F(s(0), s(y'')) -> F(-(0, min(0, y'')), s(0))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))
F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(0))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x

Strategy:

innermost

Using Semantic Labelling, the DP problem could be transformed. The following quasi-model was found:

twice(x₀) = 1

s(x₀) = 1

F(x₀, x₁) = 0

-(x₀, x₁) = x₀

min(x₀, x₁) = x₀

0 = 0

From the dependency graph we obtain 1 (labeled) SCCs which each result in correspondingDP problem.

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 19

                 ↳Unlabel

Dependency Pairs:

F₁₁(s₀(0), s₁(y'')) -> F₁₁(-₁₀(y'', min₀₁(0, y'')), s₀(0))
F₁₁(s₁(s₁(x'')), s₁(s₁(y''))) -> F₁₁(-₁₁(s₁(x''), s₁(min₁₁(x'', y''))), s₁(twice₁(min₁₁(s₁(x''), s₁(y'')))))
F₁₁(s₁(s₁(x'')), s₁(s₀(y''))) -> F₁₁(-₁₁(s₁(x''), s₁(min₁₀(x'', y''))), s₁(twice₁(min₁₁(s₁(x''), s₀(y'')))))
F₁₁(s₁(s₀(x'')), s₁(s₁(y''))) -> F₁₁(-₁₁(s₀(x''), s₀(min₀₁(x'', y''))), s₁(twice₁(min₁₁(s₀(x''), s₁(y'')))))
F₁₁(s₁(s₀(x'')), s₁(s₀(y''))) -> F₁₁(-₁₁(s₀(x''), s₀(min₀₀(x'', y''))), s₁(twice₁(min₁₁(s₀(x''), s₀(y'')))))
F₁₁(s₁(s₁(x'')), s₁(s₁(y''))) -> F₁₁(-₁₁(s₁(x''), min₁₁(s₁(x''), s₁(y''))), s₁(twice₁(s₁(min₁₁(x'', y'')))))
F₁₁(s₁(s₁(x'')), s₁(s₀(y''))) -> F₁₁(-₁₁(s₁(x''), min₁₁(s₁(x''), s₀(y''))), s₁(twice₁(s₁(min₁₀(x'', y'')))))
F₁₁(s₁(s₀(x'')), s₁(s₁(y''))) -> F₁₁(-₁₁(s₀(x''), min₁₁(s₀(x''), s₁(y''))), s₁(twice₁(s₀(min₀₁(x'', y'')))))
F₁₁(s₁(s₀(x'')), s₁(s₀(y''))) -> F₁₁(-₁₁(s₀(x''), min₁₁(s₀(x''), s₀(y''))), s₁(twice₁(s₀(min₀₀(x'', y'')))))
F₁₁(s₁(x''), s₀(0)) -> F₁₁(x'', s₁(twice₁(min₁₀(x'', 0))))
F₁₁(s₁(x''), s₀(0)) -> F₁₁(-₁₁(x'', min₁₀(x'', 0)), s₀(0))
F₁₁(s₀(0), s₁(y'')) -> F₁₁(y'', s₁(twice₀(min₀₁(0, y''))))
F₁₁(s₁(s₁(x'')), s₁(s₁(y''))) -> F₁₁(-₁₁(s₁(y''), s₁(min₁₁(x'', y''))), s₁(twice₁(min₁₁(s₁(x''), s₁(y'')))))
F₁₁(s₁(s₁(x'')), s₁(s₀(y''))) -> F₁₁(-₁₁(s₀(y''), s₁(min₁₀(x'', y''))), s₁(twice₁(min₁₁(s₁(x''), s₀(y'')))))
F₁₁(s₁(s₀(x'')), s₁(s₁(y''))) -> F₁₁(-₁₁(s₁(y''), s₀(min₀₁(x'', y''))), s₁(twice₁(min₁₁(s₀(x''), s₁(y'')))))
F₁₁(s₁(s₀(x'')), s₁(s₀(y''))) -> F₁₁(-₁₁(s₀(y''), s₀(min₀₀(x'', y''))), s₁(twice₁(min₁₁(s₀(x''), s₀(y'')))))
F₁₁(s₁(s₁(x'')), s₁(s₁(y''))) -> F₁₁(-₁₁(s₁(y''), min₁₁(s₁(x''), s₁(y''))), s₁(twice₁(s₁(min₁₁(x'', y'')))))
F₁₁(s₁(s₁(x'')), s₁(s₀(y''))) -> F₁₁(-₁₁(s₀(y''), min₁₁(s₁(x''), s₀(y''))), s₁(twice₁(s₁(min₁₀(x'', y'')))))
F₁₁(s₁(s₀(x'')), s₁(s₁(y''))) -> F₁₁(-₁₁(s₁(y''), min₁₁(s₀(x''), s₁(y''))), s₁(twice₁(s₀(min₀₁(x'', y'')))))
F₁₁(s₁(s₀(x'')), s₁(s₀(y''))) -> F₁₁(-₁₁(s₀(y''), min₁₁(s₀(x''), s₀(y''))), s₁(twice₁(s₀(min₀₀(x'', y'')))))

Rules:

twice₁(s₀(x)) -> s₁(s₁(twice₀(x)))
twice₁(s₁(x)) -> s₁(s₁(twice₁(x)))
twice₁(x) -> twice₀(x)
s₁(x) -> s₀(x)
twice₀(0) -> 0
min₀₀(0, y) -> 0
min₀₀(x, 0) -> 0
min₀₁(0, y) -> 0
min₀₁(x, x') -> min₀₀(x, x')
min₀₁(x, x') -> min₁₀(x, x')
min₁₁(s₀(x), s₀(y)) -> s₀(min₀₀(x, y))
min₁₁(s₀(x), s₁(y)) -> s₀(min₀₁(x, y))
min₁₁(s₁(x), s₀(y)) -> s₁(min₁₀(x, y))
min₁₁(s₁(x), s₁(y)) -> s₁(min₁₁(x, y))
min₁₁(x, x') -> min₀₁(x, x')
min₁₁(x, x') -> min₀₀(x, x')
min₁₁(x, x') -> min₁₀(x, x')
min₁₀(x, 0) -> 0
min₁₀(x, x') -> min₀₀(x, x')
-₁₁(s₀(x), s₀(y)) -> -₀₀(x, y)
-₁₁(s₀(x), s₁(y)) -> -₀₁(x, y)
-₁₁(s₁(x), s₀(y)) -> -₁₀(x, y)
-₁₁(s₁(x), s₁(y)) -> -₁₁(x, y)
-₁₁(x, x') -> -₀₀(x, x')
-₁₁(x, x') -> -₀₁(x, x')
-₁₁(x, x') -> -₁₀(x, x')
-₀₀(x, 0) -> x
-₀₁(x, x') -> -₀₀(x, x')
-₀₁(x, x') -> -₁₀(x, x')
-₁₀(x, 0) -> x
-₁₀(x, x') -> -₀₀(x, x')

Removed all semantic labels.

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 20

                 ↳Non-Overlappingness Check

Dependency Pairs:

F(s(0), s(y'')) -> F(y'', s(twice(min(0, y''))))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), min(s(x''), s(y''))), s(twice(s(min(x'', y'')))))
F(s(x''), s(0)) -> F(x'', s(twice(min(x'', 0))))
F(s(s(x'')), s(s(y''))) -> F(-(s(y''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(0), s(y'')) -> F(-(y'', min(0, y'')), s(0))
F(s(s(x'')), s(s(y''))) -> F(-(s(x''), s(min(x'', y''))), s(twice(min(s(x''), s(y'')))))
F(s(x''), s(0)) -> F(-(x'', min(x'', 0)), s(0))

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0

R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

       →DP Problem 3

         ↳UsableRules

       →DP Problem 4

         ↳UsableRules

           →DP Problem 8

             ↳Nar

...

               →DP Problem 21

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

Rules:

twice(s(x)) -> s(s(twice(x)))
twice(0) -> 0
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))
min(x, 0) -> 0

Strategy:

innermost

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

twice(x₀)	= 1
s(x₀)	= 1
F(x₀, x₁)	= 0
-(x₀, x₁)	= x₀
min(x₀, x₁)	= x₀
0	= 0