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)

Innermost 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
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) -> 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)


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:



   R
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) -> 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)


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:



   R
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) -> 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)


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(x1))=  1 + x1  
  POL(+'(x1, x2))=  1 + x1  

resulting in one new DP problem.



   R
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) -> 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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
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) -> 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)


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:



   R
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) -> 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)


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:



   R
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) -> 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)


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(x1))=  1 + x1  
  POL(GT(x1, x2))=  1 + x1  

resulting in one new DP problem.



   R
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) -> 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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
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) -> 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)


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:



   R
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) -> 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)


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:



   R
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) -> 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)


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(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
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) -> 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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
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) -> 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)


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:



   R
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) -> 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)


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:



   R
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) -> 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)


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(*'(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
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) -> 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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
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:

U1(True, N, NzM) -> QUOT(d(N, NzM), NzM)
U11(True, N, NzM) -> U1(gt(N, NzM), N, NzM)
QUOT(N, NzM) -> U11(isNzNat(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) -> 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)


Strategy:

innermost




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

QUOT(N, NzM) -> U11(isNzNat(NzM), N, NzM)
two new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:



   R
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:

U11(True, N, NzM) -> U1(gt(N, NzM), N, NzM)
QUOT(N, s(N'')) -> U11(True, N, s(N''))
U1(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) -> 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)


Strategy:

innermost




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

U11(True, N, NzM) -> U1(gt(N, NzM), N, NzM)
three new Dependency Pairs are created:

