Runtime Complexity (innermost) proof of /tmp/tmpie5yiy/gexgcd2.xml

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

0 CpxRelTRS

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

↳2 CdtProblem

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

↳4 CdtProblem

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

↳6 CdtProblem

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

↳8 CdtProblem

↳9 CdtUsableRulesProof (⇔, 0 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 306 ms)

↳12 CdtProblem

↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 6 ms)

↳14 CdtProblem

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

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 198 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 320 ms)

↳20 CdtProblem

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

↳22 BOUNDS(1, 1)

(0) Obligation:

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

monus(S(x'), S(x)) → monus(x', x)
gcd(x, y) → gcd[Ite](equal0(x, y), x, y)
equal0(a, b) → equal0[Ite](<(a, b), a, b)

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

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
gcd[Ite](False, x, y) → gcd[False][Ite](<(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(y, monus(y, x))
gcd[False][Ite](True, x, y) → gcd(monus(x, y), y)
equal0[Ite](False, a, b) → False
equal0[Ite](True, a, b) → equal0[True][Ite](<(b, a), a, b)
equal0[True][Ite](False, a, b) → False
equal0[True][Ite](True, a, b) → True

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
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
<'(0, S(z0)) → c1
<'(z0, 0) → c2
GCD[ITE](False, z0, z1) → c3(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[ITE](True, z0, z1) → c4
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](False, z0, z1) → c7
EQUAL0[ITE](True, z0, z1) → c8(EQUAL0[TRUE][ITE](<(z1, z0), z0, z1), <'(z1, z0))
EQUAL0[TRUE][ITE](False, z0, z1) → c9
EQUAL0[TRUE][ITE](True, z0, z1) → c10
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c13(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))

S tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c13(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))

K tuples:none
Defined Rule Symbols:

monus, gcd, equal0, <, gcd[Ite], gcd[False][Ite], equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0[TRUE][ITE], MONUS, GCD, EQUAL0

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13

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

Removed 6 trailing nodes:

<'(z0, 0) → c2
<'(0, S(z0)) → c1
EQUAL0[TRUE][ITE](True, z0, z1) → c10
GCD[ITE](True, z0, z1) → c4
EQUAL0[TRUE][ITE](False, z0, z1) → c9
EQUAL0[ITE](False, z0, z1) → c7

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[ITE](False, z0, z1) → c3(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(EQUAL0[TRUE][ITE](<(z1, z0), z0, z1), <'(z1, z0))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c13(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))

S tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c13(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))

K tuples:none
Defined Rule Symbols:

monus, gcd, equal0, <, gcd[Ite], gcd[False][Ite], equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], MONUS, GCD, EQUAL0

Compound Symbols:

c, c3, c5, c6, c8, c11, c12, c13

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

Removed 1 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[ITE](False, z0, z1) → c3(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c13(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))

S tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c13(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))

K tuples:none
Defined Rule Symbols:

monus, gcd, equal0, <, gcd[Ite], gcd[False][Ite], equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[ITE], GCD[FALSE][ITE], MONUS, GCD, EQUAL0, EQUAL0[ITE]

Compound Symbols:

c, c3, c5, c6, c11, c12, c13, c8

(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
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[ITE](False, z0, z1) → c3(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

S tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

K tuples:none
Defined Rule Symbols:

monus, gcd, equal0, <, gcd[Ite], gcd[False][Ite], equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[ITE], GCD[FALSE][ITE], MONUS, GCD, EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c3, c5, c6, c11, c12, c8, c1

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[ITE](False, z0, z1) → c3(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

S tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

K tuples:none
Defined Rule Symbols:

<, monus, equal0, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[ITE], GCD[FALSE][ITE], MONUS, GCD, EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c3, c5, c6, c11, c12, c8, 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.

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))

We considered the (Usable) Rules:

monus(S(z0), S(z1)) → monus(z0, z1)

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[ITE](False, z0, z1) → c3(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → 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(EQUAL0(x₁, x₂)) = 0
POL(EQUAL0[ITE](x₁, x₂, x₃)) = 0
POL(False) = 0
POL(GCD(x₁, x₂)) = x₁ + [2]x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = x₂ + [2]x₃
POL(GCD[ITE](x₁, x₂, x₃)) = x₂ + [2]x₃
POL(MONUS(x₁, x₂)) = x₁
POL(S(x₁)) = [1] + x₁
POL(True) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁)) = x₁
POL(equal0(x₁, x₂)) = x₁
POL(equal0[Ite](x₁, x₂, x₃)) = [3]x₂ + [2]x₃
POL(equal0[True][Ite](x₁, x₂, x₃)) = [3] + [2]x₂ + [5]x₃
POL(monus(x₁, x₂)) = 0

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[ITE](False, z0, z1) → c3(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

S tuples:

GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))

Defined Rule Symbols:

