YES(O(1), O(n^2)) 25.49/6.97 YES(O(1), O(n^2)) 25.84/7.01 25.84/7.01 25.84/7.01 25.84/7.01 25.84/7.01 25.84/7.01 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 25.84/7.01 25.84/7.01 25.84/7.01
25.84/7.01
25.84/7.01
25.84/7.01
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxRelTRS
25.84/7.01 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
25.84/7.01 
↳2 CdtProblem
25.84/7.01 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
25.84/7.01 
↳4 CdtProblem
25.84/7.01 
↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
25.84/7.01 
↳6 CdtProblem
25.84/7.01 
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)
25.84/7.01 
↳8 CdtProblem
25.84/7.01 
↳9 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
25.84/7.01 
↳10 CdtProblem
25.84/7.01 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
25.84/7.01 
↳12 CdtProblem
25.84/7.01 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
25.84/7.01 
↳14 CdtProblem
25.84/7.01 
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
25.84/7.01 
↳16 CdtProblem
25.84/7.01 
↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
25.84/7.01 
↳18 CdtProblem
25.84/7.01 
↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
25.84/7.01 
↳20 CdtProblem
25.84/7.01 
↳21 SIsEmptyProof (BOTH BOUNDS(ID, ID))
25.84/7.01 
↳22 BOUNDS(O(1), O(1))
25.84/7.01
25.84/7.01 25.84/7.01
25.84/7.01
25.84/7.01

(0) Obligation:

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

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

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

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

Rewrite Strategy: INNERMOST
25.84/7.01
25.84/7.01

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

Relative innermost TRS to CDT Problem.
25.84/7.01
25.84/7.01

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.01
and(True, False) → False 25.84/7.01
and(False, True) → False 25.84/7.01
and(True, True) → True 25.84/7.01
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.01
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.01
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.01
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.01
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.01
@(Nil, z0) → z0 25.84/7.01
gt0(Cons(z0, z1), Nil) → True 25.84/7.01
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.01
gt0(Nil, z0) → False 25.84/7.01
gcd(Nil, Nil) → Nil 25.84/7.01
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.01
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.01
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.84/7.01
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.01
lgth(Nil) → Nil 25.84/7.01
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.01
eqList(Cons(z0, z1), Nil) → False 25.84/7.03
eqList(Nil, Cons(z0, z1)) → False 25.84/7.03
eqList(Nil, Nil) → True 25.84/7.03
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.03
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.03
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.03
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.03
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.03
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.84/7.03
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.03
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.03
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.03
GOAL(z0, z1) → c24(GCD(z0, z1))
S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.03
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.03
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.84/7.03
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.03
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.03
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.03
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

25.84/7.03
25.84/7.03

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

Removed 1 trailing tuple parts
25.84/7.03
25.84/7.03

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.03
and(True, False) → False 25.84/7.03
and(False, True) → False 25.84/7.03
and(True, True) → True 25.84/7.03
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.03
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.03
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.03
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.03
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.03
@(Nil, z0) → z0 25.84/7.03
gt0(Cons(z0, z1), Nil) → True 25.84/7.03
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.03
gt0(Nil, z0) → False 25.84/7.03
gcd(Nil, Nil) → Nil 25.84/7.03
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.03
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.03
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.84/7.03
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.03
lgth(Nil) → Nil 25.84/7.03
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.03
eqList(Cons(z0, z1), Nil) → False 25.84/7.03
eqList(Nil, Cons(z0, z1)) → False 25.84/7.03
eqList(Nil, Nil) → True 25.84/7.03
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.03
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.03
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.03
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.03
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.03
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.84/7.03
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.03
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.03
GOAL(z0, z1) → c24(GCD(z0, z1)) 25.84/7.03
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))
S tuples:

@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.03
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.03
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.84/7.03
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.03
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.03
GOAL(z0, z1) → c24(GCD(z0, z1)) 25.84/7.03
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.84/7.03
25.84/7.03

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

