24.70/6.90 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

24.70/6.90

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

0 CpxRelTRS

24.70/6.90

↳1 CpxRelTrsToCDT (UPPER BOUND (ID))

24.70/6.90

↳2 CdtProblem

24.70/6.90

↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

24.70/6.90

↳4 CdtProblem

24.70/6.90

↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))

24.70/6.90

↳6 CdtProblem

24.70/6.90

↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)

24.70/6.90

↳8 CdtProblem

24.70/6.90

↳9 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

24.70/6.90

↳10 CdtProblem

24.70/6.90

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

24.70/6.90

↳12 CdtProblem

24.70/6.90

↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

24.70/6.90

↳14 CdtProblem

24.70/6.90

↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

24.70/6.90

↳16 CdtProblem

24.70/6.90

↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

24.70/6.90

↳18 CdtProblem

24.70/6.90

↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

24.70/6.90

↳20 CdtProblem

24.70/6.90

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

24.70/6.90

↳22 BOUNDS(O(1), O(1))

24.70/6.90

24.70/6.90 24.70/6.90

24.70/6.90

(0) Obligation:

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

@(Cons(x, xs), ys) → Cons(x, @(xs, ys)) 24.70/6.90
@(Nil, ys) → ys 24.70/6.90
gt0(Cons(x, xs), Nil) → True 24.70/6.90
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs) 24.70/6.90
gcd(Nil, Nil) → Nil 24.70/6.90
gcd(Nil, Cons(x, xs)) → Nil 24.70/6.90
gcd(Cons(x, xs), Nil) → Nil 24.70/6.90
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite][False][Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs)) 24.70/6.90
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs)) 24.70/6.90
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys)) 24.70/6.90
eqList(Cons(x, xs), Nil) → False 24.70/6.90
eqList(Nil, Cons(y, ys)) → False 24.70/6.90
eqList(Nil, Nil) → True 24.70/6.90
lgth(Nil) → Nil 24.70/6.90
gt0(Nil, y) → False 24.70/6.90
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y) 24.70/6.90
goal(x, y) → gcd(x, y)

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

and(False, False) → False 24.70/6.90
and(True, False) → False 24.70/6.90
and(False, True) → False 24.70/6.90
and(True, True) → True 24.70/6.90
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs) 24.70/6.90
monus[Ite](True, Cons(x, xs), y) → xs 24.70/6.90
gcd[Ite][False][Ite](False, x, y) → gcd[Ite][False][Ite][False][Ite](gt0(x, y), x, y) 24.70/6.90
gcd[Ite][False][Ite](True, x, y) → x

Rewrite Strategy: INNERMOST

24.70/6.90

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.

24.70/6.90

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 24.70/6.90
and(True, False) → False 24.70/6.90
and(False, True) → False 24.70/6.90
and(True, True) → True 24.70/6.90
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 24.70/6.90
monus[Ite](True, Cons(z0, z1), z2) → z1 24.70/6.90
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 24.70/6.90
gcd[Ite][False][Ite](True, z0, z1) → z0 24.70/6.90
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 24.70/6.90
@(Nil, z0) → z0 24.70/6.90
gt0(Cons(z0, z1), Nil) → True 24.70/6.90
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 24.70/6.90
gt0(Nil, z0) → False 24.70/6.90
gcd(Nil, Nil) → Nil 24.70/6.90
gcd(Nil, Cons(z0, z1)) → Nil 24.70/6.90
gcd(Cons(z0, z1), Nil) → Nil 24.70/6.90
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 24.70/6.90
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 24.70/6.90
lgth(Nil) → Nil 24.70/6.90
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 24.70/6.90
eqList(Cons(z0, z1), Nil) → False 24.70/6.90
eqList(Nil, Cons(z0, z1)) → False 24.70/6.90
eqList(Nil, Nil) → True 24.70/6.90
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 24.70/6.90
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 24.70/6.90
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 24.70/6.90
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 24.70/6.90
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 24.70/6.90
GCD(Cons(z0, z1), Cons(z2, z3)) → c16(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) 24.70/6.90
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 24.70/6.90
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2), EQLIST(z1, z3)) 24.70/6.90
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 24.70/6.90
GOAL(z0, z1) → c24(GCD(z0, z1))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 24.70/6.90
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 24.70/6.90
GCD(Cons(z0, z1), Cons(z2, z3)) → c16(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) 24.70/6.90
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 24.70/6.90
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2), EQLIST(z1, z3)) 24.70/6.90
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 24.70/6.90
GOAL(z0, z1) → c24(GCD(z0, z1))

