Termination Proof using AProVE

MAYBE Termination Proof using AProVETerm Rewriting System R:
[M, N, M', N', 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(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'(tt, M, N)
U12'(tt, M, N) -> +(N, +(M, *(N, M)))
U12'(tt, M, N) -> +(M, *(N, M))
U12'(tt, M, N) -> *(N, M)
U21'(tt, M, N) -> U22'(tt, M, N)
U22'(tt, M, N) -> +(N, M)
U31'(tt, M, N) -> U32'(tt, M, N)
U32'(tt, M, N) -> _{>_'}(M, N)
U41'(tt, M, N) -> U42'(tt, M, N)
U42'(tt, M, N) -> _{>_'}(N, M)
U51'(tt, M, N) -> U52'(tt, M, N)
U52'(tt, M, N) -> d(N, M)
U61'(tt, M', N') -> U62'(tt, M', N')
U62'(tt, M', N') -> U63'(equal(> (N', M'), true), M', N')
U62'(tt, M', N') -> EQUAL(> (N', M'), true)
U62'(tt, M', N') -> _{>_'}(N', M')
U63'(tt, M', N') -> gcd(d(N', M'), M')
U63'(tt, M', N') -> d(N', M')
U71'(tt, M', N) -> U72'(tt, M', N)
U72'(tt, M', N) -> U73'(equal(> (M', N), true))
U72'(tt, M', N) -> EQUAL(> (M', N), true)
U72'(tt, M', N) -> _{>_'}(M', N)
U81'(tt, M', N) -> U82'(tt, M', N)
U82'(tt, M', N) -> U83'(equal(> (N, M'), true), M', N)
U82'(tt, M', N) -> EQUAL(> (N, M'), true)
U82'(tt, M', N) -> _{>_'}(N, M')
U83'(tt, M', N) -> QUOT(d(N, M'), M')
U83'(tt, M', N) -> d(N, M')
*(s(N), s(M)) -> U11'(tt, M, N)
+(s(N), s(M)) -> U21'(tt, M, N)
_{<_'}(N, M) -> U31'(tt, M, N)
_{>_'}(s(N), s(M)) -> U41'(tt, M, N)
d(s(N), s(M)) -> U51'(tt, M, N)
gcd(N', M') -> U61'(tt, M', N')
QUOT(N, M') -> U71'(tt, M', N)
QUOT(N, M') -> U81'(tt, M', N)

Furthermore, R contains six SCCs.

     ↳DPs

       →DP Problem 1

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U22'(tt, M, N) -> +(N, M)
U21'(tt, M, N) -> U22'(tt, M, N)
+(s(N), s(M)) -> U21'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

The following dependency pair can be strictly oriented:

+(s(N), s(M)) -> U21'(tt, M, N)

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(tt) = 0

POL(U21'(x₁, x₂, x₃)) = x₂ + x₃

POL(U22'(x₁, x₂, 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

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U22'(tt, M, N) -> +(N, M)
U21'(tt, M, N) -> U22'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(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

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

*(s(N), s(M)) -> U11'(tt, M, N)
U12'(tt, M, N) -> *(N, M)
U11'(tt, M, N) -> U12'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

The following dependency pair can be strictly oriented:

*(s(N), s(M)) -> U11'(tt, M, N)

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(U12'(x₁, x₂, x₃)) = x₂ + x₃

POL(tt) = 0

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

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

POL(U11'(x₁, x₂, x₃)) = x₂ + x₃

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 8

             ↳Dependency Graph

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U12'(tt, M, N) -> *(N, M)
U11'(tt, M, N) -> U12'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polynomial Ordering

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U42'(tt, M, N) -> _{>_'}(N, M)
U41'(tt, M, N) -> U42'(tt, M, N)
_{>_'}(s(N), s(M)) -> U41'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

The following dependency pair can be strictly oriented:

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

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(U41'(x₁, x₂, x₃)) = x₃

POL(tt) = 0

POL(U42'(x₁, x₂, x₃)) = x₃

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

         ↳Polo

           →DP Problem 9

             ↳Dependency Graph

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U42'(tt, M, N) -> _{>_'}(N, M)
U41'(tt, M, N) -> U42'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polynomial Ordering

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

d(s(N), s(M)) -> U51'(tt, M, N)
U52'(tt, M, N) -> d(N, M)
U51'(tt, M, N) -> U52'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

The following dependency pair can be strictly oriented:

d(s(N), s(M)) -> U51'(tt, M, N)

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(U52'(x₁, x₂, x₃)) = x₂ + x₃

POL(U51'(x₁, x₂, x₃)) = x₂ + x₃

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

POL(tt) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

           →DP Problem 10

             ↳Dependency Graph

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U52'(tt, M, N) -> d(N, M)
U51'(tt, M, N) -> U52'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

gcd(N', M') -> U61'(tt, M', N')
U63'(tt, M', N') -> gcd(d(N', M'), M')
U62'(tt, M', N') -> U63'(equal(> (N', M'), true), M', N')
U61'(tt, M', N') -> U62'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

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

gcd(N', M') -> U61'(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

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

       →DP Problem 6

         ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

QUOT(N, M') -> U81'(tt, M', N)
U83'(tt, M', N) -> QUOT(d(N, M'), M')
U82'(tt, M', N) -> U83'(equal(> (N, M'), true), M', N)
U81'(tt, M', N) -> U82'(tt, 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(tt, M, N)
U12(tt, M, N) -> s(+(N, +(M, *(N, M))))
U21(tt, M, N) -> U22(tt, M, N)
U22(tt, M, N) -> s(s(+(N, M)))
U31(tt, M, N) -> U32(tt, M, N)
U32(tt, M, N) -> > (M, N)
U41(tt, M, N) -> U42(tt, M, N)
U42(tt, M, N) -> > (N, M)
U51(tt, M, N) -> U52(tt, M, N)
U52(tt, M, N) -> d(N, M)
U61(tt, M', N') -> U62(tt, M', N')
U62(tt, M', N') -> U63(equal(> (N', M'), true), M', N')
U63(tt, M', N') -> gcd(d(N', M'), M')
U71(tt, M', N) -> U72(tt, M', N)
U72(tt, M', N) -> U73(equal(> (M', N), true))
U73(tt) -> 0
U81(tt, M', N) -> U82(tt, M', N)
U82(tt, M', N) -> U83(equal(> (N, M'), true), M', N)
U83(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> U11(tt, M, N)
+(N, 0) -> N
+(s(N), s(M)) -> U21(tt, M, N)
< (N, M) -> U31(tt, M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> U41(tt, M, N)
d(0, N) -> N
d(s(N), s(M)) -> U51(tt, M, N)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U61(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U71(tt, M', N)
quot(N, M') -> U81(tt, M', N)

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(_+_(x₁, x₂))	= x₁ + x₂
POL(tt)	= 0
POL(U21'(x₁, x₂, x₃))	= x₂ + x₃
POL(U22'(x₁, x₂, x₃))	= x₂ + x₃
POL(s_(x₁))	= 1 + x₁

POL(U12'(x₁, x₂, x₃))	= x₂ + x₃
POL(tt)	= 0
POL(*__(x₁, x₂)**)	= x₁ + x₂
POL(s_(x₁))	= 1 + x₁
POL(U11'(x₁, x₂, x₃))	= x₂ + x₃

POL(U41'(x₁, x₂, x₃))	= x₃
POL(tt)	= 0
POL(U42'(x₁, x₂, x₃))	= x₃
POL(_>_'(x₁, x₂))	= x₁
POL(s_(x₁))	= 1 + x₁

POL(U52'(x₁, x₂, x₃))	= x₂ + x₃
POL(U51'(x₁, x₂, x₃))	= x₂ + x₃
POL(d(x₁, x₂))	= x₁ + x₂
POL(tt)	= 0
POL(s_(x₁))	= 1 + x₁