Split RHS of tuples not part of any SCC
25.84/7.03
25.84/7.03

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.03
and(True, False) → False 25.84/7.03
and(False, True) → False 25.84/7.03
and(True, True) → True 25.84/7.03
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.03
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.03
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.03
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.03
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.03
@(Nil, z0) → z0 25.84/7.03
gt0(Cons(z0, z1), Nil) → True 25.84/7.03
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.03
gt0(Nil, z0) → False 25.84/7.03
gcd(Nil, Nil) → Nil 25.84/7.03
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.03
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.03
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.84/7.03
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.03
lgth(Nil) → Nil 25.84/7.03
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.03
eqList(Cons(z0, z1), Nil) → False 25.84/7.03
eqList(Nil, Cons(z0, z1)) → False 25.84/7.03
eqList(Nil, Nil) → True 25.84/7.03
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.03
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.03
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.03
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.03
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.03
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.03
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.03
GOAL(z0, z1) → c24(GCD(z0, z1)) 25.84/7.03
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.03
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.84/7.03
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.84/7.03
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.03
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.03
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.03
GOAL(z0, z1) → c24(GCD(z0, z1)) 25.84/7.03
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.03
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.84/7.03
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.84/7.03
25.84/7.03

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0, z1) → c24(GCD(z0, z1)) 25.84/7.03
GCD(Cons(z0, z1), Cons(z2, z3)) → c(EQLIST(Cons(z0, z1), Cons(z2, z3)))
25.84/7.03
25.84/7.03

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.03
and(True, False) → False 25.84/7.03
and(False, True) → False 25.84/7.03
and(True, True) → True 25.84/7.03
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.03
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.03
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.03
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.03
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.03
@(Nil, z0) → z0 25.84/7.03
gt0(Cons(z0, z1), Nil) → True 25.84/7.03
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.03
gt0(Nil, z0) → False 25.84/7.03
gcd(Nil, Nil) → Nil 25.84/7.03
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.03
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.03
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.84/7.03
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.03
lgth(Nil) → Nil 25.84/7.04
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.04
eqList(Cons(z0, z1), Nil) → False 25.84/7.04
eqList(Nil, Cons(z0, z1)) → False 25.84/7.04
eqList(Nil, Nil) → True 25.84/7.04
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.04
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.04
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.04
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.04
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.04
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.04
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.04
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.04
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.84/7.04
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.04
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.04
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.04
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.04
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.84/7.04
25.84/7.04

(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.84/7.04
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1))
25.84/7.04
25.84/7.04

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.04
and(True, False) → False 25.84/7.04
and(False, True) → False 25.84/7.04
and(True, True) → True 25.84/7.04
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.04
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.04
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.04
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.04
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.04
@(Nil, z0) → z0 25.84/7.04
gt0(Cons(z0, z1), Nil) → True 25.84/7.04
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.04
gt0(Nil, z0) → False 25.84/7.04
gcd(Nil, Nil) → Nil 25.84/7.04
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.04
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.04
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.84/7.04
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.04
lgth(Nil) → Nil 25.84/7.04
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.05
eqList(Cons(z0, z1), Nil) → False 25.84/7.05
eqList(Nil, Cons(z0, z1)) → False 25.84/7.05
eqList(Nil, Nil) → True 25.84/7.05
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.05
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.05
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.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
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.84/7.05
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.84/7.05
25.84/7.05