K tuples:none
Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, GCD, LGTH, EQLIST, MONUS, GOAL

Compound Symbols:

c4, c6, c8, c11, c16, c17, c19, c23, c24

24.70/6.90

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

Removed 1 trailing tuple parts

24.70/6.90

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 24.70/6.90
and(True, False) → False 24.70/6.90
and(False, True) → False 24.70/6.90
and(True, True) → True 24.70/6.90
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 24.70/6.90
monus[Ite](True, Cons(z0, z1), z2) → z1 24.70/6.90
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 24.70/6.90
gcd[Ite][False][Ite](True, z0, z1) → z0 24.70/6.90
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 24.70/6.90
@(Nil, z0) → z0 24.70/6.90
gt0(Cons(z0, z1), Nil) → True 24.70/6.90
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 24.70/6.90
gt0(Nil, z0) → False 24.70/6.90
gcd(Nil, Nil) → Nil 24.70/6.90
gcd(Nil, Cons(z0, z1)) → Nil 24.70/6.90
gcd(Cons(z0, z1), Nil) → Nil 24.70/6.90
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 24.70/6.90
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 24.70/6.90
lgth(Nil) → Nil 24.70/6.90
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 24.70/6.90
eqList(Cons(z0, z1), Nil) → False 25.05/6.92
eqList(Nil, Cons(z0, z1)) → False 25.05/6.92
eqList(Nil, Nil) → True 25.05/6.92
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.92
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.92
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.92
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.92
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.92
GCD(Cons(z0, z1), Cons(z2, z3)) → c16(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) 25.05/6.92
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.92
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.92
GOAL(z0, z1) → c24(GCD(z0, z1)) 25.05/6.92
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.92
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.92
GCD(Cons(z0, z1), Cons(z2, z3)) → c16(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) 25.05/6.92
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.92
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.92
GOAL(z0, z1) → c24(GCD(z0, z1)) 25.05/6.92
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))

K tuples:none
Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, GCD, LGTH, MONUS, GOAL, EQLIST

Compound Symbols:

c4, c6, c8, c11, c16, c17, c23, c24, c19

25.05/6.92

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

Split RHS of tuples not part of any SCC

25.05/6.92

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.05/6.92
and(True, False) → False 25.05/6.92
and(False, True) → False 25.05/6.92
and(True, True) → True 25.05/6.92
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.05/6.92
monus[Ite](True, Cons(z0, z1), z2) → z1 25.05/6.92
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.05/6.92
gcd[Ite][False][Ite](True, z0, z1) → z0 25.05/6.92
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.92
@(Nil, z0) → z0 25.05/6.92
gt0(Cons(z0, z1), Nil) → True 25.05/6.92
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.05/6.92
gt0(Nil, z0) → False 25.05/6.92
gcd(Nil, Nil) → Nil 25.05/6.92
gcd(Nil, Cons(z0, z1)) → Nil 25.05/6.92
gcd(Cons(z0, z1), Nil) → Nil 25.05/6.92
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 25.05/6.92
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.92
lgth(Nil) → Nil 25.05/6.92
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.92
eqList(Cons(z0, z1), Nil) → False 25.05/6.92
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.94
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
GOAL(z0, z1) → c24(GCD(z0, z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(EQLIST(Cons(z0, z1), Cons(z2, z3)))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
GOAL(z0, z1) → c24(GCD(z0, z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(EQLIST(Cons(z0, z1), Cons(z2, z3)))

K tuples:none
Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, GOAL, EQLIST, GCD

Compound Symbols:

c4, c6, c8, c11, c17, c23, c24, c19, c

25.05/6.94

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0, z1) → c24(GCD(z0, z1)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(EQLIST(Cons(z0, z1), Cons(z2, z3)))

25.05/6.94

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.05/6.94
monus[Ite](True, Cons(z0, z1), z2) → z1 25.05/6.94
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.05/6.94
gcd[Ite][False][Ite](True, z0, z1) → z0 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0 25.05/6.94
gt0(Cons(z0, z1), Nil) → True 25.05/6.94
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.05/6.94
gt0(Nil, z0) → False 25.05/6.94
gcd(Nil, Nil) → Nil 25.05/6.94
gcd(Nil, Cons(z0, z1)) → Nil 25.05/6.94
gcd(Cons(z0, z1), Nil) → Nil 25.05/6.94
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.94
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

K tuples:none
Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD

Compound Symbols:

c4, c6, c8, c11, c17, c23, c19, c

25.05/6.94

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

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

GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1))

25.05/6.94

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.05/6.94
monus[Ite](True, Cons(z0, z1), z2) → z1 25.05/6.94
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.05/6.94
gcd[Ite][False][Ite](True, z0, z1) → z0 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0 25.05/6.94
gt0(Cons(z0, z1), Nil) → True 25.05/6.94
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.05/6.94
gt0(Nil, z0) → False 25.05/6.94
gcd(Nil, Nil) → Nil 25.05/6.94
gcd(Nil, Cons(z0, z1)) → Nil 25.05/6.94
gcd(Cons(z0, z1), Nil) → Nil 25.05/6.94
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.94
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))

