Termination Proof using AProVE

MAYBE Termination Proof using AProVETerm Rewriting System R:
[M', N', N, M, X, y, x]
1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)
*(x, y) == *(y, x)
+(x, y) == +(y, x)
d(x, y) == d(y, x)
gcd(x, y) == gcd(y, x)

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

U11'(tt, M', N') -> U12'(equal(> (N', M'), true), M', N')
U11'(tt, M', N') -> EQUAL(> (N', M'), true)
U11'(tt, M', N') -> _{>_'}(N', M')
U12'(tt, M', N') -> gcd(d(N', M'), M')
U12'(tt, M', N') -> d(N', M')
U21'(tt, M', N) -> U22'(equal(> (M', N), true))
U21'(tt, M', N) -> EQUAL(> (M', N), true)
U21'(tt, M', N) -> _{>_'}(M', N)
U31'(tt, M', N) -> U32'(equal(> (N, M'), true), M', N)
U31'(tt, M', N) -> EQUAL(> (N, M'), true)
U31'(tt, M', N) -> _{>_'}(N, M')
U32'(tt, M', N) -> QUOT(d(N, M'), M')
U32'(tt, M', N) -> d(N, M')
*(s(N), s(M)) -> +(N, +(M, *(N, M)))
*(s(N), s(M)) -> +(M, *(N, M))
*(s(N), s(M)) -> *(N, M)
+(s(N), s(M)) -> +(N, M)
_{<_'}(N, M) -> _{>_'}(M, N)
_{>_'}(s(N), s(M)) -> _{>_'}(N, M)
d(s(N), s(M)) -> d(N, M)
gcd(N', M') -> U11'(tt, M', N')
QUOT(N, M') -> U21'(tt, M', N)
QUOT(N, M') -> U31'(tt, M', N)

Furthermore, R contains six SCCs.

     ↳DPs

       →DP Problem 1

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Inst

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

Dependency Pair:

_{>_'}(s(N), s(M)) -> _{>_'}(N, M)

Rules:

1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)

The following dependency pair can be strictly oriented:

_{>_'}(s(N), s(M)) -> _{>_'}(N, M)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(_>_'(x₁, x₂)) = x₁

POL(s_(x₁)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 7

             ↳Dependency Graph

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Inst

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

Dependency Pair:

Rules:

1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Inst

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

Dependency Pair:

d(s(N), s(M)) -> d(N, M)

Rules:

1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)

The following dependency pair can be strictly oriented:

d(s(N), s(M)) -> d(N, M)

There are no usable rules using the Ce-refinement that need to be oriented.

Oriented Equation:

d(x, y) == d(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(d(x₁, x₂)) = x₁ + x₂

POL(s_(x₁)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Instantiation Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

Dependency Pairs:

gcd(N', M') -> U11'(tt, M', N')
U12'(tt, M', N') -> gcd(d(N', M'), M')
U11'(tt, M', N') -> U12'(equal(> (N', M'), true), M', N')

Rules:

1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)

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

gcd(N', M') -> U11'(tt, M', N')

no new Dependency Pairs are created.
The transformation is resulting in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Inst

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

The following remains to be proven:
Dependency Pairs:

QUOT(N, M') -> U31'(tt, M', N)
U32'(tt, M', N) -> QUOT(d(N, M'), M')
U31'(tt, M', N) -> U32'(equal(> (N, M'), true), M', N)

Rules:

1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Inst

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Polynomial Ordering

       →DP Problem 6

         ↳Polo

Dependency Pair:

+(s(N), s(M)) -> +(N, M)

Rules:

1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)

The following dependency pair can be strictly oriented:

+(s(N), s(M)) -> +(N, M)

There are no usable rules using the Ce-refinement that need to be oriented.

Oriented Equation:

+(x, y) == +(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(_+_(x₁, x₂)) = x₁ + x₂

POL(s_(x₁)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Inst

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polynomial Ordering

Dependency Pair:

*(s(N), s(M)) -> *(N, M)

Rules:

1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)

The following dependency pair can be strictly oriented:

*(s(N), s(M)) -> *(N, M)

There are no usable rules using the Ce-refinement that need to be oriented.

Oriented Equation:

*(x, y) == *(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(_*_(x₁, x₂)) = x₁ + x₂

POL(s_(x₁)) = 1 + x₁

resulting in one new DP problem.

The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
5:00 minutes Timeout: aborting command ``runme'' with signal 9

POL(d(x₁, x₂))	= x₁ + x₂
POL(s_(x₁))	= 1 + x₁

POL(_+_(x₁, x₂))	= x₁ + x₂
POL(s_(x₁))	= 1 + x₁

POL(*__(x₁, x₂)**)	= x₁ + x₂
POL(s_(x₁))	= 1 + x₁