<, monus, equal0, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[ITE], GCD[FALSE][ITE], MONUS, GCD, EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c3, c5, c6, c11, c12, c8, c1

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace GCD[ITE](False, z0, z1) → c3(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1)) by

GCD[ITE](False, S(z0), S(z1)) → c3(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c3(GCD[FALSE][ITE](True, 0, S(z0)), <'(0, S(z0)))
GCD[ITE](False, z0, 0) → c3(GCD[FALSE][ITE](False, z0, 0), <'(z0, 0))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c3(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c3(GCD[FALSE][ITE](True, 0, S(z0)), <'(0, S(z0)))
GCD[ITE](False, z0, 0) → c3(GCD[FALSE][ITE](False, z0, 0), <'(z0, 0))

S tuples:

GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))

Defined Rule Symbols:

<, monus, equal0, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[FALSE][ITE], MONUS, GCD, EQUAL0[ITE], EQUAL0, GCD[ITE]

Compound Symbols:

c, c5, c6, c11, c12, c8, c1, c3

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

Removed 2 trailing tuple parts

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c3(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c3(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c3(GCD[FALSE][ITE](False, z0, 0))

S tuples:

GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))

Defined Rule Symbols:

<, monus, equal0, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[FALSE][ITE], MONUS, GCD, EQUAL0[ITE], EQUAL0, GCD[ITE]

Compound Symbols:

c, c5, c6, c11, c12, c8, c1, c3, c3

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

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

EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

We considered the (Usable) Rules:

monus(S(z0), S(z1)) → monus(z0, z1)
<(z0, 0) → False
<(0, S(z0)) → True
<(S(z0), S(z1)) → <(z0, z1)

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c3(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c3(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c3(GCD[FALSE][ITE](False, z0, 0))

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

POL(0) = [1]
POL(<(x₁, x₂)) = [1]
POL(<'(x₁, x₂)) = 0
POL(EQUAL0(x₁, x₂)) = [1]
POL(EQUAL0[ITE](x₁, x₂, x₃)) = 0
POL(False) = 0
POL(GCD(x₁, x₂)) = [2] + x₂ + [2]x₁·x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = [2] + x₁·x₃
POL(GCD[ITE](x₁, x₂, x₃)) = [1] + x₃ + x₂·x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = [1]
POL(True) = [1]
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁)) = x₁
POL(equal0(x₁, x₂)) = 0
POL(equal0[Ite](x₁, x₂, x₃)) = 0
POL(equal0[True][Ite](x₁, x₂, x₃)) = 0
POL(monus(x₁, x₂)) = 0

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c3(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c3(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c3(GCD[FALSE][ITE](False, z0, 0))

S tuples:

GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))

Defined Rule Symbols:

<, monus, equal0, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[FALSE][ITE], MONUS, GCD, EQUAL0[ITE], EQUAL0, GCD[ITE]

Compound Symbols:

c, c5, c6, c11, c12, c8, c1, c3, c3

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

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

GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))

We considered the (Usable) Rules:

monus(S(z0), S(z1)) → monus(z0, z1)
<(z0, 0) → False
<(0, S(z0)) → True
<(S(z0), S(z1)) → <(z0, z1)

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c3(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c3(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c3(GCD[FALSE][ITE](False, z0, 0))

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

POL(0) = [1]
POL(<(x₁, x₂)) = [2] + [2]x₁
POL(<'(x₁, x₂)) = 0
POL(EQUAL0(x₁, x₂)) = 0
POL(EQUAL0[ITE](x₁, x₂, x₃)) = 0
POL(False) = [2]
POL(GCD(x₁, x₂)) = [2] + [3]x₂ + x₂² + [2]x₁·x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = [2] + x₃² + x₁·x₃
POL(GCD[ITE](x₁, x₂, x₃)) = [1] + [3]x₃ + x₃² + [2]x₂·x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = [2] + x₁
POL(True) = [3]
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁)) = x₁
POL(equal0(x₁, x₂)) = 0
POL(equal0[Ite](x₁, x₂, x₃)) = 0
POL(equal0[True][Ite](x₁, x₂, x₃)) = 0
POL(monus(x₁, x₂)) = 0

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c5(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c6(GCD(monus(z0, z1), z1), MONUS(z0, z1))
MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0[ITE](True, z0, z1) → c8(<'(z1, z0))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c3(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c3(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c3(GCD[FALSE][ITE](False, z0, 0))

S tuples:none
K tuples:

MONUS(S(z0), S(z1)) → c11(MONUS(z0, z1))
EQUAL0(z0, z1) → c1(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c1(<'(z0, z1))
GCD(z0, z1) → c12(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))

Defined Rule Symbols:

<, monus, equal0, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

<', GCD[FALSE][ITE], MONUS, GCD, EQUAL0[ITE], EQUAL0, GCD[ITE]

Compound Symbols:

c, c5, c6, c11, c12, c8, c1, c3, c3

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

The set S is empty

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) CdtUsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

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

(12) Obligation:

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) BOUNDS(1, 1)