The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

m2(S(0), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0, b, res, True) → False
m3(S(0), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0, b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0
help1(S(0)) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0)), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0, y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0) → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0, tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0, False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
m2(S(0), z0, z1, True) → False
m2(S(S(z0)), z1, z2, True) → True
m2(0, z0, z1, True) → False
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m3(S(0), z0, z1, z2) → False
m3(S(S(z0)), z1, z2, z3) → True
m3(0, z0, z1, z2) → False
l8(z0, z1, z2, True, z3, z4) → z0
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4)
l5(z0, z1, z2, z3, z4, True) → 0
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False)
help1(S(0)) → False
help1(S(S(z0))) → True
help1(0) → False
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4)
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4)
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4)
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False)
l2(z0, z1, z2, z3, z4, True) → z2
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False)
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
l9(z0, z1, z2, z3, z4, z5) → z0
l6(z0, z1, z2, z3, z4, z5) → 0
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False)
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False)
e7(z0, z1, z2, z3) → False
e6(z0, z1, z2, z3) → False
e5(z0, z1, z2, z3) → True
monus(z0, z1) → m1(z0, z1, False, False)
m5(z0, z1, z2, z3) → z2
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5)
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5)
l16(z0, z1, z2, z3, z4, z5) → z2
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5)
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5)
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1))
gcd(z0, z1) → l1(z0, z1, 0, False, False, False)
equal0(z0, z1) → e1(z0, z1, False, False)
e8(z0, z1, z2, z3) → z2
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
<'(0, S(z0)) → c1
<'(z0, 0) → c2
M2(S(0), z0, z1, True) → c3
M2(S(S(z0)), z1, z2, True) → c4
M2(0, z0, z1, True) → c5
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
M3(S(0), z0, z1, z2) → c7
M3(S(S(z0)), z1, z2, z3) → c8
M3(0, z0, z1, z2) → c9
L8(z0, z1, z2, True, z3, z4) → c10
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, True) → c12
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
HELP1(S(0)) → c14
HELP1(S(S(z0))) → c15
HELP1(0) → c16
E4(z0, z1, z2, False) → c17
E4(z0, z1, z2, True) → c18
E2(z0, z1, z2, False) → c19
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L15(z0, z1, z2, z3, False, z4) → c21(L16(z0, z1, gcd(z1, 0), z3, False, z4), GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(L16(z0, z1, gcd(z1, S(0)), z3, True, z4), GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(L16(z0, z1, gcd(0, z1), z3, False, z4), GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(L16(z0, z1, gcd(S(0), z1), z3, True, z4), GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(M5(S(z0), S(z1), monus(z0, z1), z3), MONUS(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L2(z0, z1, z2, z3, z4, True) → c27
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
BOOL2NAT(False) → c30
BOOL2NAT(True) → c31
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L9(z0, z1, z2, z3, z4, z5) → c33
L6(z0, z1, z2, z3, z4, z5) → c34
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
E7(z0, z1, z2, z3) → c37
E6(z0, z1, z2, z3) → c38
E5(z0, z1, z2, z3) → c39
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
M5(z0, z1, z2, z3) → c41
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L16(z0, z1, z2, z3, z4, z5) → c44
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
E8(z0, z1, z2, z3) → c50
E3(z0, z1, z2, z3) → c51(E4(z0, z1, z2, <(z1, z0)), <'(z1, z0))
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))

S tuples:

M2(S(0), z0, z1, True) → c3
M2(S(S(z0)), z1, z2, True) → c4
M2(0, z0, z1, True) → c5
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
M3(S(0), z0, z1, z2) → c7
M3(S(S(z0)), z1, z2, z3) → c8
M3(0, z0, z1, z2) → c9
L8(z0, z1, z2, True, z3, z4) → c10
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, True) → c12
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
HELP1(S(0)) → c14
HELP1(S(S(z0))) → c15
HELP1(0) → c16
E4(z0, z1, z2, False) → c17
E4(z0, z1, z2, True) → c18
E2(z0, z1, z2, False) → c19
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L15(z0, z1, z2, z3, False, z4) → c21(L16(z0, z1, gcd(z1, 0), z3, False, z4), GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(L16(z0, z1, gcd(z1, S(0)), z3, True, z4), GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(L16(z0, z1, gcd(0, z1), z3, False, z4), GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(L16(z0, z1, gcd(S(0), z1), z3, True, z4), GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(M5(S(z0), S(z1), monus(z0, z1), z3), MONUS(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L2(z0, z1, z2, z3, z4, True) → c27
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
BOOL2NAT(False) → c30
BOOL2NAT(True) → c31
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L9(z0, z1, z2, z3, z4, z5) → c33
L6(z0, z1, z2, z3, z4, z5) → c34
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
E7(z0, z1, z2, z3) → c37
E6(z0, z1, z2, z3) → c38
E5(z0, z1, z2, z3) → c39
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
M5(z0, z1, z2, z3) → c41
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L16(z0, z1, z2, z3, z4, z5) → c44
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
E8(z0, z1, z2, z3) → c50
E3(z0, z1, z2, z3) → c51(E4(z0, z1, z2, <(z1, z0)), <'(z1, z0))
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))

K tuples:none
Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, M3, L8, L5, HELP1, E4, E2, L15, L13, M4, L2, L11, BOOL2NAT, M1, L9, L6, L4, L1, E7, E6, E5, MONUS, M5, L7, L3, L16, L14, L12, L10, GCD, EQUAL0, E8, E3, E1

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 27 trailing nodes:

E2(z0, z1, z2, False) → c19
E6(z0, z1, z2, z3) → c38
HELP1(S(0)) → c14
E5(z0, z1, z2, z3) → c39
M2(S(0), z0, z1, True) → c3
E7(z0, z1, z2, z3) → c37
L9(z0, z1, z2, z3, z4, z5) → c33
M2(0, z0, z1, True) → c5
E8(z0, z1, z2, z3) → c50
L6(z0, z1, z2, z3, z4, z5) → c34
M3(S(0), z0, z1, z2) → c7
M3(0, z0, z1, z2) → c9
L2(z0, z1, z2, z3, z4, True) → c27
E4(z0, z1, z2, False) → c17
M2(S(S(z0)), z1, z2, True) → c4
<'(0, S(z0)) → c1
BOOL2NAT(False) → c30
L5(z0, z1, z2, z3, z4, True) → c12
L16(z0, z1, z2, z3, z4, z5) → c44
BOOL2NAT(True) → c31
HELP1(0) → c16
<'(z0, 0) → c2
M3(S(S(z0)), z1, z2, z3) → c8
E4(z0, z1, z2, True) → c18
L8(z0, z1, z2, True, z3, z4) → c10
HELP1(S(S(z0))) → c15
M5(z0, z1, z2, z3) → c41

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
m2(S(0), z0, z1, True) → False
m2(S(S(z0)), z1, z2, True) → True
m2(0, z0, z1, True) → False
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m3(S(0), z0, z1, z2) → False
m3(S(S(z0)), z1, z2, z3) → True
m3(0, z0, z1, z2) → False
l8(z0, z1, z2, True, z3, z4) → z0
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4)
l5(z0, z1, z2, z3, z4, True) → 0
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False)
help1(S(0)) → False
help1(S(S(z0))) → True
help1(0) → False
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4)
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4)
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4)
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False)
l2(z0, z1, z2, z3, z4, True) → z2
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False)
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
l9(z0, z1, z2, z3, z4, z5) → z0
l6(z0, z1, z2, z3, z4, z5) → 0
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False)
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False)
e7(z0, z1, z2, z3) → False
e6(z0, z1, z2, z3) → False
e5(z0, z1, z2, z3) → True
monus(z0, z1) → m1(z0, z1, False, False)
m5(z0, z1, z2, z3) → z2
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5)
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5)
l16(z0, z1, z2, z3, z4, z5) → z2
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5)
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5)
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1))
gcd(z0, z1) → l1(z0, z1, 0, False, False, False)
equal0(z0, z1) → e1(z0, z1, False, False)
e8(z0, z1, z2, z3) → z2
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L15(z0, z1, z2, z3, False, z4) → c21(L16(z0, z1, gcd(z1, 0), z3, False, z4), GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(L16(z0, z1, gcd(z1, S(0)), z3, True, z4), GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(L16(z0, z1, gcd(0, z1), z3, False, z4), GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(L16(z0, z1, gcd(S(0), z1), z3, True, z4), GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(M5(S(z0), S(z1), monus(z0, z1), z3), MONUS(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
E3(z0, z1, z2, z3) → c51(E4(z0, z1, z2, <(z1, z0)), <'(z1, z0))
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L15(z0, z1, z2, z3, False, z4) → c21(L16(z0, z1, gcd(z1, 0), z3, False, z4), GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(L16(z0, z1, gcd(z1, S(0)), z3, True, z4), GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(L16(z0, z1, gcd(0, z1), z3, False, z4), GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(L16(z0, z1, gcd(S(0), z1), z3, True, z4), GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(M5(S(z0), S(z1), monus(z0, z1), z3), MONUS(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
E3(z0, z1, z2, z3) → c51(E4(z0, z1, z2, <(z1, z0)), <'(z1, z0))
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))

K tuples:none
Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L15, L13, M4, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c21, c22, c23, c24, c25, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c51, c52

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 6 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
m2(S(0), z0, z1, True) → False
m2(S(S(z0)), z1, z2, True) → True
m2(0, z0, z1, True) → False
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m3(S(0), z0, z1, z2) → False
m3(S(S(z0)), z1, z2, z3) → True
m3(0, z0, z1, z2) → False
l8(z0, z1, z2, True, z3, z4) → z0
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4)
l5(z0, z1, z2, z3, z4, True) → 0
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False)
help1(S(0)) → False
help1(S(S(z0))) → True
help1(0) → False
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4)
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4)
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4)
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False)
l2(z0, z1, z2, z3, z4, True) → z2
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False)
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
l9(z0, z1, z2, z3, z4, z5) → z0
l6(z0, z1, z2, z3, z4, z5) → 0
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False)
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False)
e7(z0, z1, z2, z3) → False
e6(z0, z1, z2, z3) → False
e5(z0, z1, z2, z3) → True
monus(z0, z1) → m1(z0, z1, False, False)
m5(z0, z1, z2, z3) → z2
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5)
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5)
l16(z0, z1, z2, z3, z4, z5) → z2
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5)
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5)
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1))
gcd(z0, z1) → l1(z0, z1, 0, False, False, False)
equal0(z0, z1) → e1(z0, z1, False, False)
e8(z0, z1, z2, z3) → z2
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))

