YES(O(1), O(n^2)) 24.70/6.86 YES(O(1), O(n^2)) 24.70/6.90 24.70/6.90 24.70/6.90
24.70/6.90 24.70/6.900 CpxRelTRS24.70/6.90
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))24.70/6.90
↳2 CdtProblem24.70/6.90
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))24.70/6.90
↳4 CdtProblem24.70/6.90
↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))24.70/6.90
↳6 CdtProblem24.70/6.90
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)24.70/6.90
↳8 CdtProblem24.70/6.90
↳9 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))24.70/6.90
↳10 CdtProblem24.70/6.90
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))24.70/6.90
↳12 CdtProblem24.70/6.90
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))24.70/6.90
↳14 CdtProblem24.70/6.90
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))24.70/6.90
↳16 CdtProblem24.70/6.90
↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))24.70/6.90
↳18 CdtProblem24.70/6.90
↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))24.70/6.90
↳20 CdtProblem24.70/6.90
↳21 SIsEmptyProof (BOTH BOUNDS(ID, ID))24.70/6.90
↳22 BOUNDS(O(1), O(1))24.70/6.90
@(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)
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
Tuples:
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)
S 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))
K tuples:none
@'(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))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, GCD, LGTH, EQLIST, MONUS, GOAL
c4, c6, c8, c11, c16, c17, c19, c23, c24
Tuples:
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)
S 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))
K tuples:none
@'(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))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, GCD, LGTH, MONUS, GOAL, EQLIST
c4, c6, c8, c11, c16, c17, c23, c24, c19
Tuples:
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)
S 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)))
K tuples:none
@'(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)))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, GOAL, EQLIST, GCD
c4, c6, c8, c11, c17, c23, c24, c19, c
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)))
Tuples:
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)
S 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)))
K tuples:none
@'(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)))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD
c4, c6, c8, c11, c17, c23, c19, c
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))
Tuples:
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)
S 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)))
K 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))
Defined Rule Symbols:
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))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD
c4, c6, c8, c11, c17, c23, c19, c
We considered the (Usable) Rules:
GT0(Cons(z0, z1), Cons(z2, z3)) → c11(GT0(z1, z3))
And the Tuples:
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
The order we found is given by the following interpretation:
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)))
POL(@(x1, x2)) = [3] + x1 25.05/6.94
POL(@'(x1, x2)) = 0 25.05/6.94
POL(Cons(x1, x2)) = [1] + x1 + x2 25.05/6.94
POL(EQLIST(x1, x2)) = 0 25.05/6.94
POL(False) = 0 25.05/6.94
POL(GCD(x1, x2)) = [1] + x1 + [4]x2 25.05/6.94
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = [3] + x2 25.05/6.94
POL(GT0(x1, x2)) = [1] + x1 25.05/6.94
POL(LGTH(x1)) = 0 25.05/6.94
POL(MONUS(x1, x2)) = 0 25.05/6.94
POL(MONUS[ITE](x1, x2, x3)) = 0 25.05/6.94
POL(Nil) = 0 25.05/6.94
POL(True) = 0 25.05/6.94
POL(and(x1, x2)) = [3] 25.05/6.94
POL(c(x1)) = x1 25.05/6.94
POL(c11(x1)) = x1 25.05/6.94
POL(c17(x1, x2)) = x1 + x2 25.05/6.94
POL(c19(x1, x2)) = x1 + x2 25.05/6.94
POL(c23(x1, x2, x3)) = x1 + x2 + x3 25.05/6.94
POL(c4(x1)) = x1 25.05/6.94
POL(c6(x1)) = x1 25.05/6.94
POL(c8(x1)) = x1 25.05/6.94
POL(eqList(x1, x2)) = 0 25.05/6.94
POL(lgth(x1)) = [4] + [2]x1
Tuples:
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)
S 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)))
K 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))
Defined Rule Symbols:
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))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD
c4, c6, c8, c11, c17, c23, c19, c
We considered the (Usable) Rules:
MONUS(z0, z1) → c23(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
And the Tuples:
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
The order we found is given by the following interpretation:
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)))
POL(@(x1, x2)) = [3] + [3]x1 + [3]x2 25.05/6.94
POL(@'(x1, x2)) = 0 25.05/6.94
POL(Cons(x1, x2)) = [1] + x2 25.05/6.94
POL(EQLIST(x1, x2)) = 0 25.05/6.94
POL(False) = 0 25.05/6.94
POL(GCD(x1, x2)) = 0 25.05/6.94
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = 0 25.05/6.94
POL(GT0(x1, x2)) = 0 25.05/6.94
POL(LGTH(x1)) = 0 25.05/6.94
POL(MONUS(x1, x2)) = [1] + [2]x1 25.05/6.94
POL(MONUS[ITE](x1, x2, x3)) = [2]x2 25.05/6.94
POL(Nil) = 0 25.05/6.94
POL(True) = 0 25.05/6.94
POL(and(x1, x2)) = [3] 25.05/6.94
POL(c(x1)) = x1 25.05/6.94
POL(c11(x1)) = x1 25.05/6.94
POL(c17(x1, x2)) = x1 + x2 25.05/6.94
POL(c19(x1, x2)) = x1 + x2 25.05/6.94
POL(c23(x1, x2, x3)) = x1 + x2 + x3 25.05/6.94
POL(c4(x1)) = x1 25.05/6.94
POL(c6(x1)) = x1 25.05/6.94
POL(c8(x1)) = x1 25.05/6.94
POL(eqList(x1, x2)) = 0 25.05/6.94
POL(lgth(x1)) = 0
Tuples:
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)
S 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)))
K 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))
Defined Rule Symbols:
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))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD
c4, c6, c8, c11, c17, c23, c19, c
We considered the (Usable) Rules:
EQLIST(Cons(z0, z1), Cons(z2, z3)) → c19(EQLIST(z0, z2), EQLIST(z1, z3))
And the Tuples:
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
The order we found is given by the following interpretation:
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)))
POL(@(x1, x2)) = [3] + [3]x1 + [3]x2 25.05/6.94
POL(@'(x1, x2)) = 0 25.05/6.94
POL(Cons(x1, x2)) = [2] + x1 + x2 25.05/6.94
POL(EQLIST(x1, x2)) = [1] + x2 25.05/6.94
POL(False) = 0 25.05/6.94
POL(GCD(x1, x2)) = 0 25.05/6.94
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = 0 25.05/6.94
POL(GT0(x1, x2)) = 0 25.05/6.94
POL(LGTH(x1)) = [1] 25.05/6.94
POL(MONUS(x1, x2)) = [5] + [4]x1 25.05/6.94
POL(MONUS[ITE](x1, x2, x3)) = [4]x2 25.05/6.94
POL(Nil) = 0 25.05/6.94
POL(True) = 0 25.05/6.94
POL(and(x1, x2)) = [3] 25.05/6.94
POL(c(x1)) = x1 25.05/6.94
POL(c11(x1)) = x1 25.05/6.94
POL(c17(x1, x2)) = x1 + x2 25.05/6.94
POL(c19(x1, x2)) = x1 + x2 25.05/6.94
POL(c23(x1, x2, x3)) = x1 + x2 + x3 25.05/6.94
POL(c4(x1)) = x1 25.05/6.94
POL(c6(x1)) = x1 25.05/6.94
POL(c8(x1)) = x1 25.05/6.94
POL(eqList(x1, x2)) = 0 25.05/6.94
POL(lgth(x1)) = 0
Tuples:
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)
S 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)))
K tuples:
@'(Cons(z0, z1), z2) → c8(@'(z1, z2)) 25.05/6.94
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
Defined Rule Symbols:
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))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD
c4, c6, c8, c11, c17, c23, c19, c
We considered the (Usable) Rules:
LGTH(Cons(z0, z1)) → c17(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
And the Tuples:
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
The order we found is given by the following interpretation:
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)))
POL(@(x1, x2)) = [3] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2 + [3]x12 25.05/6.94
POL(@'(x1, x2)) = 0 25.05/6.94
POL(Cons(x1, x2)) = [1] + x2 25.05/6.94
POL(EQLIST(x1, x2)) = 0 25.05/6.94
POL(False) = 0 25.05/6.94
POL(GCD(x1, x2)) = x1·x2 25.05/6.94
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = 0 25.05/6.94
POL(GT0(x1, x2)) = 0 25.05/6.94
POL(LGTH(x1)) = x1 25.05/6.94
POL(MONUS(x1, x2)) = x2 + x1·x2 25.05/6.94
POL(MONUS[ITE](x1, x2, x3)) = x2·x3 25.05/6.94
POL(Nil) = 0 25.05/6.94
POL(True) = 0 25.05/6.94
POL(and(x1, x2)) = [3] 25.05/6.94
POL(c(x1)) = x1 25.05/6.94
POL(c11(x1)) = x1 25.05/6.94
POL(c17(x1, x2)) = x1 + x2 25.05/6.94
POL(c19(x1, x2)) = x1 + x2 25.05/6.94
POL(c23(x1, x2, x3)) = x1 + x2 + x3 25.05/6.94
POL(c4(x1)) = x1 25.05/6.94
POL(c6(x1)) = x1 25.05/6.94
POL(c8(x1)) = x1 25.05/6.94
POL(eqList(x1, x2)) = 0 25.05/6.94
POL(lgth(x1)) = 0
Tuples:
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)
S 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)))
K tuples:
@'(Cons(z0, z1), z2) → c8(@'(z1, z2))
Defined Rule Symbols:
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))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD
c4, c6, c8, c11, c17, c23, c19, c
We considered the (Usable) Rules:
@'(Cons(z0, z1), z2) → c8(@'(z1, z2))
And the Tuples:
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
The order we found is given by the following interpretation:
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)))
POL(@(x1, x2)) = [3] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2 + [3]x12 25.05/6.95
POL(@'(x1, x2)) = x12 25.05/6.95
POL(Cons(x1, x2)) = [2] + x1 + x2 25.05/6.95
POL(EQLIST(x1, x2)) = 0 25.05/6.95
POL(False) = 0 25.05/6.95
POL(GCD(x1, x2)) = x2 25.05/6.95
POL(GCD[ITE][FALSE][ITE](x1, x2, x3)) = 0 25.05/6.95
POL(GT0(x1, x2)) = 0 25.05/6.95
POL(LGTH(x1)) = [3]x1 25.05/6.95
POL(MONUS(x1, x2)) = [2] + [2]x1 + [3]x2 + x22 + x12 25.05/6.95
POL(MONUS[ITE](x1, x2, x3)) = x32 + x22 25.05/6.95
POL(Nil) = 0 25.05/6.95
POL(True) = 0 25.05/6.95
POL(and(x1, x2)) = [3] 25.05/6.95
POL(c(x1)) = x1 25.05/6.95
POL(c11(x1)) = x1 25.05/6.95
POL(c17(x1, x2)) = x1 + x2 25.05/6.95
POL(c19(x1, x2)) = x1 + x2 25.05/6.95
POL(c23(x1, x2, x3)) = x1 + x2 + x3 25.05/6.95
POL(c4(x1)) = x1 25.05/6.95
POL(c6(x1)) = x1 25.05/6.95
POL(c8(x1)) = x1 25.05/6.95
POL(eqList(x1, x2)) = [2] 25.05/6.95
POL(lgth(x1)) = 0
Tuples:
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)
S tuples:none
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)))
Defined Rule Symbols:
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))
@, gt0, gcd, lgth, eqList, monus, goal, and, monus[Ite], gcd[Ite][False][Ite]
MONUS[ITE], GCD[ITE][FALSE][ITE], @', GT0, LGTH, MONUS, EQLIST, GCD
c4, c6, c8, c11, c17, c23, c19, c