min(

min(0,

min(s(

max(

max(0,

max(s(

-(

-(s(

gcd(s(

R

↳Dependency Pair Analysis

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

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

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

GCD(s(x), s(y)) -> GCD(-(s(max(x,y)), s(min(x,y))), s(min(x,y)))

GCD(s(x), s(y)) -> -'(s(max(x,y)), s(min(x,y)))

GCD(s(x), s(y)) -> MAX(x,y)

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Polynomial Ordering

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Remaining

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

min(x, 0) -> 0

min(0,y) -> 0

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

max(x, 0) ->x

max(0,y) ->y

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

-(x, 0) ->x

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

gcd(s(x), s(y)) -> gcd(-(s(max(x,y)), s(min(x,y))), s(min(x,y)))

The following dependency pair can be strictly oriented:

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

There are no usable rules 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 5

↳Dependency Graph

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Remaining

min(x, 0) -> 0

min(0,y) -> 0

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

max(x, 0) ->x

max(0,y) ->y

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

-(x, 0) ->x

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

gcd(s(x), s(y)) -> gcd(-(s(max(x,y)), s(min(x,y))), s(min(x,y)))

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

↳Remaining

**MAX(s( x), s(y)) -> MAX(x, y)**

min(x, 0) -> 0

min(0,y) -> 0

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

max(x, 0) ->x

max(0,y) ->y

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

-(x, 0) ->x

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

gcd(s(x), s(y)) -> gcd(-(s(max(x,y)), s(min(x,y))), s(min(x,y)))

The following dependency pair can be strictly oriented:

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

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(MAX(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

↳Remaining

min(x, 0) -> 0

min(0,y) -> 0

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

max(x, 0) ->x

max(0,y) ->y

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

-(x, 0) ->x

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

gcd(s(x), s(y)) -> gcd(-(s(max(x,y)), s(min(x,y))), s(min(x,y)))

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

↳Remaining

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

min(x, 0) -> 0

min(0,y) -> 0

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

max(x, 0) ->x

max(0,y) ->y

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

-(x, 0) ->x

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

gcd(s(x), s(y)) -> gcd(-(s(max(x,y)), s(min(x,y))), s(min(x,y)))

The following dependency pair can be strictly oriented:

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

There are no usable rules 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 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 7

↳Dependency Graph

→DP Problem 4

↳Remaining

min(x, 0) -> 0

min(0,y) -> 0

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

max(x, 0) ->x

max(0,y) ->y

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

-(x, 0) ->x

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

gcd(s(x), s(y)) -> gcd(-(s(max(x,y)), s(min(x,y))), s(min(x,y)))

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

↳Remaining Obligation(s)

The following remains to be proven:

**GCD(s( x), s(y)) -> GCD(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))**

min(x, 0) -> 0

min(0,y) -> 0

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

max(x, 0) ->x

max(0,y) ->y

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

-(x, 0) ->x

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

gcd(s(x), s(y)) -> gcd(-(s(max(x,y)), s(min(x,y))), s(min(x,y)))

Duration:

0:00 minutes