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

         ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 7

             ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining

Dependency Pair:

+'(s(s(N'')), s(s(M''))) -> +'(s(N''), s(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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 7

             ↳FwdInst

...

               →DP Problem 8

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining

Dependency Pair:

+'(s(s(s(N''''))), s(s(s(M'''')))) -> +'(s(s(N'''')), s(s(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(s(s(N''''))), s(s(s(M'''')))) -> +'(s(s(N'''')), s(s(M'''')))

There are no usable rules for innermost that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(+'(x₁, x₂)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 7

             ↳FwdInst

...

               →DP Problem 9

                 ↳Dependency Graph

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →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

         ↳FwdInst

       →DP Problem 2

         ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining

Dependency Pair:

GT(s(s(N'')), s(s(M''))) -> GT(s(N''), s(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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳FwdInst

...

               →DP Problem 11

                 ↳Polynomial Ordering

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining

Dependency Pair:

GT(s(s(s(N''''))), s(s(s(M'''')))) -> GT(s(s(N'''')), s(s(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(s(s(N''''))), s(s(s(M'''')))) -> GT(s(s(N'''')), s(s(M'''')))

There are no usable rules for innermost that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(GT(x₁, x₂)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳FwdInst

...

               →DP Problem 12

                 ↳Dependency Graph

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 13

             ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining

Dependency Pair:

D(s(s(N'')), s(s(M''))) -> D(s(N''), s(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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 13

             ↳FwdInst

...

               →DP Problem 14

                 ↳Polynomial Ordering

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining

Dependency Pair:

D(s(s(s(N''''))), s(s(s(M'''')))) -> D(s(s(N'''')), s(s(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(s(s(N''''))), s(s(s(M'''')))) -> D(s(s(N'''')), s(s(M'''')))

There are no usable rules for innermost that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(D(x₁, x₂)) = 1 + x₁

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 13

             ↳FwdInst

...

               →DP Problem 15

                 ↳Dependency Graph

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳Nar

       →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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining

Dependency Pair:

*'(s(s(N'')), s(s(M''))) -> *'(s(N''), s(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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 17

                 ↳Polynomial Ordering

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining

Dependency Pair:

*'(s(s(s(N''''))), s(s(s(M'''')))) -> *'(s(s(N'''')), s(s(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(s(s(N''''))), s(s(s(M'''')))) -> *'(s(s(N'''')), s(s(M'''')))

There are no usable rules for innermost that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(*'(x₁, x₂)) = 1 + x₁

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 18

                 ↳Dependency Graph

       →DP Problem 5

         ↳Nar

       →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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

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

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

QUOT(N, NzM) -> U₁₁(is_NzNat(NzM), N, NzM)

two new Dependency Pairs are created:

QUOT(N, 0) -> U₁₁(False, N, 0)
QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, N, NzM) -> U₁(gt(N, NzM), N, NzM)
QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))
U₁(True, N, NzM) -> QUOT(d(N, NzM), 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

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

U₁₁(True, N, NzM) -> U₁(gt(N, NzM), N, NzM)

three new Dependency Pairs are created:

U₁₁(True, 0, NzM') -> U₁(False, 0, NzM')
U₁₁(True, N', 0) -> U₁(u₄(is_NzNat(N')), N', 0)
U₁₁(True, s(N''), s(M')) -> U₁(gt(N'', M'), s(N''), s(M'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 20

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, N, NzM) -> QUOT(d(N, NzM), NzM)
U₁₁(True, s(N''), s(M')) -> U₁(gt(N'', M'), s(N''), s(M'))
QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))

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

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

U₁₁(True, s(N''), s(M')) -> U₁(gt(N'', M'), s(N''), s(M'))

three new Dependency Pairs are created:

U₁₁(True, s(0), s(M'')) -> U₁(False, s(0), s(M''))
U₁₁(True, s(N'''), s(0)) -> U₁(u₄(is_NzNat(N''')), s(N'''), s(0))
U₁₁(True, s(s(N')), s(s(M''))) -> U₁(gt(N', M''), s(s(N')), s(s(M'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 21

                 ↳Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(N')), s(s(M''))) -> U₁(gt(N', M''), s(s(N')), s(s(M'')))
U₁₁(True, s(N'''), s(0)) -> U₁(u₄(is_NzNat(N''')), s(N'''), s(0))
QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))
U₁(True, N, NzM) -> QUOT(d(N, NzM), 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

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

U₁(True, N, NzM) -> QUOT(d(N, NzM), NzM)

two new Dependency Pairs are created:

U₁(True, s(N'''''), s(0)) -> QUOT(d(s(N'''''), s(0)), s(0))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(s(N''')), s(s(M''''))), s(s(M'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 22

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(N'''''), s(0)) -> QUOT(d(s(N'''''), s(0)), s(0))
U₁₁(True, s(N'''), s(0)) -> U₁(u₄(is_NzNat(N''')), s(N'''), s(0))
QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(s(N''')), s(s(M''''))), s(s(M'''')))
U₁₁(True, s(s(N')), s(s(M''))) -> U₁(gt(N', M''), s(s(N')), s(s(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

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

U₁(True, s(N'''''), s(0)) -> QUOT(d(s(N'''''), s(0)), s(0))

one new Dependency Pair is created:

U₁(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 23

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(s(N''')), s(s(M''''))), s(s(M'''')))
U₁₁(True, s(s(N')), s(s(M''))) -> U₁(gt(N', M''), s(s(N')), s(s(M'')))
QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))
U₁(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))
U₁₁(True, s(N'''), s(0)) -> U₁(u₄(is_NzNat(N''')), s(N'''), s(0))

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

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

U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(s(N''')), s(s(M''''))), s(s(M'''')))

one new Dependency Pair is created:

U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(N'''), s(M'''')), s(s(M'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 24

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))
U₁₁(True, s(N'''), s(0)) -> U₁(u₄(is_NzNat(N''')), s(N'''), s(0))
QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(N'''), s(M'''')), s(s(M'''')))
U₁₁(True, s(s(N')), s(s(M''))) -> U₁(gt(N', M''), s(s(N')), s(s(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

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

U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(N'''), s(M'''')), s(s(M'''')))

one new Dependency Pair is created:

U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 25

                 ↳Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(N')), s(s(M''))) -> U₁(gt(N', M''), s(s(N')), s(s(M'')))
U₁₁(True, s(N'''), s(0)) -> U₁(u₄(is_NzNat(N''')), s(N'''), s(0))
QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))
U₁(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))

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

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

QUOT(N, s(N'')) -> U₁₁(True, N, s(N''))

two new Dependency Pairs are created:

QUOT(N', s(0)) -> U₁₁(True, N', s(0))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))

The transformation is resulting in two new DP problems:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 26

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(N')), s(s(M''))) -> U₁(gt(N', M''), s(s(N')), s(s(M'')))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(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

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

U₁₁(True, s(s(N')), s(s(M''))) -> U₁(gt(N', M''), s(s(N')), s(s(M'')))

three new Dependency Pairs are created:

U₁₁(True, s(s(0)), s(s(M'''))) -> U₁(False, s(s(0)), s(s(M''')))
U₁₁(True, s(s(N'')), s(s(0))) -> U₁(u₄(is_NzNat(N'')), s(s(N'')), s(s(0)))
U₁₁(True, s(s(s(N''))), s(s(s(M')))) -> U₁(gt(N'', M'), s(s(s(N''))), s(s(s(M'))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 29

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(N''))), s(s(s(M')))) -> U₁(gt(N'', M'), s(s(s(N''))), s(s(s(M'))))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(N'')), s(s(0))) -> U₁(u₄(is_NzNat(N'')), s(s(N'')), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(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

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

U₁₁(True, s(s(N'')), s(s(0))) -> U₁(u₄(is_NzNat(N'')), s(s(N'')), s(s(0)))

two new Dependency Pairs are created:

U₁₁(True, s(s(0)), s(s(0))) -> U₁(u₄(False), s(s(0)), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(u₄(True), s(s(s(N'))), s(s(0)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 30

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(u₄(True), s(s(s(N'))), s(s(0)))
U₁₁(True, s(s(0)), s(s(0))) -> U₁(u₄(False), s(s(0)), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(s(N''))), s(s(s(M')))) -> U₁(gt(N'', M'), s(s(s(N''))), s(s(s(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

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

U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(u₄(True), s(s(s(N'))), s(s(0)))

one new Dependency Pair is created:

U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 31

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
U₁₁(True, s(s(s(N''))), s(s(s(M')))) -> U₁(gt(N'', M'), s(s(s(N''))), s(s(s(M'))))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(0)), s(s(0))) -> U₁(u₄(False), s(s(0)), s(s(0)))

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

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

U₁₁(True, s(s(s(N''))), s(s(s(M')))) -> U₁(gt(N'', M'), s(s(s(N''))), s(s(s(M'))))

three new Dependency Pairs are created:

U₁₁(True, s(s(s(0))), s(s(s(M'')))) -> U₁(False, s(s(s(0))), s(s(s(M''))))
U₁₁(True, s(s(s(N'''))), s(s(s(0)))) -> U₁(u₄(is_NzNat(N''')), s(s(s(N'''))), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U₁(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 32

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U₁(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))
U₁₁(True, s(s(s(N'''))), s(s(s(0)))) -> U₁(u₄(is_NzNat(N''')), s(s(s(N'''))), s(s(s(0))))
U₁₁(True, s(s(0)), s(s(0))) -> U₁(u₄(False), s(s(0)), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))

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

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

U₁₁(True, s(s(0)), s(s(0))) -> U₁(u₄(False), s(s(0)), s(s(0)))

no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 33

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(N'''))), s(s(s(0)))) -> U₁(u₄(is_NzNat(N''')), s(s(s(N'''))), s(s(s(0))))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U₁(gt(N', M''), s(s(s(s(N')))), s(s(s(s(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

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

U₁₁(True, s(s(s(N'''))), s(s(s(0)))) -> U₁(u₄(is_NzNat(N''')), s(s(s(N'''))), s(s(s(0))))

two new Dependency Pairs are created:

U₁₁(True, s(s(s(0))), s(s(s(0)))) -> U₁(u₄(False), s(s(s(0))), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(u₄(True), s(s(s(s(N')))), s(s(s(0))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 34

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(u₄(True), s(s(s(s(N')))), s(s(s(0))))
U₁₁(True, s(s(s(0))), s(s(s(0)))) -> U₁(u₄(False), s(s(s(0))), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U₁(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))

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

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

U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(u₄(True), s(s(s(s(N')))), s(s(s(0))))

one new Dependency Pair is created:

U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 35

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U₁(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(s(0))), s(s(s(0)))) -> U₁(u₄(False), s(s(s(0))), s(s(s(0))))

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

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

U₁₁(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U₁(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))

three new Dependency Pairs are created:

U₁₁(True, s(s(s(s(0)))), s(s(s(s(M'''))))) -> U₁(False, s(s(s(s(0)))), s(s(s(s(M''')))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 36

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁₁(True, s(s(s(0))), s(s(s(0)))) -> U₁(u₄(False), s(s(s(0))), s(s(s(0))))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))

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

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

U₁₁(True, s(s(s(0))), s(s(s(0)))) -> U₁(u₄(False), s(s(s(0))), s(s(s(0))))

no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 37

                 ↳Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(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

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

U₁(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))

four new Dependency Pairs are created:

U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(s(N'''')), s(0)), s(s(s(0))))
U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(s(N''''')), s(s(0))), s(s(s(s(0)))))
U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(s(N'''''))), s(s(s(M''')))), s(s(s(s(s(M'''))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 38

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(s(N'''''))), s(s(s(M''')))), s(s(s(s(s(M'''))))))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(s(N'''')), s(0)), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(s(N''''')), s(s(0))), s(s(s(s(0)))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))

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

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

U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(s(N'''')), s(0)), s(s(s(0))))

one new Dependency Pair is created:

U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 39

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(s(N''''')), s(s(0))), s(s(s(s(0)))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(s(N'''''))), s(s(s(M''')))), s(s(s(s(s(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

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

U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(s(N''''')), s(s(0))), s(s(s(s(0)))))

one new Dependency Pair is created:

U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(N'''''), s(0)), s(s(s(s(0)))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 40

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(N'''''), s(0)), s(s(s(s(0)))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(s(N'''''))), s(s(s(M''')))), s(s(s(s(s(M'''))))))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(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

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

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(s(N'''''))), s(s(s(M''')))), s(s(s(s(s(M'''))))))

one new Dependency Pair is created:

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(N''''')), s(s(M'''))), s(s(s(s(s(M'''))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 41

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(N''''')), s(s(M'''))), s(s(s(s(s(M'''))))))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(N'''''), s(0)), s(s(s(s(0)))))

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

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

U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(N'''''), s(0)), s(s(s(s(0)))))

one new Dependency Pair is created:

U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 42

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(N''''')), s(s(M'''))), s(s(s(s(s(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

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

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(s(N''''')), s(s(M'''))), s(s(s(s(s(M'''))))))

one new Dependency Pair is created:

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(N'''''), s(M''')), s(s(s(s(s(M'''))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 43

                 ↳Rewriting Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(N'''''), s(M''')), s(s(s(s(s(M'''))))))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(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

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

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(s(N'''''), s(M''')), s(s(s(s(s(M'''))))))

one new Dependency Pair is created:

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(N''''', M'''), s(s(s(s(s(M'''))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 44

                 ↳Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(N''''', M'''), s(s(s(s(s(M'''))))))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))
U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))

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

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

QUOT(N', s(s(M''''''))) -> U₁₁(True, N', s(s(M'''''')))

four new Dependency Pairs are created:

QUOT(N'', s(s(0))) -> U₁₁(True, N'', s(s(0)))
QUOT(N'', s(s(s(0)))) -> U₁₁(True, N'', s(s(s(0))))
QUOT(N'', s(s(s(s(0))))) -> U₁₁(True, N'', s(s(s(s(0)))))
QUOT(N'', s(s(s(s(s(M''''')))))) -> U₁₁(True, N'', s(s(s(s(s(M'''''))))))

The transformation is resulting in four new DP problems:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 45

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
QUOT(N'', s(s(s(s(s(M''''')))))) -> U₁₁(True, N'', s(s(s(s(s(M'''''))))))
U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(N''''', M'''), s(s(s(s(s(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

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

QUOT(N'', s(s(s(s(s(M''''')))))) -> U₁₁(True, N'', s(s(s(s(s(M'''''))))))

one new Dependency Pair is created:

QUOT(s(s(s(s(s(N''''))))), s(s(s(s(s(M'''''')))))) -> U₁₁(True, s(s(s(s(s(N''''))))), s(s(s(s(s(M''''''))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
QUOT(s(s(s(s(s(N''''))))), s(s(s(s(s(M'''''')))))) -> U₁₁(True, s(s(s(s(s(N''''))))), s(s(s(s(s(M''''''))))))
U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(N''''', M'''), s(s(s(s(s(M'''))))))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(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
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 46

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

QUOT(N'', s(s(s(s(0))))) -> U₁₁(True, N'', s(s(s(s(0)))))
U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))
U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))

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

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

QUOT(N'', s(s(s(s(0))))) -> U₁₁(True, N'', s(s(s(s(0)))))

one new Dependency Pair is created:

QUOT(s(s(s(s(N'''')))), s(s(s(s(0))))) -> U₁₁(True, s(s(s(s(N'''')))), s(s(s(s(0)))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 50

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U₁(u₄(is_NzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
QUOT(s(s(s(s(N'''')))), s(s(s(s(0))))) -> U₁₁(True, s(s(s(s(N'''')))), s(s(s(s(0)))))
U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))

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

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

U₁(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))

one new Dependency Pair is created:

U₁(True, s(s(s(s(0)))), s(s(s(s(0))))) -> QUOT(0, s(s(s(s(0)))))

The transformation is resulting in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 47

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))
QUOT(N'', s(s(s(0)))) -> U₁₁(True, N'', s(s(s(0))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))

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

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

QUOT(N'', s(s(s(0)))) -> U₁₁(True, N'', s(s(s(0))))

one new Dependency Pair is created:

QUOT(s(s(s(s(N'''')))), s(s(s(0)))) -> U₁₁(True, s(s(s(s(N'''')))), s(s(s(0))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 51

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

QUOT(s(s(s(s(N'''')))), s(s(s(0)))) -> U₁₁(True, s(s(s(s(N'''')))), s(s(s(0))))
U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U₁₁(True, s(s(s(s(N')))), s(s(s(0)))) -> U₁(True, s(s(s(s(N')))), s(s(s(0))))

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

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

U₁(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))

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

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 48

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))
QUOT(N'', s(s(0))) -> U₁₁(True, N'', s(s(0)))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))

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

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

QUOT(N'', s(s(0))) -> U₁₁(True, N'', s(s(0)))

one new Dependency Pair is created:

QUOT(s(s(s(N''''))), s(s(0))) -> U₁₁(True, s(s(s(N''''))), s(s(0)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 52

                 ↳Narrowing Transformation

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

QUOT(s(s(s(N''''))), s(s(0))) -> U₁₁(True, s(s(s(N''''))), s(s(0)))
U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U₁₁(True, s(s(s(N'))), s(s(0))) -> U₁(True, s(s(s(N'))), s(s(0)))

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

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

U₁(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))

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

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 27

                 ↳Polynomial Ordering

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

QUOT(N', s(0)) -> U₁₁(True, N', s(0))
U₁(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))
U₁₁(True, s(N'''), s(0)) -> U₁(u₄(is_NzNat(N''')), s(N'''), s(0))

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:

QUOT(N', s(0)) -> U₁₁(True, N', s(0))

Additionally, the following usable rules for innermost can be oriented:

d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
u₄(True) -> True
is_NzNat(0) -> False
is_NzNat(s(N)) -> True

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(QUOT(x₁, x₂)) = 1 + x₁

POL(0) = 0

POL(False) = 0

POL(U_11(x₁, x₂, x₃)) = x₂

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

POL(u_4(x₁)) = 0

POL(True) = 0

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

POL(U_1(x₁, x₂, x₃)) = 1

POL(is_NzNat(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

           →DP Problem 19

             ↳Nar

...

               →DP Problem 28

                 ↳Dependency Graph

       →DP Problem 6

         ↳Remaining

Dependency Pairs:

U₁(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))
U₁₁(True, s(N'''), s(0)) -> U₁(u₄(is_NzNat(N''')), s(N'''), s(0))

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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
QUOT(s(s(s(s(s(N''''))))), s(s(s(s(s(M'''''')))))) -> U₁₁(True, s(s(s(s(s(N''''))))), s(s(s(s(s(M''''''))))))
U₁(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(N''''', M'''), s(s(s(s(s(M'''))))))
U₁₁(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U₁(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(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
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:04 minutes

POL(QUOT(x₁, x₂))	= 1 + x₁
POL(0)	= 0
POL(False)	= 0
POL(U_11(x₁, x₂, x₃))	= x₂
POL(d(x₁, x₂))	= x₂
POL(u_4(x₁))	= 0
POL(True)	= 0
POL(s(x₁))	= 1 + x₁
POL(U_1(x₁, x₂, x₃))	= 1
POL(is_NzNat(x₁))	= 0