Runtime Complexity (innermost) proof of /tmp/tmpycDGbi/gexgcd.xml

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

0 CpxRelTRS

↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)

↳2 CpxTRS

↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CdtProblem

↳9 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳10 CdtProblem

↳11 CdtUsableRulesProof (⇔, 24 ms)

↳12 CdtProblem

↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 345 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 174 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 121 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 121 ms)

↳20 CdtProblem

↳21 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 1 ms)

↳22 CdtProblem

↳23 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 1735 ms)

↳24 CdtProblem

↳25 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳26 BOUNDS(1, 1)

(0) Obligation:

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

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) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

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

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))
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False

Tuples:

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

S tuples:

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

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

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

Removed 27 trailing nodes:

M5(z0, z1, z2, z3) → c38
L2(z0, z1, z2, z3, z4, True) → c24
E4(z0, z1, z2, True) → c15
HELP1(S(0)) → c11
HELP1(0) → c13
HELP1(S(S(z0))) → c12
M2(0, z0, z1, True) → c2
M3(S(S(z0)), z1, z2, z3) → c5
BOOL2NAT(True) → c28
M3(S(0), z0, z1, z2) → c4
E4(z0, z1, z2, False) → c14
M3(0, z0, z1, z2) → c6
E5(z0, z1, z2, z3) → c36
M2(S(0), z0, z1, True) → c
E7(z0, z1, z2, z3) → c34
L9(z0, z1, z2, z3, z4, z5) → c30
E8(z0, z1, z2, z3) → c47
<'(0, S(z0)) → c51
<'(z0, 0) → c52
L16(z0, z1, z2, z3, z4, z5) → c41
E2(z0, z1, z2, False) → c16
L5(z0, z1, z2, z3, z4, True) → c9
E6(z0, z1, z2, z3) → c35
BOOL2NAT(False) → c27
L8(z0, z1, z2, True, z3, z4) → c7
L6(z0, z1, z2, z3, z4, z5) → c31
M2(S(S(z0)), z1, z2, True) → c1

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False

Tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L15(z0, z1, z2, z3, False, z4) → c18(L16(z0, z1, gcd(z1, 0), z3, False, z4), GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(L16(z0, z1, gcd(z1, S(0)), z3, True, z4), GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(L16(z0, z1, gcd(0, z1), z3, False, z4), GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(L16(z0, z1, gcd(S(0), z1), z3, True, z4), GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(M5(S(z0), S(z1), monus(z0, z1), z3), MONUS(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
E3(z0, z1, z2, z3) → c48(E4(z0, z1, z2, <(z1, z0)), <'(z1, z0))
E1(z0, z1, z2, z3) → c49(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))
<'(S(z0), S(z1)) → c50(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L15(z0, z1, z2, z3, False, z4) → c18(L16(z0, z1, gcd(z1, 0), z3, False, z4), GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(L16(z0, z1, gcd(z1, S(0)), z3, True, z4), GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(L16(z0, z1, gcd(0, z1), z3, False, z4), GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(L16(z0, z1, gcd(S(0), z1), z3, True, z4), GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(M5(S(z0), S(z1), monus(z0, z1), z3), MONUS(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
E3(z0, z1, z2, z3) → c48(E4(z0, z1, z2, <(z1, z0)), <'(z1, z0))
E1(z0, z1, z2, z3) → c49(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))
<'(S(z0), S(z1)) → c50(<'(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:

c3, c8, c10, c17, c18, c19, c20, c21, c22, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c48, c49, c50

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

Removed 6 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False

Tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
E1(z0, z1, z2, z3) → c49(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))

S tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
E1(z0, z1, z2, z3) → c49(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c49, c50, c18, c19, c20, c21, c22, c48

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

Split RHS of tuples not part of any SCC

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False

Tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c50, c18, c19, c20, c21, c22, c48, c

(11) 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

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

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c50, c18, c19, c20, c21, c22, c48, c

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

L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, True, z4) → c21(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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(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) = 0
POL(GCD(x₁, x₂)) = 0
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₄ + [2]x₅
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + [2]x₄
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄
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₆)) = x₄ + x₆
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄ + [2]x₅ + x₆
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₄ + x₅
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₆
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃ + x₆
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃
POL(M1(x₁, x₂, x₃, x₄)) = [2]x₃
POL(M2(x₁, x₂, x₃, x₄)) = x₃
POL(M4(x₁, x₂, x₃, x₄)) = 0
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = 0
POL(True) = [1]
POL(c(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c21(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c29(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁)) = x₁
POL(c37(x₁)) = x₁
POL(c39(x₁, x₂)) = x₁ + x₂
POL(c40(x₁)) = x₁
POL(c42(x₁, x₂)) = x₁ + x₂
POL(c43(x₁, x₂)) = x₁ + x₂
POL(c44(x₁, x₂)) = x₁ + x₂
POL(c45(x₁)) = x₁
POL(c46(x₁)) = x₁
POL(c48(x₁)) = x₁
POL(c50(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(e1(x₁, x₂, x₃, x₄)) = 0
POL(e2(x₁, x₂, x₃, x₄)) = 0
POL(e3(x₁, x₂, x₃, x₄)) = 0
POL(e4(x₁, x₂, x₃, x₄)) = 0
POL(equal0(x₁, x₂)) = 0
POL(m1(x₁, x₂, x₃, x₄)) = [3]x₃
POL(m2(x₁, x₂, x₃, x₄)) = [3]x₃
POL(m4(x₁, x₂, x₃, x₄)) = x₃ + [2]x₄
POL(m5(x₁, x₂, x₃, x₄)) = 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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, True, z4) → c21(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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c50, c18, c19, c20, c21, c22, c48, c

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

M4(S(z0), S(z1), z2, z3) → c22(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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(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₄)) = x₃
POL(E2(x₁, x₂, x₃, x₄)) = x₃
POL(E3(x₁, x₂, x₃, x₄)) = 0
POL(EQUAL0(x₁, x₂)) = 0
POL(False) = 0
POL(GCD(x₁, x₂)) = x₁ + x₂
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₄ + x₅
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄
POL(L12(x₁, 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₆)) = x₁ + x₂ + x₃ + x₄ + x₆
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = x₂ + x₄ + x₅ + x₆
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₄ + x₅
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₄ + x₅
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄ + x₅
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄ + x₅
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄ + x₆
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃
POL(M1(x₁, x₂, x₃, x₄)) = x₁ + x₃
POL(M2(x₁, x₂, x₃, x₄)) = x₁
POL(M4(x₁, x₂, x₃, x₄)) = x₁
POL(MONUS(x₁, x₂)) = x₁
POL(S(x₁)) = [1] + x₁
POL(True) = [1]
POL(c(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c21(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c29(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁)) = x₁
POL(c37(x₁)) = x₁
POL(c39(x₁, x₂)) = x₁ + x₂
POL(c40(x₁)) = x₁
POL(c42(x₁, x₂)) = x₁ + x₂
POL(c43(x₁, x₂)) = x₁ + x₂
POL(c44(x₁, x₂)) = x₁ + x₂
POL(c45(x₁)) = x₁
POL(c46(x₁)) = x₁
POL(c48(x₁)) = x₁
POL(c50(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(e1(x₁, x₂, x₃, x₄)) = x₂
POL(e2(x₁, x₂, x₃, x₄)) = x₂
POL(e3(x₁, x₂, x₃, x₄)) = x₂
POL(e4(x₁, x₂, x₃, x₄)) = x₂ + x₄
POL(equal0(x₁, x₂)) = [1] + 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₄)) = 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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c50, c18, c19, c20, c21, c22, c48, c

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

L13(z0, z1, z2, z3, False, z4) → c20(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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(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) = [1]
POL(GCD(x₁, x₂)) = 0
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆
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₆)) = x₃
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃
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(c10(x₁)) = x₁
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c21(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c29(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁)) = x₁
POL(c37(x₁)) = x₁
POL(c39(x₁, x₂)) = x₁ + x₂
POL(c40(x₁)) = x₁
POL(c42(x₁, x₂)) = x₁ + x₂
POL(c43(x₁, x₂)) = x₁ + x₂
POL(c44(x₁, x₂)) = x₁ + x₂
POL(c45(x₁)) = x₁
POL(c46(x₁)) = x₁
POL(c48(x₁)) = x₁
POL(c50(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(e1(x₁, x₂, x₃, x₄)) = 0
POL(e2(x₁, x₂, x₃, x₄)) = 0
POL(e3(x₁, x₂, x₃, x₄)) = 0
POL(e4(x₁, x₂, x₃, x₄)) = 0
POL(equal0(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(m5(x₁, x₂, x₃, 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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
L13(z0, z1, z2, z3, False, z4) → c20(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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c50, c18, c19, c20, c21, c22, c48, c

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

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

L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
L15(z0, z1, z2, z3, False, z4) → c18(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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(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₂)) = [2]
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃
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₆)) = x₃
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₅
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = [2] + [2]x₃
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = [2] + [2]x₃
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₃
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) = [2]
POL(c(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c21(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c29(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁)) = x₁
POL(c37(x₁)) = x₁
POL(c39(x₁, x₂)) = x₁ + x₂
POL(c40(x₁)) = x₁
POL(c42(x₁, x₂)) = x₁ + x₂
POL(c43(x₁, x₂)) = x₁ + x₂
POL(c44(x₁, x₂)) = x₁ + x₂
POL(c45(x₁)) = x₁
POL(c46(x₁)) = x₁
POL(c48(x₁)) = x₁
POL(c50(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(e1(x₁, x₂, x₃, x₄)) = 0
POL(e2(x₁, x₂, x₃, x₄)) = 0
POL(e3(x₁, x₂, x₃, x₄)) = 0
POL(e4(x₁, x₂, x₃, x₄)) = 0
POL(equal0(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(m5(x₁, x₂, x₃, x₄)) = [2]x₃
POL(monus(x₁, x₂)) = 0

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

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
L15(z0, z1, z2, z3, False, z4) → c18(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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c50, c18, c19, c20, c21, c22, c48, c

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

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

L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))

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

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

S tuples:

<'(S(z0), S(z1)) → c50(<'(z0, z1))

K tuples:

L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))

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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c50, c18, c19, c20, c21, c22, c48, c

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

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

<'(S(z0), S(z1)) → c50(<'(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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

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

POL(0) = 0
POL(<(x₁, x₂)) = [2]x₁·x₂
POL(<'(x₁, x₂)) = x₁·x₂
POL(E1(x₁, x₂, x₃, x₄)) = x₄ + [2]x₄² + x₃·x₄ + [2]x₁·x₄ + x₁·x₂ + [2]x₁·x₃ + [2]x₃² + [2]x₂·x₃
POL(E2(x₁, x₂, x₃, x₄)) = x₁·x₂ + [2]x₁·x₃ + [2]x₃² + [2]x₂·x₃
POL(E3(x₁, x₂, x₃, x₄)) = x₁·x₂ + x₁·x₃ + x₃²
POL(EQUAL0(x₁, x₂)) = x₁·x₂
POL(False) = 0
POL(GCD(x₁, x₂)) = [2]x₁·x₂
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + [2]x₄ + [2]x₅ + x₆ + [2]x₆² + x₅·x₆ + x₄·x₆ + [2]x₂·x₆ + [2]x₁·x₆ + [2]x₁·x₂ + [2]x₁·x₃ + [2]x₁·x₄ + [2]x₁·x₅ + [2]x₅² + x₃·x₅ + [2]x₂·x₅ + [2]x₂·x₃ + [2]x₂·x₄ + [2]x₃·x₄ + [2]x₃²
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₆² + x₅·x₆ + x₄·x₆ + x₃·x₆ + x₁·x₆ + x₁·x₂ + [2]x₁·x₄ + [2]x₄·x₅ + [2]x₂·x₄ + [2]x₄² + [2]x₃·x₄ + [2]x₃²
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₁·x₄ + [2]x₄·x₅ + [2]x₂·x₄ + [2]x₄² + [2]x₃²
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₁·x₄ + x₄·x₅ + [2]x₂·x₄ + [2]x₄² + [2]x₃²
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁·x₄ + [2]x₂·x₅ + x₂·x₄ + x₄²
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₆ + [2]x₆² + x₅·x₆ + [2]x₄·x₆ + [2]x₃·x₆ + [2]x₂·x₆ + x₁·x₆ + [2]x₁·x₄ + [2]x₄·x₅ + [2]x₂·x₄ + [2]x₄² + [2]x₃²
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ + x₆² + [2]x₅·x₆ + x₄·x₆ + x₃·x₆ + x₁·x₆ + [2]x₁·x₄ + [2]x₂·x₅ + x₄² + x₃²
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + [2]x₄ + x₅ + [2]x₆ + x₆² + x₅·x₆ + x₄·x₆ + x₃·x₆ + [2]x₂·x₆ + [2]x₁·x₂ + [2]x₁·x₃ + [2]x₁·x₄ + [2]x₁·x₅ + [2]x₅² + x₃·x₅ + x₂·x₅ + [2]x₂·x₃ + [2]x₂·x₄ + [2]x₃·x₄ + x₃²
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₄ + [2]x₆ + [2]x₆² + [2]x₅·x₆ + x₄·x₆ + [2]x₃·x₆ + [2]x₁·x₆ + [2]x₁·x₂ + x₁·x₃ + [2]x₁·x₄ + [2]x₁·x₅ + [2]x₅² + x₃·x₅ + [2]x₂·x₄ + x₃²
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + [2]x₄ + [2]x₆² + [2]x₅·x₆ + [2]x₃·x₆ + [2]x₁·x₆ + [2]x₁·x₂ + [2]x₁·x₃ + x₁·x₄ + [2]x₁·x₅ + [2]x₃·x₅ + x₂·x₃ + [2]x₂·x₄ + x₃·x₄ + [2]x₃²
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₆ + [2]x₅·x₆ + [2]x₄·x₆ + [2]x₃·x₆ + x₁·x₆ + [2]x₁·x₂ + x₁·x₄ + [2]x₁·x₅ + x₂·x₃ + [2]x₂·x₄ + [2]x₃²
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₆ + [2]x₆² + x₅·x₆ + x₄·x₆ + x₃·x₆ + [2]x₂·x₆ + [2]x₁·x₆ + [2]x₁·x₂ + x₁·x₄ + [2]x₁·x₅ + x₂·x₃ + [2]x₃²
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₆² + x₅·x₆ + x₃·x₆ + x₂·x₆ + x₁·x₆ + x₁·x₂ + [2]x₁·x₅ + x₂·x₃ + [2]x₃²
POL(M1(x₁, x₂, x₃, x₄)) = [2]x₃ + [2]x₄ + [2]x₄² + [2]x₁·x₄ + x₁·x₃ + [2]x₃² + [2]x₂·x₃
POL(M2(x₁, x₂, x₃, x₄)) = x₃ + [2]x₄ + [2]x₃·x₄ + x₁·x₄ + [2]x₃² + x₂·x₃
POL(M4(x₁, x₂, x₃, x₄)) = x₃ + x₄ + x₄² + x₃·x₄ + [2]x₂·x₄ + [2]x₁·x₄ + x₂·x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = [2] + x₁
POL(True) = [2]
POL(c(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁)) = x₁
POL(c21(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c29(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁)) = x₁
POL(c37(x₁)) = x₁
POL(c39(x₁, x₂)) = x₁ + x₂
POL(c40(x₁)) = x₁
POL(c42(x₁, x₂)) = x₁ + x₂
POL(c43(x₁, x₂)) = x₁ + x₂
POL(c44(x₁, x₂)) = x₁ + x₂
POL(c45(x₁)) = x₁
POL(c46(x₁)) = x₁
POL(c48(x₁)) = x₁
POL(c50(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(e1(x₁, x₂, x₃, x₄)) = [1] + x₃ + x₄ + x₄² + x₃·x₄ + x₂·x₄ + x₁·x₄ + x₁² + [2]x₁·x₂ + x₁·x₃ + x₃² + [2]x₂·x₃ + x₂²
POL(e2(x₁, x₂, x₃, x₄)) = [1] + [2]x₁ + [2]x₂ + x₃ + [2]x₄ + x₄² + [2]x₃·x₄ + [2]x₁·x₄ + [2]x₁² + [2]x₁·x₃ + x₂·x₃ + [2]x₂²
POL(e3(x₁, x₂, x₃, x₄)) = [1] + [2]x₁ + x₂ + [2]x₄ + x₄² + x₃·x₄ + x₂·x₄ + x₁·x₄ + x₁² + [2]x₃² + x₂·x₃
POL(e4(x₁, x₂, x₃, x₄)) = [1] + x₁ + [2]x₃ + [2]x₃·x₄ + [2]x₂·x₄ + [2]x₁·x₄ + [2]x₁² + [2]x₁·x₂ + x₃² + [2]x₂·x₃ + [2]x₂²
POL(equal0(x₁, x₂)) = 0
POL(m1(x₁, x₂, x₃, x₄)) = [2]x₃ + x₄² + [2]x₃·x₄ + x₁·x₃ + x₃² + x₂·x₃
POL(m2(x₁, x₂, x₃, x₄)) = [2]x₃ + [2]x₄ + x₄² + [2]x₃·x₄ + x₁·x₄ + x₁·x₃ + x₃² + x₂·x₃
POL(m4(x₁, x₂, x₃, x₄)) = [2]x₃ + x₁·x₃ + x₃² + x₂·x₃
POL(m5(x₁, x₂, x₃, x₄)) = x₃ + [2]x₃·x₄
POL(monus(x₁, x₂)) = 0

(24) 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:

M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
<'(S(z0), S(z1)) → c50(<'(z0, z1))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))

S tuples:none
K tuples:

L15(z0, z1, z2, z3, True, z4) → c19(GCD(z1, S(0)))
L13(z0, z1, z2, z3, True, z4) → c21(GCD(S(0), z1))
M4(S(z0), S(z1), z2, z3) → c22(MONUS(z0, z1))
L13(z0, z1, z2, z3, False, z4) → c20(GCD(0, z1))
L5(z0, z1, z2, z3, z4, False) → c10(L7(z0, z1, z2, z3, z4, False))
L15(z0, z1, z2, z3, False, z4) → c18(GCD(z1, 0))
L7(z0, z1, z2, z3, z4, z5) → c39(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1))
GCD(z0, z1) → c45(L1(z0, z1, 0, False, False, False))
EQUAL0(z0, z1) → c46(E1(z0, z1, False, False))
E1(z0, z1, z2, z3) → c(E2(z0, z1, z2, <(z0, z1)))
E1(z0, z1, z2, z3) → c(<'(z0, z1))
L8(z0, z1, z2, False, z3, z4) → c8(L10(z0, z1, z2, False, z3, z4))
L1(z0, z1, z2, z3, z4, z5) → c33(L2(z0, z1, z2, z3, z4, False))
E2(z0, z1, z2, True) → c17(E3(z0, z1, z2, True))
L10(z0, z1, z2, z3, z4, z5) → c44(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1))
L2(z0, z1, z2, z3, z4, False) → c23(L3(z0, z1, z2, z3, z4, False))
E3(z0, z1, z2, z3) → c48(<'(z1, z0))
L11(z0, z1, z2, z3, z4, False) → c25(L14(z0, z1, z2, z3, z4, False))
L11(z0, z1, z2, z3, z4, True) → c26(L12(z0, z1, z2, z3, z4, True))
L3(z0, z1, z2, z3, z4, z5) → c40(L4(z0, z1, 0, z3, z4, z5))
L14(z0, z1, z2, z3, z4, z5) → c42(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L12(z0, z1, z2, z3, z4, z5) → c43(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))
L4(z0, z1, z2, z3, z4, z5) → c32(L5(z0, z1, z2, z3, z4, False))
MONUS(z0, z1) → c37(M1(z0, z1, False, False))
M1(z0, z1, z2, z3) → c29(M2(z0, z1, z2, False))
M2(z0, z1, z2, False) → c3(M4(z0, z1, z2, False))
<'(S(z0), S(z1)) → c50(<'(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:

c3, c8, c10, c17, c23, c25, c26, c29, c32, c33, c37, c39, c40, c42, c43, c44, c45, c46, c50, c18, c19, c20, c21, c22, c48, c

(25) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(0) Obligation:

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

(11) CdtUsableRulesProof (EQUIVALENT transformation)

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(24) Obligation:

(25) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

(26) BOUNDS(1, 1)