K tuples:none
Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, E1, L15, L13, M4, E3

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c52, c21, c22, c23, c24, c25, c51

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
m2(S(0), z0, z1, True) → False
m2(S(S(z0)), z1, z2, True) → True
m2(0, z0, z1, True) → False
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m3(S(0), z0, z1, z2) → False
m3(S(S(z0)), z1, z2, z3) → True
m3(0, z0, z1, z2) → False
l8(z0, z1, z2, True, z3, z4) → z0
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4)
l5(z0, z1, z2, z3, z4, True) → 0
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False)
help1(S(0)) → False
help1(S(S(z0))) → True
help1(0) → False
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4)
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4)
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4)
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False)
l2(z0, z1, z2, z3, z4, True) → z2
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False)
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
l9(z0, z1, z2, z3, z4, z5) → z0
l6(z0, z1, z2, z3, z4, z5) → 0
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False)
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False)
e7(z0, z1, z2, z3) → False
e6(z0, z1, z2, z3) → False
e5(z0, z1, z2, z3) → True
monus(z0, z1) → m1(z0, z1, False, False)
m5(z0, z1, z2, z3) → z2
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5)
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5)
l16(z0, z1, z2, z3, z4, z5) → z2
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5)
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5)
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1))
gcd(z0, z1) → l1(z0, z1, 0, False, False, False)
equal0(z0, z1) → e1(z0, z1, False, False)
e8(z0, z1, z2, z3) → z2
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:none
Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