K tuples:

GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1))

Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD

Compound Symbols:

c4, c6, c8, c11, c17, c23, c19, c

25.05/6.94

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3))

We considered the (Usable) Rules:

eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0

And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

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

POL(@(x₁, x₂)) = [3] + x₁ 25.05/6.94
POL(@'(x₁, x₂)) = 0 25.05/6.94
POL(Cons(x₁, x₂)) = [1] + x₁ + x₂ 25.05/6.94
POL(EQLIST(x₁, x₂)) = 0 25.05/6.94
POL(False) = 0 25.05/6.94
POL(GCD(x₁, x₂)) = [1] + x₁ + [4]x₂ 25.05/6.94
POL(GCD[ITE][FALSE][ITE](x₁, x₂, x₃)) = [3] + x₂ 25.05/6.94
POL(GT0(x₁, x₂)) = [1] + x₁ 25.05/6.94
POL(LGTH(x₁)) = 0 25.05/6.94
POL(MONUS(x₁, x₂)) = 0 25.05/6.94
POL(MONUS[ITE](x₁, x₂, x₃)) = 0 25.05/6.94
POL(Nil) = 0 25.05/6.94
POL(True) = 0 25.05/6.94
POL(and(x₁, x₂)) = [3] 25.05/6.94
POL(c(x₁)) = x₁ 25.05/6.94
POL(c11(x₁)) = x₁ 25.05/6.94
POL(c17(x₁, x₂)) = x₁ + x₂ 25.05/6.94
POL(c19(x₁, x₂)) = x₁ + x₂ 25.05/6.94
POL(c23(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 25.05/6.94
POL(c4(x₁)) = x₁ 25.05/6.94
POL(c6(x₁)) = x₁ 25.05/6.94
POL(c8(x₁)) = x₁ 25.05/6.94
POL(eqList(x₁, x₂)) = 0 25.05/6.94
POL(lgth(x₁)) = [4] + [2]x₁

25.05/6.94

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.05/6.94
monus[Ite](True, Cons(z0, z1), z2) → z1 25.05/6.94
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.05/6.94
gcd[Ite][False][Ite](True, z0, z1) → z0 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0 25.05/6.94
gt0(Cons(z0, z1), Nil) → True 25.05/6.94
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.05/6.94
gt0(Nil, z0) → False 25.05/6.94
gcd(Nil, Nil) → Nil 25.05/6.94
gcd(Nil, Cons(z0, z1)) → Nil 25.05/6.94
gcd(Cons(z0, z1), Nil) → Nil 25.05/6.94
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.94
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))

K tuples:

GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3))

Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD

Compound Symbols:

c4, c6, c8, c11, c17, c23, c19, c

25.05/6.94

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))

We considered the (Usable) Rules:

eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0

And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

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