U11(True, 0, NzM') -> U1(False, 0, NzM')
U11(True, N', 0) -> U1(u4(isNzNat(N')), N', 0)
U11(True, s(N''), s(M')) -> U1(gt(N'', M'), s(N''), s(M'))

The transformation is resulting in one new DP problem:



   R
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:

U1(True, N, NzM) -> QUOT(d(N, NzM), NzM)
U11(True, s(N''), s(M')) -> U1(gt(N'', M'), s(N''), s(M'))
QUOT(N, s(N'')) -> U11(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) -> 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)


Strategy:

innermost




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

U11(True, s(N''), s(M')) -> U1(gt(N'', M'), s(N''), s(M'))
three new Dependency Pairs are created:

U11(True, s(0), s(M'')) -> U1(False, s(0), s(M''))
U11(True, s(N'''), s(0)) -> U1(u4(isNzNat(N''')), s(N'''), s(0))
U11(True, s(s(N')), s(s(M''))) -> U1(gt(N', M''), s(s(N')), s(s(M'')))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(N')), s(s(M''))) -> U1(gt(N', M''), s(s(N')), s(s(M'')))
U11(True, s(N'''), s(0)) -> U1(u4(isNzNat(N''')), s(N'''), s(0))
QUOT(N, s(N'')) -> U11(True, N, s(N''))
U1(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) -> 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)


Strategy:

innermost




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

U1(True, N, NzM) -> QUOT(d(N, NzM), NzM)
two new Dependency Pairs are created:

U1(True, s(N'''''), s(0)) -> QUOT(d(s(N'''''), s(0)), s(0))
U1(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:



   R
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:

U1(True, s(N'''''), s(0)) -> QUOT(d(s(N'''''), s(0)), s(0))
U11(True, s(N'''), s(0)) -> U1(u4(isNzNat(N''')), s(N'''), s(0))
QUOT(N, s(N'')) -> U11(True, N, s(N''))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(s(N''')), s(s(M''''))), s(s(M'''')))
U11(True, s(s(N')), s(s(M''))) -> U1(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) -> 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)


Strategy:

innermost




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

U1(True, s(N'''''), s(0)) -> QUOT(d(s(N'''''), s(0)), s(0))
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:



   R
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:

U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(s(N''')), s(s(M''''))), s(s(M'''')))
U11(True, s(s(N')), s(s(M''))) -> U1(gt(N', M''), s(s(N')), s(s(M'')))
QUOT(N, s(N'')) -> U11(True, N, s(N''))
U1(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))
U11(True, s(N'''), s(0)) -> U1(u4(isNzNat(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) -> 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)


Strategy:

innermost




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

U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(s(N''')), s(s(M''''))), s(s(M'''')))
one new Dependency Pair is created:

U1(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:



   R
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:

U1(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))
U11(True, s(N'''), s(0)) -> U1(u4(isNzNat(N''')), s(N'''), s(0))
QUOT(N, s(N'')) -> U11(True, N, s(N''))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(N'''), s(M'''')), s(s(M'''')))
U11(True, s(s(N')), s(s(M''))) -> U1(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) -> 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)


Strategy:

innermost




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

U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(s(N'''), s(M'''')), s(s(M'''')))
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:



   R
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:

U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(N')), s(s(M''))) -> U1(gt(N', M''), s(s(N')), s(s(M'')))
U11(True, s(N'''), s(0)) -> U1(u4(isNzNat(N''')), s(N'''), s(0))
QUOT(N, s(N'')) -> U11(True, N, s(N''))
U1(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) -> 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)


Strategy:

innermost




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

QUOT(N, s(N'')) -> U11(True, N, s(N''))
two new Dependency Pairs are created:

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

The transformation is resulting in two new DP problems:



   R
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:

U11(True, s(s(N')), s(s(M''))) -> U1(gt(N', M''), s(s(N')), s(s(M'')))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(N')), s(s(M''))) -> U1(gt(N', M''), s(s(N')), s(s(M'')))
three new Dependency Pairs are created:

U11(True, s(s(0)), s(s(M'''))) -> U1(False, s(s(0)), s(s(M''')))
U11(True, s(s(N'')), s(s(0))) -> U1(u4(isNzNat(N'')), s(s(N'')), s(s(0)))
U11(True, s(s(s(N''))), s(s(s(M')))) -> U1(gt(N'', M'), s(s(s(N''))), s(s(s(M'))))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(N''))), s(s(s(M')))) -> U1(gt(N'', M'), s(s(s(N''))), s(s(s(M'))))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(N'')), s(s(0))) -> U1(u4(isNzNat(N'')), s(s(N'')), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(N'')), s(s(0))) -> U1(u4(isNzNat(N'')), s(s(N'')), s(s(0)))
two new Dependency Pairs are created:

U11(True, s(s(0)), s(s(0))) -> U1(u4(False), s(s(0)), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(u4(True), s(s(s(N'))), s(s(0)))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(N'))), s(s(0))) -> U1(u4(True), s(s(s(N'))), s(s(0)))
U11(True, s(s(0)), s(s(0))) -> U1(u4(False), s(s(0)), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(s(N''))), s(s(s(M')))) -> U1(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(s(N'))), s(s(0))) -> U1(u4(True), s(s(s(N'))), s(s(0)))
one new Dependency Pair is created:

U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
U11(True, s(s(s(N''))), s(s(s(M')))) -> U1(gt(N'', M'), s(s(s(N''))), s(s(s(M'))))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(0)), s(s(0))) -> U1(u4(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(s(N''))), s(s(s(M')))) -> U1(gt(N'', M'), s(s(s(N''))), s(s(s(M'))))
three new Dependency Pairs are created:

U11(True, s(s(s(0))), s(s(s(M'')))) -> U1(False, s(s(s(0))), s(s(s(M''))))
U11(True, s(s(s(N'''))), s(s(s(0)))) -> U1(u4(isNzNat(N''')), s(s(s(N'''))), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U1(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U1(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))
U11(True, s(s(s(N'''))), s(s(s(0)))) -> U1(u4(isNzNat(N''')), s(s(s(N'''))), s(s(s(0))))
U11(True, s(s(0)), s(s(0))) -> U1(u4(False), s(s(0)), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(s(N'))), s(s(0))) -> U1(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(0)), s(s(0))) -> U1(u4(False), s(s(0)), s(s(0)))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(N'''))), s(s(s(0)))) -> U1(u4(isNzNat(N''')), s(s(s(N'''))), s(s(s(0))))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U1(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(s(N'''))), s(s(s(0)))) -> U1(u4(isNzNat(N''')), s(s(s(N'''))), s(s(s(0))))
two new Dependency Pairs are created:

U11(True, s(s(s(0))), s(s(s(0)))) -> U1(u4(False), s(s(s(0))), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(u4(True), s(s(s(s(N')))), s(s(s(0))))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(u4(True), s(s(s(s(N')))), s(s(s(0))))
U11(True, s(s(s(0))), s(s(s(0)))) -> U1(u4(False), s(s(s(0))), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U1(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(s(N'))), s(s(0))) -> U1(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(u4(True), s(s(s(s(N')))), s(s(s(0))))
one new Dependency Pair is created:

U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U1(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(s(0))), s(s(s(0)))) -> U1(u4(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(s(s(N')))), s(s(s(s(M''))))) -> U1(gt(N', M''), s(s(s(s(N')))), s(s(s(s(M'')))))
three new Dependency Pairs are created:

U11(True, s(s(s(s(0)))), s(s(s(s(M'''))))) -> U1(False, s(s(s(s(0)))), s(s(s(s(M''')))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U11(True, s(s(s(0))), s(s(s(0)))) -> U1(u4(False), s(s(s(0))), s(s(s(0))))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(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) -> 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)


Strategy:

innermost




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

U11(True, s(s(s(0))), s(s(s(0)))) -> U1(u4(False), s(s(s(0))), s(s(s(0))))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(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) -> 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)


Strategy:

innermost




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

U1(True, s(s(N''')), s(s(M''''))) -> QUOT(d(N''', M''''), s(s(M'''')))
four new Dependency Pairs are created:

U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(s(N'''')), s(0)), s(s(s(0))))
U1(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(s(N''''')), s(s(0))), s(s(s(s(0)))))
U1(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:



   R
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:

U1(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'''))))))
U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(s(N'''')), s(0)), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(s(N''''')), s(s(0))), s(s(s(s(0)))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(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) -> 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)


Strategy:

innermost




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

U1(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:

U1(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:



   R
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:

U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U1(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(s(N''''')), s(s(0))), s(s(s(s(0)))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(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) -> 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)


Strategy:

innermost




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

U1(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:

U1(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:



   R
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:

U1(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(s(N'''''), s(0)), s(s(s(s(0)))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(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'''))))))
U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(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) -> 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)


Strategy:

innermost




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

U1(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:

U1(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:



   R
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:

U1(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'''))))))
U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(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) -> 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)


Strategy:

innermost




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

U1(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:

U1(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:



   R
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:

U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U1(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(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) -> 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)


Strategy:

innermost




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

U1(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:

U1(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:



   R
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:

U1(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(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'''))))))
U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(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) -> 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)


Strategy:

innermost




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

U1(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:

U1(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:



   R
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:

U1(True, s(s(s(s(s(N'''''))))), s(s(s(s(s(M''')))))) -> QUOT(d(N''''', M'''), s(s(s(s(s(M'''))))))
U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N', s(s(M''''''))) -> U11(True, N', s(s(M'''''')))
U1(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) -> 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)


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''''''))) -> U11(True, N', s(s(M'''''')))
four new Dependency Pairs are created:

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

The transformation is resulting in four new DP problems:



   R
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:

U11(True, s(s(s(s(s(N''))))), s(s(s(s(s(M')))))) -> U1(gt(N'', M'), s(s(s(s(s(N''))))), s(s(s(s(s(M'))))))
QUOT(N'', s(s(s(s(s(M''''')))))) -> U11(True, N'', s(s(s(s(s(M'''''))))))
U1(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) -> 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)


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

The transformation is resulting in one new DP problem:



   R
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:


   R
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))))) -> U11(True, N'', s(s(s(s(0)))))
U1(True, s(s(s(s(N''''')))), s(s(s(s(0))))) -> QUOT(d(N''''', 0), s(s(s(s(0)))))
U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(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) -> 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)


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))))) -> U11(True, N'', s(s(s(s(0)))))
one new Dependency Pair is created:

QUOT(s(s(s(s(N'''')))), s(s(s(s(0))))) -> U11(True, s(s(s(s(N'''')))), s(s(s(s(0)))))

The transformation is resulting in one new DP problem:



   R
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:

U11(True, s(s(s(s(N'')))), s(s(s(s(0))))) -> U1(u4(isNzNat(N'')), s(s(s(s(N'')))), s(s(s(s(0)))))
QUOT(s(s(s(s(N'''')))), s(s(s(s(0))))) -> U11(True, s(s(s(s(N'''')))), s(s(s(s(0)))))
U1(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) -> 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)


Strategy:

innermost




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

U1(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:

U1(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.



   R
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:

U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(True, s(s(s(s(N')))), s(s(s(0))))
QUOT(N'', s(s(s(0)))) -> U11(True, N'', s(s(s(0))))
U1(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) -> 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)


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)))) -> U11(True, N'', s(s(s(0))))
one new Dependency Pair is created:

QUOT(s(s(s(s(N'''')))), s(s(s(0)))) -> U11(True, s(s(s(s(N'''')))), s(s(s(0))))

The transformation is resulting in one new DP problem:



   R
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)))) -> U11(True, s(s(s(s(N'''')))), s(s(s(0))))
U1(True, s(s(s(s(N'''')))), s(s(s(0)))) -> QUOT(d(s(N''''), 0), s(s(s(0))))
U11(True, s(s(s(s(N')))), s(s(s(0)))) -> U1(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) -> 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)


Strategy:

innermost




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

U1(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.



   R
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:

U11(True, s(s(s(N'))), s(s(0))) -> U1(True, s(s(s(N'))), s(s(0)))
QUOT(N'', s(s(0))) -> U11(True, N'', s(s(0)))
U1(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) -> 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)


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))) -> U11(True, N'', s(s(0)))
one new Dependency Pair is created:

QUOT(s(s(s(N''''))), s(s(0))) -> U11(True, s(s(s(N''''))), s(s(0)))

The transformation is resulting in one new DP problem:



   R
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))) -> U11(True, s(s(s(N''''))), s(s(0)))
U1(True, s(s(s(N''''))), s(s(0))) -> QUOT(d(s(N''''), 0), s(s(0)))
U11(True, s(s(s(N'))), s(s(0))) -> U1(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) -> 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)


Strategy:

innermost




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

U1(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.



   R
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)) -> U11(True, N', s(0))
U1(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))
U11(True, s(N'''), s(0)) -> U1(u4(isNzNat(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) -> 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)


Strategy:

innermost




The following dependency pair can be strictly oriented:

QUOT(N', s(0)) -> U11(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)
u4(True) -> True
isNzNat(0) -> False
isNzNat(s(N)) -> True


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(QUOT(x1, x2))=  1 + x1  
  POL(0)=  0  
  POL(False)=  0  
  POL(U_11(x1, x2, x3))=  x2  
  POL(d(x1, x2))=  x2  
  POL(u_4(x1))=  0  
  POL(True)=  0  
  POL(s(x1))=  1 + x1  
  POL(U_1(x1, x2, x3))=  1  
  POL(is_NzNat(x1))=  0  

resulting in one new DP problem.



   R
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:

U1(True, s(N'''''), s(0)) -> QUOT(d(N''''', 0), s(0))
U11(True, s(N'''), s(0)) -> U1(u4(isNzNat(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) -> 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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
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:

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