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) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)

Termination of R to be shown.



   R
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) -> U4(isNzNat(NzN))
GT(NzN, 0) -> ISNZNAT(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) -> U11(isNzNat(NzM), N, NzM)
QUOT(N, NzM) -> ISNZNAT(NzM)
QUOT(NzM, NzM) -> U01(isNzNat(NzM))
QUOT(NzM, NzM) -> ISNZNAT(NzM)
QUOT(N, NzM) -> U21(isNzNat(NzM), NzM, N)
U11(True, N, NzM) -> U1(gt(N, NzM), N, NzM)
U11(True, N, NzM) -> GT(N, NzM)
U1(True, N, NzM) -> QUOT(d(N, NzM), NzM)
U1(True, N, NzM) -> D(N, NzM)
U21(True, NzM, N) -> U2(gt(NzM, N))
U21(True, NzM, N) -> GT(NzM, N)
GCD(NzM, NzM) -> U02(isNzNat(NzM), NzM)
GCD(NzM, NzM) -> ISNZNAT(NzM)
GCD(NzN, NzM) -> U31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
GCD(NzN, NzM) -> ISNZNAT(NzN)
GCD(NzN, NzM) -> ISNZNAT(NzM)
U31(True, True, NzN, NzM) -> U3(gt(NzN, NzM), NzN, NzM)
U31(True, True, NzN, NzM) -> GT(NzN, NzM)
U3(True, NzN, NzM) -> GCD(d(NzN, NzM), NzM)
U3(True, NzN, NzM) -> D(NzN, NzM)

Furthermore, R contains six SCCs.


   R
DPs
       →DP Problem 1
Polynomial Ordering
       →DP Problem 2
Polo
       →DP Problem 3
Polo
       →DP Problem 4
Polo
       →DP Problem 5
Remaining
       →DP Problem 6
Remaining


Dependency Pair:

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


Rules:


p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)





The following dependency pair can be strictly oriented:

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


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(s(x1))=  1 + x1  
  POL(+'(x1, x2))=  x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
           →DP Problem 7
Dependency Graph
       →DP Problem 2
Polo
       →DP Problem 3
Polo
       →DP Problem 4
Polo
       →DP Problem 5
Remaining
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polynomial Ordering
       →DP Problem 3
Polo
       →DP Problem 4
Polo
       →DP Problem 5
Remaining
       →DP Problem 6
Remaining


Dependency Pair:

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


Rules:


p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)





The following dependency pair can be strictly oriented:

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


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(s(x1))=  1 + x1  
  POL(GT(x1, x2))=  x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
           →DP Problem 8
Dependency Graph
       →DP Problem 3
Polo
       →DP Problem 4
Polo
       →DP Problem 5
Remaining
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polynomial Ordering
       →DP Problem 4
Polo
       →DP Problem 5
Remaining
       →DP Problem 6
Remaining


Dependency Pair:

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


Rules:


p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)





The following dependency pair can be strictly oriented:

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


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(D(x1, x2))=  x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 9
Dependency Graph
       →DP Problem 4
Polo
       →DP Problem 5
Remaining
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
       →DP Problem 4
Polynomial Ordering
       →DP Problem 5
Remaining
       →DP Problem 6
Remaining


Dependency Pair:

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


Rules:


p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)





The following dependency pair can be strictly oriented:

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


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(*'(x1, x2))=  x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
       →DP Problem 4
Polo
           →DP Problem 10
Dependency Graph
       →DP Problem 5
Remaining
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


p(s(N)) -> N
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
gt(0, M) -> False
gt(NzN, 0) -> u4(isNzNat(NzN))
gt(s(N), s(M)) -> gt(N, M)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True
lt(N, M) -> gt(M, N)
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
quot(N, NzM) -> u11(isNzNat(NzM), N, NzM)
quot(NzM, NzM) -> u01(isNzNat(NzM))
quot(N, NzM) -> u21(isNzNat(NzM), NzM, N)
u11(True, N, NzM) -> u1(gt(N, NzM), N, NzM)
u1(True, N, NzM) -> s(quot(d(N, NzM), NzM))
u01(True) -> s(0)
u21(True, NzM, N) -> u2(gt(NzM, N))
u2(True) -> 0
gcd(0, N) -> 0
gcd(NzM, NzM) -> u02(isNzNat(NzM), NzM)
gcd(NzN, NzM) -> u31(isNzNat(NzN), isNzNat(NzM), NzN, NzM)
u02(True, NzM) -> NzM
u31(True, True, NzN, NzM) -> u3(gt(NzN, NzM), NzN, NzM)
u3(True, NzN, NzM) -> gcd(d(NzN, NzM), NzM)





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
       →DP Problem 4
Polo
       →DP Problem 5
Remaining Obligation(s)
       →DP Problem 6
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
       →DP Problem 4
Polo
       →DP Problem 5
Remaining Obligation(s)
       →DP Problem 6
Remaining Obligation(s)




The following remains to be proven:

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