POL(@(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ 25.05/6.94
POL(@'(x₁, x₂)) = 0 25.05/6.94
POL(Cons(x₁, x₂)) = [1] + x₂ 25.05/6.94
POL(EQLIST(x₁, x₂)) = 0 25.05/6.94
POL(False) = 0 25.05/6.94
POL(GCD(x₁, x₂)) = 0 25.05/6.94
POL(GCD[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0 25.05/6.94
POL(GT0(x₁, x₂)) = 0 25.05/6.94
POL(LGTH(x₁)) = 0 25.05/6.94
POL(MONUS(x₁, x₂)) = [1] + [2]x₁ 25.05/6.94
POL(MONUS[ITE](x₁, x₂, x₃)) = [2]x₂ 25.05/6.94
POL(Nil) = 0 25.05/6.94
POL(True) = 0 25.05/6.94
POL(and(x₁, x₂)) = [3] 25.05/6.94
POL(c(x₁)) = x₁ 25.05/6.94
POL(c11(x₁)) = x₁ 25.05/6.94
POL(c17(x₁, x₂)) = x₁ + x₂ 25.05/6.94
POL(c19(x₁, x₂)) = x₁ + x₂ 25.05/6.94
POL(c23(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 25.05/6.94
POL(c4(x₁)) = x₁ 25.05/6.94
POL(c6(x₁)) = x₁ 25.05/6.94
POL(c8(x₁)) = x₁ 25.05/6.94
POL(eqList(x₁, x₂)) = 0 25.05/6.94
POL(lgth(x₁)) = 0

25.05/6.94

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.05/6.94
monus[Ite](True, Cons(z0, z1), z2) → z1 25.05/6.94
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.05/6.94
gcd[Ite][False][Ite](True, z0, z1) → z0 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0 25.05/6.94
gt0(Cons(z0, z1), Nil) → True 25.05/6.94
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.05/6.94
gt0(Nil, z0) → False 25.05/6.94
gcd(Nil, Nil) → Nil 25.05/6.94
gcd(Nil, Cons(z0, z1)) → Nil 25.05/6.94
gcd(Cons(z0, z1), Nil) → Nil 25.05/6.94
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.94
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))

K tuples:

GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))

Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD

Compound Symbols:

c4, c6, c8, c11, c17, c23, c19, c

25.05/6.94

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))

We considered the (Usable) Rules:

eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0

And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

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

POL(@(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ 25.05/6.94
POL(@'(x₁, x₂)) = 0 25.05/6.94
POL(Cons(x₁, x₂)) = [2] + x₁ + x₂ 25.05/6.94
POL(EQLIST(x₁, x₂)) = [1] + x₂ 25.05/6.94
POL(False) = 0 25.05/6.94
POL(GCD(x₁, x₂)) = 0 25.05/6.94
POL(GCD[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0 25.05/6.94
POL(GT0(x₁, x₂)) = 0 25.05/6.94
POL(LGTH(x₁)) = [1] 25.05/6.94
POL(MONUS(x₁, x₂)) = [5] + [4]x₁ 25.05/6.94
POL(MONUS[ITE](x₁, x₂, x₃)) = [4]x₂ 25.05/6.94
POL(Nil) = 0 25.05/6.94
POL(True) = 0 25.05/6.94
POL(and(x₁, x₂)) = [3] 25.05/6.94
POL(c(x₁)) = x₁ 25.05/6.94
POL(c11(x₁)) = x₁ 25.05/6.94
POL(c17(x₁, x₂)) = x₁ + x₂ 25.05/6.94
POL(c19(x₁, x₂)) = x₁ + x₂ 25.05/6.94
POL(c23(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 25.05/6.94
POL(c4(x₁)) = x₁ 25.05/6.94
POL(c6(x₁)) = x₁ 25.05/6.94
POL(c8(x₁)) = x₁ 25.05/6.94
POL(eqList(x₁, x₂)) = 0 25.05/6.94
POL(lgth(x₁)) = 0

25.05/6.94

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.05/6.94
monus[Ite](True, Cons(z0, z1), z2) → z1 25.05/6.94
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.05/6.94
gcd[Ite][False][Ite](True, z0, z1) → z0 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0 25.05/6.94
gt0(Cons(z0, z1), Nil) → True 25.05/6.94
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.05/6.94
gt0(Nil, z0) → False 25.05/6.94
gcd(Nil, Nil) → Nil 25.05/6.94
gcd(Nil, Cons(z0, z1)) → Nil 25.05/6.94
gcd(Cons(z0, z1), Nil) → Nil 25.05/6.94
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.94
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))

K tuples:

GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))

Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD

Compound Symbols:

c4, c6, c8, c11, c17, c23, c19, c

25.05/6.94

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))

We considered the (Usable) Rules:

eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.94
eqList(Cons(z0, z1), Nil) → False 25.05/6.94
eqList(Nil, Cons(z0, z1)) → False 25.05/6.94
eqList(Nil, Nil) → True 25.05/6.94
and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.94
lgth(Nil) → Nil 25.05/6.94
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.94
@(Nil, z0) → z0

And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.94
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.94
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.94
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.94
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.94
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

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

POL(@(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ + [3]x₂² + [3]x₁·x₂ + [3]x₁² 25.05/6.94
POL(@'(x₁, x₂)) = 0 25.05/6.94
POL(Cons(x₁, x₂)) = [1] + x₂ 25.05/6.94
POL(EQLIST(x₁, x₂)) = 0 25.05/6.94
POL(False) = 0 25.05/6.94
POL(GCD(x₁, x₂)) = x₁·x₂ 25.05/6.94
POL(GCD[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0 25.05/6.94
POL(GT0(x₁, x₂)) = 0 25.05/6.94
POL(LGTH(x₁)) = x₁ 25.05/6.94
POL(MONUS(x₁, x₂)) = x₂ + x₁·x₂ 25.05/6.94
POL(MONUS[ITE](x₁, x₂, x₃)) = x₂·x₃ 25.05/6.94
POL(Nil) = 0 25.05/6.94
POL(True) = 0 25.05/6.94
POL(and(x₁, x₂)) = [3] 25.05/6.94
POL(c(x₁)) = x₁ 25.05/6.94
POL(c11(x₁)) = x₁ 25.05/6.94
POL(c17(x₁, x₂)) = x₁ + x₂ 25.05/6.94
POL(c19(x₁, x₂)) = x₁ + x₂ 25.05/6.94
POL(c23(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 25.05/6.94
POL(c4(x₁)) = x₁ 25.05/6.94
POL(c6(x₁)) = x₁ 25.05/6.94
POL(c8(x₁)) = x₁ 25.05/6.94
POL(eqList(x₁, x₂)) = 0 25.05/6.94
POL(lgth(x₁)) = 0

25.05/6.94

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.05/6.94
and(True, False) → False 25.05/6.94
and(False, True) → False 25.05/6.94
and(True, True) → True 25.05/6.94
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.05/6.95
monus[Ite](True, Cons(z0, z1), z2) → z1 25.05/6.95
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.05/6.95
gcd[Ite][False][Ite](True, z0, z1) → z0 25.05/6.95
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.95
@(Nil, z0) → z0 25.05/6.95
gt0(Cons(z0, z1), Nil) → True 25.05/6.95
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.05/6.95
gt0(Nil, z0) → False 25.05/6.95
gcd(Nil, Nil) → Nil 25.05/6.95
gcd(Nil, Cons(z0, z1)) → Nil 25.05/6.95
gcd(Cons(z0, z1), Nil) → Nil 25.05/6.95
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 25.05/6.95
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.95
lgth(Nil) → Nil 25.05/6.95
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.95
eqList(Cons(z0, z1), Nil) → False 25.05/6.95
eqList(Nil, Cons(z0, z1)) → False 25.05/6.95
eqList(Nil, Nil) → True 25.05/6.95
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.95
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.95
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.95
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.95
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.95
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.95
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.95
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.95
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2))

K tuples:

GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.95
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.95
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.95
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.95
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.95
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))

Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD

Compound Symbols:

c4, c6, c8, c11, c17, c23, c19, c

25.05/6.95

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

@'(Cons(z0, z1), z2) → c8(@'(z1, z2))

We considered the (Usable) Rules:

eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.95
eqList(Cons(z0, z1), Nil) → False 25.05/6.95
eqList(Nil, Cons(z0, z1)) → False 25.05/6.95
eqList(Nil, Nil) → True 25.05/6.95
and(False, False) → False 25.05/6.95
and(True, False) → False 25.05/6.95
and(False, True) → False 25.05/6.95
and(True, True) → True 25.05/6.95
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.95
lgth(Nil) → Nil 25.05/6.95
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.95
@(Nil, z0) → z0

And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.95
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.95
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.95
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.95
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.95
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.95
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.95
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

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

POL(@(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ + [3]x₂² + [3]x₁·x₂ + [3]x₁² 25.05/6.95
POL(@'(x₁, x₂)) = x₁² 25.05/6.95
POL(Cons(x₁, x₂)) = [2] + x₁ + x₂ 25.05/6.95
POL(EQLIST(x₁, x₂)) = 0 25.05/6.95
POL(False) = 0 25.05/6.95
POL(GCD(x₁, x₂)) = x₂ 25.05/6.95
POL(GCD[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0 25.05/6.95
POL(GT0(x₁, x₂)) = 0 25.05/6.95
POL(LGTH(x₁)) = [3]x₁ 25.05/6.95
POL(MONUS(x₁, x₂)) = [2] + [2]x₁ + [3]x₂ + x₂² + x₁² 25.05/6.95
POL(MONUS[ITE](x₁, x₂, x₃)) = x₃² + x₂² 25.05/6.95
POL(Nil) = 0 25.05/6.95
POL(True) = 0 25.05/6.95
POL(and(x₁, x₂)) = [3] 25.05/6.95
POL(c(x₁)) = x₁ 25.05/6.95
POL(c11(x₁)) = x₁ 25.05/6.95
POL(c17(x₁, x₂)) = x₁ + x₂ 25.05/6.95
POL(c19(x₁, x₂)) = x₁ + x₂ 25.05/6.95
POL(c23(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 25.05/6.95
POL(c4(x₁)) = x₁ 25.05/6.95
POL(c6(x₁)) = x₁ 25.05/6.95
POL(c8(x₁)) = x₁ 25.05/6.95
POL(eqList(x₁, x₂)) = [2] 25.05/6.95
POL(lgth(x₁)) = 0

25.05/6.95

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.05/6.95
and(True, False) → False 25.05/6.95
and(False, True) → False 25.05/6.95
and(True, True) → True 25.05/6.95
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.05/6.95
monus[Ite](True, Cons(z0, z1), z2) → z1 25.05/6.95
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.05/6.95
gcd[Ite][False][Ite](True, z0, z1) → z0 25.05/6.95
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.05/6.95
@(Nil, z0) → z0 25.05/6.95
gt0(Cons(z0, z1), Nil) → True 25.05/6.95
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.05/6.95
gt0(Nil, z0) → False 25.05/6.95
gcd(Nil, Nil) → Nil 25.05/6.95
gcd(Nil, Cons(z0, z1)) → Nil 25.05/6.95
gcd(Cons(z0, z1), Nil) → Nil 25.05/6.95
gcd(Cons(z0, z1), Cons(z2, z3)) → gcd[Ite][False][Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) 25.05/6.95
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.05/6.95
lgth(Nil) → Nil 25.05/6.95
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.05/6.95
eqList(Cons(z0, z1), Nil) → False 25.05/6.95
eqList(Nil, Cons(z0, z1)) → False 25.05/6.95
eqList(Nil, Nil) → True 25.05/6.95
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.05/6.95
goal(z0, z1) → gcd(z0, z1)

Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.05/6.95
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.95
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.95
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.95
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.95
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.95
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.95
GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)))

S tuples:none
K tuples:

GCD(Cons(z0, z1), Cons(z2, z3)) → c(GCD[ITE][FALSE][ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))) 25.05/6.95
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.05/6.95
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.05/6.95
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.05/6.95
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.05/6.95
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.05/6.95
@'(Cons(z0, z1), z2) → c8(@'(z1, z2))

Defined Rule Symbols:

@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]

Defined Pair Symbols:

MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD

Compound Symbols:

c4, c6, c8, c11, c17, c23, c19, c

25.05/6.95

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

The set S is empty

25.05/6.95

(22) BOUNDS(O(1), O(1))

25.05/6.95