(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.84/7.05
eqList(Cons(z0, z1), Nil) → False 25.84/7.05
eqList(Nil, Cons(z0, z1)) → False 25.84/7.05
eqList(Nil, Nil) → True 25.84/7.05
and(False, False) → False 25.84/7.05
and(True, False) → False 25.84/7.05
and(False, True) → False 25.84/7.05
and(True, True) → True 25.84/7.05
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.05
lgth(Nil) → Nil 25.84/7.05
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.05
@(Nil, z0) → z0
And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.05
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.84/7.05

POL(@(x1, x2)) = [3] + x1    25.84/7.05
POL(@'(x1, x2)) = 0    25.84/7.05
POL(Cons(x1, x2)) = [1] + x1 + x2    25.84/7.05
POL(EQLIST(x1, x2)) = 0    25.84/7.05
POL(False) = 0    25.84/7.05
POL(GCD(x1, x2)) = [1] + x1 + [4]x2    25.84/7.05
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = [3] + x2    25.84/7.05
POL(GT0(x1, x2)) = [1] + x1    25.84/7.05
POL(LGTH(x1)) = 0    25.84/7.05
POL(MONUS(x1, x2)) = 0    25.84/7.05
POL(MONUS[ITE](x1, x2, x3)) = 0    25.84/7.05
POL(Nil) = 0    25.84/7.05
POL(True) = 0    25.84/7.05
POL(and(x1, x2)) = [3]    25.84/7.05
POL(c(x1)) = x1    25.84/7.05
POL(c11(x1)) = x1    25.84/7.05
POL(c17(x1, x2)) = x1 + x2    25.84/7.05
POL(c19(x1, x2)) = x1 + x2    25.84/7.05
POL(c23(x1, x2, x3)) = x1 + x2 + x3    25.84/7.05
POL(c4(x1)) = x1    25.84/7.05
POL(c6(x1)) = x1    25.84/7.05
POL(c8(x1)) = x1    25.84/7.05
POL(eqList(x1, x2)) = 0    25.84/7.05
POL(lgth(x1)) = [4] + [2]x1   
25.84/7.05
25.84/7.05

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.05
and(True, False) → False 25.84/7.05
and(False, True) → False 25.84/7.05
and(True, True) → True 25.84/7.05
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.05
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.05
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.05
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.05
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.05
@(Nil, z0) → z0 25.84/7.05
gt0(Cons(z0, z1), Nil) → True 25.84/7.05
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.05
gt0(Nil, z0) → False 25.84/7.05
gcd(Nil, Nil) → Nil 25.84/7.05
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.05
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.05
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.84/7.05
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.05
lgth(Nil) → Nil 25.84/7.05
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.05
eqList(Cons(z0, z1), Nil) → False 25.84/7.05
eqList(Nil, Cons(z0, z1)) → False 25.84/7.05
eqList(Nil, Nil) → True 25.84/7.05
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.05
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.05
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.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
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.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
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.84/7.05
25.84/7.05

(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.84/7.05
eqList(Cons(z0, z1), Nil) → False 25.84/7.05
eqList(Nil, Cons(z0, z1)) → False 25.84/7.05
eqList(Nil, Nil) → True 25.84/7.05
and(False, False) → False 25.84/7.05
and(True, False) → False 25.84/7.05
and(False, True) → False 25.84/7.05
and(True, True) → True 25.84/7.05
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.05
lgth(Nil) → Nil 25.84/7.05
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.05
@(Nil, z0) → z0
And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.05
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.84/7.05

POL(@(x1, x2)) = [3] + [3]x1 + [3]x2    25.84/7.05
POL(@'(x1, x2)) = 0    25.84/7.05
POL(Cons(x1, x2)) = [1] + x2    25.84/7.05
POL(EQLIST(x1, x2)) = 0    25.84/7.05
POL(False) = 0    25.84/7.05
POL(GCD(x1, x2)) = 0    25.84/7.05
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = 0    25.84/7.05
POL(GT0(x1, x2)) = 0    25.84/7.05
POL(LGTH(x1)) = 0    25.84/7.05
POL(MONUS(x1, x2)) = [1] + [2]x1    25.84/7.05
POL(MONUS[ITE](x1, x2, x3)) = [2]x2    25.84/7.05
POL(Nil) = 0    25.84/7.05
POL(True) = 0    25.84/7.05
POL(and(x1, x2)) = [3]    25.84/7.05
POL(c(x1)) = x1    25.84/7.05
POL(c11(x1)) = x1    25.84/7.05
POL(c17(x1, x2)) = x1 + x2    25.84/7.05
POL(c19(x1, x2)) = x1 + x2    25.84/7.05
POL(c23(x1, x2, x3)) = x1 + x2 + x3    25.84/7.05
POL(c4(x1)) = x1    25.84/7.05
POL(c6(x1)) = x1    25.84/7.05
POL(c8(x1)) = x1    25.84/7.05
POL(eqList(x1, x2)) = 0    25.84/7.05
POL(lgth(x1)) = 0   
25.84/7.05
25.84/7.05

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.05
and(True, False) → False 25.84/7.05
and(False, True) → False 25.84/7.05
and(True, True) → True 25.84/7.05
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.05
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.05
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.05
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.05
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.05
@(Nil, z0) → z0 25.84/7.05
gt0(Cons(z0, z1), Nil) → True 25.84/7.05
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.05
gt0(Nil, z0) → False 25.84/7.05
gcd(Nil, Nil) → Nil 25.84/7.05
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.05
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.05
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.84/7.05
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.05
lgth(Nil) → Nil 25.84/7.05
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.05
eqList(Cons(z0, z1), Nil) → False 25.84/7.05
eqList(Nil, Cons(z0, z1)) → False 25.84/7.05
eqList(Nil, Nil) → True 25.84/7.05
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.05
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.05
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.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
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.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
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.84/7.05
25.84/7.05

(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.84/7.05
eqList(Cons(z0, z1), Nil) → False 25.84/7.05
eqList(Nil, Cons(z0, z1)) → False 25.84/7.05
eqList(Nil, Nil) → True 25.84/7.05
and(False, False) → False 25.84/7.05
and(True, False) → False 25.84/7.05
and(False, True) → False 25.84/7.05
and(True, True) → True 25.84/7.05
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.05
lgth(Nil) → Nil 25.84/7.05
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.05
@(Nil, z0) → z0
And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.05
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.84/7.05

POL(@(x1, x2)) = [3] + [3]x1 + [3]x2    25.84/7.05
POL(@'(x1, x2)) = 0    25.84/7.05
POL(Cons(x1, x2)) = [2] + x1 + x2    25.84/7.05
POL(EQLIST(x1, x2)) = [1] + x2    25.84/7.05
POL(False) = 0    25.84/7.05
POL(GCD(x1, x2)) = 0    25.84/7.05
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = 0    25.84/7.05
POL(GT0(x1, x2)) = 0    25.84/7.05
POL(LGTH(x1)) = [1]    25.84/7.05
POL(MONUS(x1, x2)) = [5] + [4]x1    25.84/7.05
POL(MONUS[ITE](x1, x2, x3)) = [4]x2    25.84/7.05
POL(Nil) = 0    25.84/7.05
POL(True) = 0    25.84/7.05
POL(and(x1, x2)) = [3]    25.84/7.05
POL(c(x1)) = x1    25.84/7.05
POL(c11(x1)) = x1    25.84/7.05
POL(c17(x1, x2)) = x1 + x2    25.84/7.05
POL(c19(x1, x2)) = x1 + x2    25.84/7.05
POL(c23(x1, x2, x3)) = x1 + x2 + x3    25.84/7.05
POL(c4(x1)) = x1    25.84/7.05
POL(c6(x1)) = x1    25.84/7.05
POL(c8(x1)) = x1    25.84/7.05
POL(eqList(x1, x2)) = 0    25.84/7.05
POL(lgth(x1)) = 0   
25.84/7.05
25.84/7.05

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.05
and(True, False) → False 25.84/7.05
and(False, True) → False 25.84/7.05
and(True, True) → True 25.84/7.05
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.05
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.05
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.05
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.05
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.05
@(Nil, z0) → z0 25.84/7.05
gt0(Cons(z0, z1), Nil) → True 25.84/7.05
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.05
gt0(Nil, z0) → False 25.84/7.05
gcd(Nil, Nil) → Nil 25.84/7.05
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.05
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.05
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.84/7.05
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.05
lgth(Nil) → Nil 25.84/7.05
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.05
eqList(Cons(z0, z1), Nil) → False 25.84/7.05
eqList(Nil, Cons(z0, z1)) → False 25.84/7.05
eqList(Nil, Nil) → True 25.84/7.05
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.05
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.05
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.84/7.05
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.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
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.84/7.05
25.84/7.05

(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.84/7.05
eqList(Cons(z0, z1), Nil) → False 25.84/7.05
eqList(Nil, Cons(z0, z1)) → False 25.84/7.05
eqList(Nil, Nil) → True 25.84/7.05
and(False, False) → False 25.84/7.05
and(True, False) → False 25.84/7.05
and(False, True) → False 25.84/7.05
and(True, True) → True 25.84/7.05
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.05
lgth(Nil) → Nil 25.84/7.05
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.05
@(Nil, z0) → z0
And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.05
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.05
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.05
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.05
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.05
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.05
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.05
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.84/7.05

POL(@(x1, x2)) = [3] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2 + [3]x12    25.84/7.05
POL(@'(x1, x2)) = 0    25.84/7.05
POL(Cons(x1, x2)) = [1] + x2    25.84/7.05
POL(EQLIST(x1, x2)) = 0    25.84/7.05
POL(False) = 0    25.84/7.05
POL(GCD(x1, x2)) = x1·x2    25.84/7.05
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = 0    25.84/7.05
POL(GT0(x1, x2)) = 0    25.84/7.05
POL(LGTH(x1)) = x1    25.84/7.05
POL(MONUS(x1, x2)) = x2 + x1·x2    25.84/7.05
POL(MONUS[ITE](x1, x2, x3)) = x2·x3    25.84/7.05
POL(Nil) = 0    25.84/7.05
POL(True) = 0    25.84/7.05
POL(and(x1, x2)) = [3]    25.84/7.05
POL(c(x1)) = x1    25.84/7.05
POL(c11(x1)) = x1    25.84/7.05
POL(c17(x1, x2)) = x1 + x2    25.84/7.05
POL(c19(x1, x2)) = x1 + x2    25.84/7.05
POL(c23(x1, x2, x3)) = x1 + x2 + x3    25.84/7.05
POL(c4(x1)) = x1    25.84/7.05
POL(c6(x1)) = x1    25.84/7.05
POL(c8(x1)) = x1    25.84/7.05
POL(eqList(x1, x2)) = 0    25.84/7.05
POL(lgth(x1)) = 0   
25.84/7.05
25.84/7.05

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.05
and(True, False) → False 25.84/7.05
and(False, True) → False 25.84/7.05
and(True, True) → True 25.84/7.05
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.06
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.06
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.06
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.06
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.06
@(Nil, z0) → z0 25.84/7.06
gt0(Cons(z0, z1), Nil) → True 25.84/7.06
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.06
gt0(Nil, z0) → False 25.84/7.06
gcd(Nil, Nil) → Nil 25.84/7.06
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.06
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.06
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.84/7.06
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.06
lgth(Nil) → Nil 25.84/7.06
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.06
eqList(Cons(z0, z1), Nil) → False 25.84/7.06
eqList(Nil, Cons(z0, z1)) → False 25.84/7.06
eqList(Nil, Nil) → True 25.84/7.06
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.06
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.06
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.06
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.06
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.06
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.06
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.06
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.06
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.84/7.06
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.06
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.06
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.06
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.06
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.84/7.06
25.84/7.06

(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.84/7.06
eqList(Cons(z0, z1), Nil) → False 25.84/7.06
eqList(Nil, Cons(z0, z1)) → False 25.84/7.06
eqList(Nil, Nil) → True 25.84/7.06
and(False, False) → False 25.84/7.06
and(True, False) → False 25.84/7.06
and(False, True) → False 25.84/7.06
and(True, True) → True 25.84/7.06
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.06
lgth(Nil) → Nil 25.84/7.06
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.06
@(Nil, z0) → z0
And the Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.06
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.06
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.06
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.06
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.06
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.06
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.06
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.84/7.06

POL(@(x1, x2)) = [3] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2 + [3]x12    25.84/7.06
POL(@'(x1, x2)) = x12    25.84/7.06
POL(Cons(x1, x2)) = [2] + x1 + x2    25.84/7.06
POL(EQLIST(x1, x2)) = 0    25.84/7.06
POL(False) = 0    25.84/7.06
POL(GCD(x1, x2)) = x2    25.84/7.06
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = 0    25.84/7.06
POL(GT0(x1, x2)) = 0    25.84/7.06
POL(LGTH(x1)) = [3]x1    25.84/7.06
POL(MONUS(x1, x2)) = [2] + [2]x1 + [3]x2 + x22 + x12    25.84/7.06
POL(MONUS[ITE](x1, x2, x3)) = x32 + x22    25.84/7.06
POL(Nil) = 0    25.84/7.06
POL(True) = 0    25.84/7.06
POL(and(x1, x2)) = [3]    25.84/7.06
POL(c(x1)) = x1    25.84/7.06
POL(c11(x1)) = x1    25.84/7.06
POL(c17(x1, x2)) = x1 + x2    25.84/7.06
POL(c19(x1, x2)) = x1 + x2    25.84/7.06
POL(c23(x1, x2, x3)) = x1 + x2 + x3    25.84/7.06
POL(c4(x1)) = x1    25.84/7.06
POL(c6(x1)) = x1    25.84/7.06
POL(c8(x1)) = x1    25.84/7.06
POL(eqList(x1, x2)) = [2]    25.84/7.06
POL(lgth(x1)) = 0   
25.84/7.06
25.84/7.06

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 25.84/7.06
and(True, False) → False 25.84/7.06
and(False, True) → False 25.84/7.06
and(True, True) → True 25.84/7.06
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) → monus(z1, z3) 25.84/7.06
monus[Ite](True, Cons(z0, z1), z2) → z1 25.84/7.06
gcd[Ite][False][Ite](False, z0, z1) → gcd[Ite][False][Ite][False][Ite](gt0(z0, z1), z0, z1) 25.84/7.06
gcd[Ite][False][Ite](True, z0, z1) → z0 25.84/7.06
@(Cons(z0, z1), z2) → Cons(z0, @(z1, z2)) 25.84/7.06
@(Nil, z0) → z0 25.84/7.06
gt0(Cons(z0, z1), Nil) → True 25.84/7.06
gt0(Cons(z0, z1), Cons(z2, z3)) → gt0(z1, z3) 25.84/7.06
gt0(Nil, z0) → False 25.84/7.06
gcd(Nil, Nil) → Nil 25.84/7.06
gcd(Nil, Cons(z0, z1)) → Nil 25.84/7.06
gcd(Cons(z0, z1), Nil) → Nil 25.84/7.06
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.84/7.06
lgth(Cons(z0, z1)) → @(Cons(Nil, Nil), lgth(z1)) 25.84/7.06
lgth(Nil) → Nil 25.84/7.06
eqList(Cons(z0, z1), Cons(z2, z3)) → and(eqList(z0, z2), eqList(z1, z3)) 25.84/7.06
eqList(Cons(z0, z1), Nil) → False 25.84/7.06
eqList(Nil, Cons(z0, z1)) → False 25.84/7.06
eqList(Nil, Nil) → True 25.84/7.06
monus(z0, z1) → monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) 25.84/7.06
goal(z0, z1) → gcd(z0, z1)
Tuples:

MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) → c4(MONUS(z1, z3)) 25.84/7.06
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.06
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.84/7.06
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.06
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.06
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.06
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.06
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.84/7.06
GCD[ITE][FALSE][ITE](False, z0, z1) → c6(GT0(z0, z1)) 25.84/7.06
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3)) 25.84/7.06
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) 25.84/7.06
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3)) 25.84/7.06
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) 25.84/7.06
@'(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.84/7.06
25.84/7.06

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

The set S is empty
25.84/7.06
25.84/7.06

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

25.84/7.06
25.84/7.06
25.84/7.09 EOF