-(

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

↳Polynomial Ordering

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(-'(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 5

↳Dependency Graph

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→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

↳Polo

→DP Problem 2

↳Polynomial Ordering

→DP Problem 3

↳Polo

→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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(MIN(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 6

↳Dependency Graph

→DP Problem 3

↳Polo

→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

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polynomial 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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(TWICE(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→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

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→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

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Nar

→DP Problem 8

↳Narrowing 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 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

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Nar

→DP Problem 8

↳Nar

...

→DP Problem 9

↳Remaining Obligation(s)

The following remains to be proven:

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

Duration:

0:07 minutes