m2(S(0), z0, z1, True) → False
m2(S(S(z0)), z1, z2, True) → True
m2(0, z0, z1, True) → False
m3(S(0), z0, z1, z2) → False
m3(S(S(z0)), z1, z2, z3) → True
m3(0, z0, z1, z2) → False
l8(z0, z1, z2, True, z3, z4) → z0
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4)
l5(z0, z1, z2, z3, z4, True) → 0
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False)
help1(S(0)) → False
help1(S(S(z0))) → True
help1(0) → False
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4)
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4)
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4)
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4)
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False)
l2(z0, z1, z2, z3, z4, True) → z2
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False)
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
l9(z0, z1, z2, z3, z4, z5) → z0
l6(z0, z1, z2, z3, z4, z5) → 0
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False)
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False)
e7(z0, z1, z2, z3) → False
e6(z0, z1, z2, z3) → False
e5(z0, z1, z2, z3) → True
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5)
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5)
l16(z0, z1, z2, z3, z4, z5) → z2
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5)
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5)
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1))
gcd(z0, z1) → l1(z0, z1, 0, False, False, False)
e8(z0, z1, z2, z3) → z2

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → e1(z0, z1, False, False)
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
monus(z0, z1) → m1(z0, z1, False, False)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:none
Defined Rule Symbols:

equal0, e1, e2, <, e3, e4, monus, m1, m2, m4, m5

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))

We considered the (Usable) Rules:

m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
monus(z0, z1) → m1(z0, z1, False, False)

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(<(x₁, x₂)) = 0   
POL(<'(x₁, x₂)) = 0   
POL(E1(x₁, x₂, x₃, x₄)) = [4]x₃ + [3]x₄   
POL(E2(x₁, x₂, x₃, x₄)) = [3]x₃   
POL(E3(x₁, x₂, x₃, x₄)) = [2]x₃   
POL(EQUAL0(x₁, x₂)) = 0   
POL(False) = 0   
POL(GCD(x₁, x₂)) = [4]x₁ + [4]x₂   
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = [3]x₁ + [4]x₂ + [4]x₃ + [3]x₄ + [4]x₅ + x₆   
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₂ + [4]x₄ + [3]x₆   
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₂ + [4]x₄   
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₂ + [2]x₄   
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₂ + [2]x₄   
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₂ + [4]x₄   
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₂ + [2]x₄ + x₅   
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + [2]x₃ + [3]x₄ + [4]x₅ + [3]x₆   
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + [2]x₃ + [3]x₄ + [4]x₅ + [2]x₆   
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + x₃ + [3]x₄ + [3]x₅   
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + [3]x₄ + [3]x₅ + [3]x₆   
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + [3]x₄ + [3]x₆   
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₂ + [3]x₆   
POL(M1(x₁, x₂, x₃, x₄)) = [4]x₃ + [2]x₄   
POL(M2(x₁, x₂, x₃, x₄)) = [2]x₃ + x₄   
POL(M4(x₁, x₂, x₃, x₄)) = [2]x₃ + [3]x₄   
POL(MONUS(x₁, x₂)) = 0   
POL(S(x₁)) = 0   
POL(True) = [4]   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c25(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c28(x₁)) = x₁   
POL(c29(x₁)) = x₁   
POL(c32(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c36(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c42(x₁, x₂)) = x₁ + x₂   
POL(c43(x₁)) = x₁   
POL(c45(x₁, x₂)) = x₁ + x₂   
POL(c46(x₁, x₂)) = x₁ + x₂   
POL(c47(x₁, x₂)) = x₁ + x₂   
POL(c48(x₁)) = x₁   
POL(c49(x₁)) = x₁   
POL(c51(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(e1(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [4]x₂ + [2]x₃ + x₄   
POL(e2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + x₂ + [4]x₃ + [3]x₄   
POL(e3(x₁, x₂, x₃, x₄)) = [3] + [4]x₁ + [4]x₂ + [3]x₃ + [5]x₄   
POL(e4(x₁, x₂, x₃, x₄)) = [5] + [3]x₁ + [2]x₂ + x₃   
POL(equal0(x₁, x₂)) = [5]x₁ + [3]x₂   
POL(m1(x₁, x₂, x₃, x₄)) = [3]x₃ + [5]x₄   
POL(m2(x₁, x₂, x₃, x₄)) = [2]x₄   
POL(m4(x₁, x₂, x₃, x₄)) = [2]x₄   
POL(m5(x₁, x₂, x₃, x₄)) = x₁ + [2]x₂ + [2]x₃ + [2]x₄   
POL(monus(x₁, x₂)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → e1(z0, z1, False, False)
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
monus(z0, z1) → m1(z0, z1, False, False)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))

Defined Rule Symbols:

equal0, e1, e2, <, e3, e4, monus, m1, m2, m4, m5

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))

We considered the (Usable) Rules:

m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
monus(z0, z1) → m1(z0, z1, False, False)

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(<(x₁, x₂)) = 0   
POL(<'(x₁, x₂)) = 0   
POL(E1(x₁, x₂, x₃, x₄)) = 0   
POL(E2(x₁, x₂, x₃, x₄)) = 0   
POL(E3(x₁, x₂, x₃, x₄)) = 0   
POL(EQUAL0(x₁, x₂)) = 0   
POL(False) = [2]   
POL(GCD(x₁, x₂)) = 0   
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₃   
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = x₅   
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃   
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃   
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(M1(x₁, x₂, x₃, x₄)) = 0   
POL(M2(x₁, x₂, x₃, x₄)) = 0   
POL(M4(x₁, x₂, x₃, x₄)) = 0   
POL(MONUS(x₁, x₂)) = 0   
POL(S(x₁)) = 0   
POL(True) = 0   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c25(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c28(x₁)) = x₁   
POL(c29(x₁)) = x₁   
POL(c32(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c36(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c42(x₁, x₂)) = x₁ + x₂   
POL(c43(x₁)) = x₁   
POL(c45(x₁, x₂)) = x₁ + x₂   
POL(c46(x₁, x₂)) = x₁ + x₂   
POL(c47(x₁, x₂)) = x₁ + x₂   
POL(c48(x₁)) = x₁   
POL(c49(x₁)) = x₁   
POL(c51(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(e1(x₁, x₂, x₃, x₄)) = [2] + [3]x₁ + x₂ + [2]x₃ + [3]x₄   
POL(e2(x₁, x₂, x₃, x₄)) = [2] + [4]x₁ + [4]x₂ + [5]x₃   
POL(e3(x₁, x₂, x₃, x₄)) = [2] + [3]x₁ + [4]x₂ + [2]x₄   
POL(e4(x₁, x₂, x₃, x₄)) = [2] + [4]x₁ + [4]x₂ + [4]x₃   
POL(equal0(x₁, x₂)) = [3]x₁   
POL(m1(x₁, x₂, x₃, x₄)) = 0   
POL(m2(x₁, x₂, x₃, x₄)) = 0   
POL(m4(x₁, x₂, x₃, x₄)) = 0   
POL(m5(x₁, x₂, x₃, x₄)) = [3]x₁ + x₃   
POL(monus(x₁, x₂)) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → e1(z0, z1, False, False)
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
monus(z0, z1) → m1(z0, z1, False, False)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))

Defined Rule Symbols:

equal0, e1, e2, <, e3, e4, monus, m1, m2, m4, m5

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))

We considered the (Usable) Rules:

m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
monus(z0, z1) → m1(z0, z1, False, False)

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(<(x₁, x₂)) = 0   
POL(<'(x₁, x₂)) = 0   
POL(E1(x₁, x₂, x₃, x₄)) = [3]x₄   
POL(E2(x₁, x₂, x₃, x₄)) = 0   
POL(E3(x₁, x₂, x₃, x₄)) = 0   
POL(EQUAL0(x₁, x₂)) = 0   
POL(False) = 0   
POL(GCD(x₁, x₂)) = 0   
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃ + [4]x₄ + [2]x₅ + [3]x₆   
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₄ + [2]x₆   
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₄   
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄   
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄ + x₅   
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₄ + [5]x₆   
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₄ + [4]x₅ + [2]x₆   
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃ + [4]x₄ + [2]x₅   
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃ + [3]x₄ + [2]x₅   
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₃ + [3]x₄   
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₃ + [4]x₆   
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₆   
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₆   
POL(M1(x₁, x₂, x₃, x₄)) = [4]x₃   
POL(M2(x₁, x₂, x₃, x₄)) = [3]x₃   
POL(M4(x₁, x₂, x₃, x₄)) = [3]x₃ + [2]x₄   
POL(MONUS(x₁, x₂)) = 0   
POL(S(x₁)) = 0   
POL(True) = [4]   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c25(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c28(x₁)) = x₁   
POL(c29(x₁)) = x₁   
POL(c32(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c36(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c42(x₁, x₂)) = x₁ + x₂   
POL(c43(x₁)) = x₁   
POL(c45(x₁, x₂)) = x₁ + x₂   
POL(c46(x₁, x₂)) = x₁ + x₂   
POL(c47(x₁, x₂)) = x₁ + x₂   
POL(c48(x₁)) = x₁   
POL(c49(x₁)) = x₁   
POL(c51(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(e1(x₁, x₂, x₃, x₄)) = [2] + [2]x₁ + [3]x₂ + [3]x₄   
POL(e2(x₁, x₂, x₃, x₄)) = [2] + [4]x₁ + [4]x₂ + [2]x₃   
POL(e3(x₁, x₂, x₃, x₄)) = [2] + x₁ + [4]x₂   
POL(e4(x₁, x₂, x₃, x₄)) = [1] + [2]x₁ + x₂ + [5]x₃   
POL(equal0(x₁, x₂)) = [4]x₁ + [2]x₂   
POL(m1(x₁, x₂, x₃, x₄)) = [3]x₃ + [4]x₄   
POL(m2(x₁, x₂, x₃, x₄)) = 0   
POL(m4(x₁, x₂, x₃, x₄)) = [3]x₄   
POL(m5(x₁, x₂, x₃, x₄)) = [3]x₁ + [2]x₂ + [4]x₃   
POL(monus(x₁, x₂)) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → e1(z0, z1, False, False)
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
monus(z0, z1) → m1(z0, z1, False, False)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))

Defined Rule Symbols:

equal0, e1, e2, <, e3, e4, monus, m1, m2, m4, m5

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))

We considered the (Usable) Rules:

m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
monus(z0, z1) → m1(z0, z1, False, False)

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(<(x₁, x₂)) = [4]x₁   
POL(<'(x₁, x₂)) = 0   
POL(E1(x₁, x₂, x₃, x₄)) = 0   
POL(E2(x₁, x₂, x₃, x₄)) = 0   
POL(E3(x₁, x₂, x₃, x₄)) = 0   
POL(EQUAL0(x₁, x₂)) = 0   
POL(False) = [2]   
POL(GCD(x₁, x₂)) = [1]   
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₅   
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = x₅   
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃   
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃   
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(M1(x₁, x₂, x₃, x₄)) = 0   
POL(M2(x₁, x₂, x₃, x₄)) = 0   
POL(M4(x₁, x₂, x₃, x₄)) = 0   
POL(MONUS(x₁, x₂)) = 0   
POL(S(x₁)) = 0   
POL(True) = [1]   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c25(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c28(x₁)) = x₁   
POL(c29(x₁)) = x₁   
POL(c32(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c36(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c42(x₁, x₂)) = x₁ + x₂   
POL(c43(x₁)) = x₁   
POL(c45(x₁, x₂)) = x₁ + x₂   
POL(c46(x₁, x₂)) = x₁ + x₂   
POL(c47(x₁, x₂)) = x₁ + x₂   
POL(c48(x₁)) = x₁   
POL(c49(x₁)) = x₁   
POL(c51(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(e1(x₁, x₂, x₃, x₄)) = [2] + [4]x₁ + [5]x₂ + [3]x₃ + [2]x₄   
POL(e2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [2]x₃ + [2]x₄   
POL(e3(x₁, x₂, x₃, x₄)) = [2] + [3]x₁ + [3]x₂ + [5]x₃ + [3]x₄   
POL(e4(x₁, x₂, x₃, x₄)) = [3] + [2]x₁ + [4]x₂ + x₃   
POL(equal0(x₁, x₂)) = [5]x₂   
POL(m1(x₁, x₂, x₃, x₄)) = 0   
POL(m2(x₁, x₂, x₃, x₄)) = 0   
POL(m4(x₁, x₂, x₃, x₄)) = 0   
POL(m5(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₂ + x₃   
POL(monus(x₁, x₂)) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → e1(z0, z1, False, False)
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
monus(z0, z1) → m1(z0, z1, False, False)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))

Defined Rule Symbols:

equal0, e1, e2, <, e3, e4, monus, m1, m2, m4, m5

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

(19) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → e1(z0, z1, False, False)
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
monus(z0, z1) → m1(z0, z1, False, False)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))

Defined Rule Symbols:

equal0, e1, e2, <, e3, e4, monus, m1, m2, m4, m5

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))

We considered the (Usable) Rules:

m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
monus(z0, z1) → m1(z0, z1, False, False)

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(<(x₁, x₂)) = 0   
POL(<'(x₁, x₂)) = 0   
POL(E1(x₁, x₂, x₃, x₄)) = [4]x₃ + [3]x₄   
POL(E2(x₁, x₂, x₃, x₄)) = [3]x₃   
POL(E3(x₁, x₂, x₃, x₄)) = [3]x₃   
POL(EQUAL0(x₁, x₂)) = 0   
POL(False) = 0   
POL(GCD(x₁, x₂)) = [2]x₁ + [4]x₂   
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₁ + [4]x₂ + [3]x₃ + [5]x₄ + [5]x₅ + [3]x₆   
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + [2]x₃ + x₅ + x₆   
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + [2]x₃ + x₅   
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + [2]x₃   
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₂ + [2]x₅   
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + x₅ + x₆   
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₂ + [4]x₅   
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₁ + [4]x₂ + [3]x₃ + [5]x₄ + [5]x₅   
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₁ + [4]x₂ + [3]x₃ + [5]x₄ + [4]x₅ + [5]x₆   
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₁ + [4]x₂ + [5]x₃ + [4]x₅ + [2]x₆   
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₁ + [4]x₂ + [4]x₃ + [4]x₅ + [3]x₆   
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₁ + [4]x₂ + [2]x₃ + [4]x₅ + [4]x₆   
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + [4]x₂ + [2]x₃ + x₅ + [4]x₆   
POL(M1(x₁, x₂, x₃, x₄)) = x₁ + [2]x₃   
POL(M2(x₁, x₂, x₃, x₄)) = x₁ + [2]x₃   
POL(M4(x₁, x₂, x₃, x₄)) = x₁ + x₃   
POL(MONUS(x₁, x₂)) = x₁   
POL(S(x₁)) = [4] + x₁   
POL(True) = [4]   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c25(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c28(x₁)) = x₁   
POL(c29(x₁)) = x₁   
POL(c32(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c36(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c42(x₁, x₂)) = x₁ + x₂   
POL(c43(x₁)) = x₁   
POL(c45(x₁, x₂)) = x₁ + x₂   
POL(c46(x₁, x₂)) = x₁ + x₂   
POL(c47(x₁, x₂)) = x₁ + x₂   
POL(c48(x₁)) = x₁   
POL(c49(x₁)) = x₁   
POL(c51(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(e1(x₁, x₂, x₃, x₄)) = [3] + [2]x₁ + [2]x₂ + [3]x₄   
POL(e2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃   
POL(e3(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ + [3]x₄   
POL(e4(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [2]x₂ + [3]x₃   
POL(equal0(x₁, x₂)) = [4]x₁ + [4]x₂   
POL(m1(x₁, x₂, x₃, x₄)) = [4]x₃ + [5]x₄   
POL(m2(x₁, x₂, x₃, x₄)) = [3]x₃ + [3]x₄   
POL(m4(x₁, x₂, x₃, x₄)) = [2]x₃ + [5]x₄   
POL(m5(x₁, x₂, x₃, x₄)) = [2]x₃   
POL(monus(x₁, x₂)) = 0   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → e1(z0, z1, False, False)
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))
e2(z0, z1, z2, False) → False
e2(z0, z1, z2, True) → e3(z0, z1, z2, True)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0))
e4(z0, z1, z2, False) → False
e4(z0, z1, z2, True) → True
monus(z0, z1) → m1(z0, z1, False, False)
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False)
m2(z0, z1, z2, False) → m4(z0, z1, z2, False)
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3)
m5(z0, z1, z2, z3) → z2

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
MONUS(z0, z1) → c40(M1(z0, z1, False, False))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False))
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0))
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False))
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False))
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5))
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False))
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False))
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4))
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False))
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c1(<'(z0, z1))
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True))
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True))
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
E3(z0, z1, z2, z3) → c51(<'(z1, z0))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))

Defined Rule Symbols:

equal0, e1, e2, <, e3, e4, monus, m1, m2, m4, m5

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

(23) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

MONUS(z0, z1) → c40(M1(z0, z1, False, False))
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False))
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False))
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))

Now S is empty

(24) BOUNDS(1, 1)