TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60027 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (373ms).
| – Problem 2 was processed with processor BackwardInstantiation (2ms).
| | – Problem 8 remains open; application of the following processors failed [ForwardInstantiation (2ms), Propagation (2ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (3ms), Propagation (2ms)].
| – Problem 3 was processed with processor BackwardInstantiation (2ms).
| | – Problem 9 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (2ms)].
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (2ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| u_3#(True, NzN, NzM) | → | gcd#(d(NzN, NzM), NzM) | | u_31#(True, True, NzN, NzM) | → | u_3#(gt(NzN, NzM), NzN, NzM) |
| gcd#(NzN, NzM) | → | u_31#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, u_3, gcd
Open Dependency Pair Problem 3
Dependency Pairs
| u_1#(True, N, NzM) | → | quot#(d(N, NzM), NzM) | | quot#(N, NzM) | → | u_11#(is_NzNat(NzM), N, NzM) |
| u_11#(True, N, NzM) | → | u_1#(gt(N, NzM), N, NzM) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, u_3, gcd
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| *#(s(N), s(M)) | → | +#(N, +(M, *(N, M))) | | +#(s(N), s(M)) | → | +#(N, M) |
| u_11#(True, N, NzM) | → | gt#(N, NzM) | | u_3#(True, NzN, NzM) | → | gcd#(d(NzN, NzM), NzM) |
| quot#(N, NzM) | → | is_NzNat#(NzM) | | gcd#(NzN, NzM) | → | is_NzNat#(NzM) |
| gcd#(NzM, NzM) | → | is_NzNat#(NzM) | | d#(s(N), s(M)) | → | d#(N, M) |
| gt#(NzN, 0) | → | is_NzNat#(NzN) | | quot#(NzM, NzM) | → | is_NzNat#(NzM) |
| lt#(N, M) | → | gt#(M, N) | | gt#(s(N), s(M)) | → | gt#(N, M) |
| quot#(N, NzM) | → | u_11#(is_NzNat(NzM), N, NzM) | | quot#(NzM, NzM) | → | u_01#(is_NzNat(NzM)) |
| gcd#(NzN, NzM) | → | u_31#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) | | gcd#(NzM, NzM) | → | u_02#(is_NzNat(NzM), NzM) |
| u_21#(True, NzM, N) | → | gt#(NzM, N) | | u_21#(True, NzM, N) | → | u_2#(gt(NzM, N)) |
| u_3#(True, NzN, NzM) | → | d#(NzN, NzM) | | gcd#(NzN, NzM) | → | is_NzNat#(NzN) |
| u_31#(True, True, NzN, NzM) | → | u_3#(gt(NzN, NzM), NzN, NzM) | | u_31#(True, True, NzN, NzM) | → | gt#(NzN, NzM) |
| *#(s(N), s(M)) | → | *#(N, M) | | u_1#(True, N, NzM) | → | d#(N, NzM) |
| quot#(N, NzM) | → | u_21#(is_NzNat(NzM), NzM, N) | | u_1#(True, N, NzM) | → | quot#(d(N, NzM), NzM) |
| *#(s(N), s(M)) | → | +#(M, *(N, M)) | | gt#(NzN, 0) | → | u_4#(is_NzNat(NzN)) |
| u_11#(True, N, NzM) | → | u_1#(gt(N, NzM), N, NzM) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, gcd, u_3
Strategy
The following SCCs where found
| *#(s(N), s(M)) → *#(N, M) |
| +#(s(N), s(M)) → +#(N, M) |
| u_3#(True, NzN, NzM) → gcd#(d(NzN, NzM), NzM) | u_31#(True, True, NzN, NzM) → u_3#(gt(NzN, NzM), NzN, NzM) |
| gcd#(NzN, NzM) → u_31#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_1#(True, N, NzM) → quot#(d(N, NzM), NzM) | quot#(N, NzM) → u_11#(is_NzNat(NzM), N, NzM) |
| u_11#(True, N, NzM) → u_1#(gt(N, NzM), N, NzM) |
| gt#(s(N), s(M)) → gt#(N, M) |
| d#(s(N), s(M)) → d#(N, M) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| u_3#(True, NzN, NzM) | → | gcd#(d(NzN, NzM), NzM) | | u_31#(True, True, NzN, NzM) | → | u_3#(gt(NzN, NzM), NzN, NzM) |
| gcd#(NzN, NzM) | → | u_31#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, gcd, u_3
Strategy
Instantiation
For all potential predecessors l → r of the rule gcd
#(
NzN,
NzM) → u_31
#(is_NzNat(
NzN), is_NzNat(
NzM),
NzN,
NzM) on dependency pair chains it holds that:
- gcd#(NzN, NzM) matches r,
- all variables of gcd#(NzN, NzM) are embedded in constructor contexts, i.e., each subterm of gcd#(NzN, NzM), containing a variable is rooted by a constructor symbol.
Thus, gcd
#(
NzN,
NzM) → u_31
#(is_NzNat(
NzN), is_NzNat(
NzM),
NzN,
NzM) is replaced by instances determined through the above matching. These instances are:
| gcd#(d(_NzN, _NzM), _NzM) → u_31#(is_NzNat(d(_NzN, _NzM)), is_NzNat(_NzM), d(_NzN, _NzM), _NzM) |
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| u_1#(True, N, NzM) | → | quot#(d(N, NzM), NzM) | | quot#(N, NzM) | → | u_11#(is_NzNat(NzM), N, NzM) |
| u_11#(True, N, NzM) | → | u_1#(gt(N, NzM), N, NzM) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, gcd, u_3
Strategy
Instantiation
For all potential predecessors l → r of the rule quot
#(
N,
NzM) → u_11
#(is_NzNat(
NzM),
N,
NzM) on dependency pair chains it holds that:
- quot#(N, NzM) matches r,
- all variables of quot#(N, NzM) are embedded in constructor contexts, i.e., each subterm of quot#(N, NzM), containing a variable is rooted by a constructor symbol.
Thus, quot
#(
N,
NzM) → u_11
#(is_NzNat(
NzM),
N,
NzM) is replaced by instances determined through the above matching. These instances are:
| quot#(d(_N, _NzM), _NzM) → u_11#(is_NzNat(_NzM), d(_N, _NzM), _NzM) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| *#(s(N), s(M)) | → | *#(N, M) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, gcd, u_3
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| *#(s(N), s(M)) | → | *#(N, M) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| +#(s(N), s(M)) | → | +#(N, M) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, gcd, u_3
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| +#(s(N), s(M)) | → | +#(N, M) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| d#(s(N), s(M)) | → | d#(N, M) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, gcd, u_3
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| d#(s(N), s(M)) | → | d#(N, M) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| gt#(s(N), s(M)) | → | gt#(N, M) |
Rewrite 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_4(is_NzNat(NzN)) | | u_4(True) | → | True |
| is_NzNat(0) | → | False | | is_NzNat(s(N)) | → | True |
| gt(s(N), s(M)) | → | gt(N, M) | | lt(N, M) | → | gt(M, N) |
| d(0, N) | → | N | | d(s(N), s(M)) | → | d(N, M) |
| quot(N, NzM) | → | u_11(is_NzNat(NzM), N, NzM) | | u_11(True, N, NzM) | → | u_1(gt(N, NzM), N, NzM) |
| u_1(True, N, NzM) | → | s(quot(d(N, NzM), NzM)) | | quot(NzM, NzM) | → | u_01(is_NzNat(NzM)) |
| u_01(True) | → | s(0) | | quot(N, NzM) | → | u_21(is_NzNat(NzM), NzM, N) |
| u_21(True, NzM, N) | → | u_2(gt(NzM, N)) | | u_2(True) | → | 0 |
| gcd(0, N) | → | 0 | | gcd(NzM, NzM) | → | u_02(is_NzNat(NzM), NzM) |
| u_02(True, NzM) | → | NzM | | gcd(NzN, NzM) | → | u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) |
| u_31(True, True, NzN, NzM) | → | u_3(gt(NzN, NzM), NzN, NzM) | | u_3(True, NzN, NzM) | → | gcd(d(NzN, NzM), NzM) |
Original Signature
Termination of terms over the following signature is verified: u_31, is_NzNat, u_02, d, u_21, u_01, u_11, *, +, lt, False, u_1, 0, s, p, True, gt, u_4, quot, u_2, gcd, u_3
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| gt#(s(N), s(M)) | → | gt#(N, M) |