-(

-(s(

min(

min(0,

min(s(

twice(0) -> 0

twice(s(

f(s(

f(s(

R

↳Dependency Pair Analysis

-'(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

↳DPs

→DP Problem 1

↳Argument Filtering and Ordering

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

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

The following dependency pair can be strictly oriented:

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

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

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

-'(x,_{1}x) -> -'(_{2}x,_{1}x)_{2}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 5

↳Dependency Graph

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

-(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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳Argument Filtering and Ordering

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

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

The following dependency pair can be strictly oriented:

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

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

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

MIN(x,_{1}x) -> MIN(_{2}x,_{1}x)_{2}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 6

↳Dependency Graph

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

-(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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳Argument Filtering and Ordering

→DP Problem 4

↳Nar

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

-(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

The following dependency pair can be strictly oriented:

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

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

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

TWICE(x) -> TWICE(_{1}x)_{1}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 7

↳Dependency Graph

→DP Problem 4

↳Nar

-(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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Narrowing Transformation

**F(s( x), s(y)) -> F(-(x, min(x, y)), s(twice(min(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

On this DP problem, a Narrowing SCC transformation can be performed.

As a result of transforming the rule

six new Dependency Pairs are created:

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

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

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, min(x'', 0)), s(twice(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'')))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rewriting Transformation

**F(s(s( x'')), s(s(y''))) -> F(-(s(y''), min(s(x''), s(y''))), s(twice(s(min(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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 9

↳Rewriting Transformation

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

-(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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 10

↳Rewriting Transformation

**F(s(0), s( y'')) -> F(y'', s(twice(min(0, 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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 11

↳Rewriting Transformation

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

-(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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 12

↳Narrowing Transformation

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

-(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

On this DP problem, a Narrowing SCC transformation can be performed.

As a result of transforming the rule

six new Dependency Pairs are created:

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

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 13

↳Rewriting Transformation

**F(s(s( x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 14

↳Rewriting Transformation

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

-(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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 15

↳Rewriting Transformation

**F(s(s( x'')), s(s(y''))) -> F(-(s(x''), min(s(x''), s(y''))), s(twice(s(min(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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 16

↳Rewriting Transformation

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

-(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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Nar

→DP Problem 8

↳Rw

...

→DP Problem 17

↳Remaining Obligation(s)

The following remains to be proven:

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

-(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

Duration:

0:04 minutes