Termination Proof using AProVE

Term Rewriting System R:
[N, M, NzN, NzM]
p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

+'(s(N), s(M)) -> +'(N, M)
*'(s(N), s(M)) -> +'(N, +(M, *(N, M)))
*'(s(N), s(M)) -> +'(M, *(N, M))
*'(s(N), s(M)) -> *'(N, M)
GT(NzN, 0) -> U₄(is_NzNat(NzN))
GT(NzN, 0) -> IS_NZNAT(NzN)
GT(s(N), s(M)) -> GT(N, M)
LT(N, M) -> GT(M, N)
D(s(N), s(M)) -> D(N, M)
QUOT(N, NzM) -> U₁₁(is_NzNat(NzM), N, NzM)
QUOT(N, NzM) -> IS_NZNAT(NzM)
QUOT(NzM, NzM) -> U₀₁(is_NzNat(NzM))
QUOT(NzM, NzM) -> IS_NZNAT(NzM)
QUOT(N, NzM) -> U₂₁(is_NzNat(NzM), NzM, N)
U₁₁(True, N, NzM) -> U₁(gt(N, NzM), N, NzM)
U₁₁(True, N, NzM) -> GT(N, NzM)
U₁(True, N, NzM) -> QUOT(d(N, NzM), NzM)
U₁(True, N, NzM) -> D(N, NzM)
U₂₁(True, NzM, N) -> U₂(gt(NzM, N))
U₂₁(True, NzM, N) -> GT(NzM, N)
GCD(NzM, NzM) -> U₀₂(is_NzNat(NzM), NzM)
GCD(NzM, NzM) -> IS_NZNAT(NzM)
GCD(NzN, NzM) -> U₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
GCD(NzN, NzM) -> IS_NZNAT(NzN)
GCD(NzN, NzM) -> IS_NZNAT(NzM)
U₃₁(True, True, NzN, NzM) -> U₃(gt(NzN, NzM), NzN, NzM)
U₃₁(True, True, NzN, NzM) -> GT(NzN, NzM)
U₃(True, NzN, NzM) -> GCD(d(NzN, NzM), NzM)
U₃(True, NzN, NzM) -> D(NzN, NzM)

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

         ↳Remaining

       →DP Problem 6

         ↳Remaining

Dependency Pair:

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

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

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(s(x₁)) = 1 + x₁

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

         ↳Remaining

       →DP Problem 6

         ↳Remaining

Dependency Pair:

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:

innermost

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

         ↳Remaining

       →DP Problem 6

         ↳Remaining

Dependency Pair:

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

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

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(s(x₁)) = 1 + x₁

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

         ↳Remaining

       →DP Problem 6

         ↳Remaining

Dependency Pair:

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:

innermost

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

         ↳Remaining

       →DP Problem 6

         ↳Remaining

Dependency Pair:

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

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

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

         ↳Remaining

       →DP Problem 6

         ↳Remaining

Dependency Pair:

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:

innermost

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

         ↳Remaining

       →DP Problem 6

         ↳Remaining

Dependency Pair:

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

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

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₁, 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 4

         ↳Polo

           →DP Problem 10

             ↳Dependency Graph

       →DP Problem 5

         ↳Remaining

       →DP Problem 6

         ↳Remaining

Dependency Pair:

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:

innermost

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

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
U₁(True, N, NzM) -> QUOT(d(N, NzM), NzM)
U₁₁(True, N, NzM) -> U₁(gt(N, NzM), N, NzM)
QUOT(N, NzM) -> U₁₁(is_NzNat(NzM), N, NzM)

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:
innermost
Dependency Pairs:
U₃(True, NzN, NzM) -> GCD(d(NzN, NzM), NzM)
U₃₁(True, True, NzN, NzM) -> U₃(gt(NzN, NzM), NzN, NzM)
GCD(NzN, NzM) -> U₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:
innermost

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
U₁(True, N, NzM) -> QUOT(d(N, NzM), NzM)
U₁₁(True, N, NzM) -> U₁(gt(N, NzM), N, NzM)
QUOT(N, NzM) -> U₁₁(is_NzNat(NzM), N, NzM)

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:
innermost
Dependency Pairs:
U₃(True, NzN, NzM) -> GCD(d(NzN, NzM), NzM)
U₃₁(True, True, NzN, NzM) -> U₃(gt(NzN, NzM), NzN, NzM)
GCD(NzN, NzM) -> U₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)

Rules:

p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u₄(is_NzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u₁₁(is_NzNat(NzM), N, NzM)
quot(NzM, NzM) -> u₀₁(is_NzNat(NzM))
quot(N, NzM) -> u₂₁(is_NzNat(NzM), NzM, N)
u₁₁(True, N, NzM) -> u₁(gt(N, NzM), N, NzM)
u₁(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u₀₁(True) -> s(0)
u₂₁(True, NzM, N) -> u₂(gt(NzM, N))
u₂(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u₀₂(is_NzNat(NzM), NzM)
gcd(NzN, NzM) -> u₃₁(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u₀₂(True, NzM) -> NzM
u₃₁(True, True, NzN, NzM) -> u₃(gt(NzN, NzM), NzN, NzM)
u₃(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Strategy:
innermost

Innermost Termination of R could not be shown.
Duration:
0:00 minutes