YES(O(1), O(n^2)) 34.87/9.44 YES(O(1), O(n^2)) 34.87/9.48 34.87/9.48 34.87/9.48
34.87/9.48 34.87/9.480 CpxTRS34.87/9.48
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))34.87/9.48
↳2 CdtProblem34.87/9.48
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))34.87/9.48
↳4 CdtProblem34.87/9.48
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))34.87/9.48
↳6 CdtProblem34.87/9.48
↳7 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))34.87/9.48
↳8 CdtProblem34.87/9.48
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))34.87/9.48
↳10 CdtProblem34.87/9.48
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))34.87/9.48
↳12 CdtProblem34.87/9.48
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))34.87/9.48
↳14 CdtProblem34.87/9.48
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))34.87/9.48
↳16 CdtProblem34.87/9.48
↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))34.87/9.48
↳18 CdtProblem34.87/9.48
↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))34.87/9.48
↳20 CdtProblem34.87/9.48
↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))34.87/9.48
↳22 CdtProblem34.87/9.48
↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))34.87/9.48
↳24 CdtProblem34.87/9.48
↳25 SIsEmptyProof (BOTH BOUNDS(ID, ID))34.87/9.48
↳26 BOUNDS(O(1), O(1))34.87/9.48
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s) 34.87/9.48
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s) 34.87/9.48
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s) 34.87/9.48
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s)) 34.87/9.48
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s)) 34.87/9.48
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s)) 34.87/9.48
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s)) 34.87/9.48
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s)) 34.87/9.48
Term_sub(Term_var(x), Id) → Term_var(x) 34.87/9.48
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m 34.87/9.48
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s) 34.87/9.48
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s) 34.87/9.48
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t)) 34.87/9.48
Sum_sub(xi, Id) → Sum_term_var(xi) 34.87/9.48
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k) 34.87/9.48
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s) 34.87/9.48
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s) 34.87/9.48
Concat(Concat(s, t), u) → Concat(s, Concat(t, u)) 34.87/9.48
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t)) 34.87/9.48
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t)) 34.87/9.48
Concat(Id, s) → s
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 34.87/9.48
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.48
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.48
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 34.87/9.48
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 34.87/9.48
Term_sub(Term_var(z0), Id) → Term_var(z0) 34.87/9.48
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 34.87/9.48
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.48
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.48
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 34.87/9.48
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 34.87/9.48
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 34.87/9.48
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 34.87/9.48
Sum_sub(z0, Id) → Sum_term_var(z0) 34.87/9.48
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 34.87/9.48
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.48
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.48
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 34.87/9.48
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 34.87/9.48
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 34.87/9.48
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 34.87/9.48
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.48
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.48
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 34.87/9.48
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 34.87/9.48
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 34.87/9.48
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 34.87/9.48
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.48
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 34.87/9.48
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 34.87/9.48
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 34.87/9.48
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 34.87/9.48
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 34.87/9.48
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.48
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 34.87/9.48
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:none
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 34.87/9.48
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.48
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.48
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 34.87/9.48
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 34.87/9.48
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 34.87/9.48
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 34.87/9.48
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.48
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 34.87/9.48
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 34.87/9.48
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 34.87/9.48
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 34.87/9.48
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 34.87/9.48
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.48
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 34.87/9.48
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 34.87/9.48
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 34.87/9.48
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 34.87/9.48
Concat(Id, z0) → z0 34.87/9.48
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.48
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.48
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 34.87/9.48
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 34.87/9.48
Term_sub(Term_var(z0), Id) → Term_var(z0) 34.87/9.48
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 34.87/9.48
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.48
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.48
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 34.87/9.48
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 34.87/9.48
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 34.87/9.48
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 34.87/9.48
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 34.87/9.48
Sum_sub(z0, Id) → Sum_term_var(z0) 34.87/9.48
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 34.87/9.49
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.49
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 34.87/9.49
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.49
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.49
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 34.87/9.49
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 34.87/9.49
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 34.87/9.49
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 34.87/9.49
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.49
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 34.87/9.49
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 34.87/9.49
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 34.87/9.49
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 34.87/9.49
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 34.87/9.49
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.49
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 34.87/9.49
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [2]x1 34.87/9.49
POL(Case(x1, x2, x3)) = x1 + x3 34.87/9.49
POL(Concat(x1, x2)) = x1 + [2]x2 34.87/9.49
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3 34.87/9.49
POL(Cons_usual(x1, x2, x3)) = x1 + x2 + x3 34.87/9.49
POL(FROZEN(x1, x2, x3, x4)) = [2]x1 + [2]x3 34.87/9.49
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4 34.87/9.49
POL(Id) = 0 34.87/9.49
POL(Left) = 0 34.87/9.49
POL(Right) = 0 34.87/9.49
POL(SUM_SUB(x1, x2)) = 0 34.87/9.49
POL(Sum_constant(x1)) = 0 34.87/9.49
POL(Sum_sub(x1, x2)) = 0 34.87/9.49
POL(Sum_term_var(x1)) = x1 34.87/9.49
POL(TERM_SUB(x1, x2)) = [2]x1 34.87/9.49
POL(Term_app(x1, x2)) = [1] + x1 + x2 34.87/9.49
POL(Term_inl(x1)) = x1 34.87/9.49
POL(Term_inr(x1)) = x1 34.87/9.49
POL(Term_pair(x1, x2)) = x1 + x2 34.87/9.49
POL(Term_sub(x1, x2)) = [4]x1 + [2]x2 34.87/9.49
POL(Term_var(x1)) = x1 34.87/9.49
POL(c(x1, x2)) = x1 + x2 34.87/9.49
POL(c1(x1, x2)) = x1 + x2 34.87/9.49
POL(c10(x1)) = x1 34.87/9.49
POL(c11(x1)) = x1 34.87/9.49
POL(c12(x1, x2)) = x1 + x2 34.87/9.49
POL(c15(x1)) = x1 34.87/9.49
POL(c16(x1)) = x1 34.87/9.49
POL(c17(x1, x2)) = x1 + x2 34.87/9.49
POL(c18(x1, x2)) = x1 + x2 34.87/9.49
POL(c19(x1)) = x1 34.87/9.49
POL(c2(x1, x2)) = x1 + x2 34.87/9.49
POL(c3(x1)) = x1 34.87/9.49
POL(c4(x1)) = x1 34.87/9.49
POL(c7(x1)) = x1 34.87/9.49
POL(c8(x1)) = x1 34.87/9.49
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 34.87/9.49
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.49
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.49
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 34.87/9.49
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 34.87/9.49
Term_sub(Term_var(z0), Id) → Term_var(z0) 34.87/9.49
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 34.87/9.49
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.49
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.49
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 34.87/9.49
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 34.87/9.49
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 34.87/9.49
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 34.87/9.49
Sum_sub(z0, Id) → Sum_term_var(z0) 34.87/9.49
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 34.87/9.49
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.49
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.49
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 34.87/9.49
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 34.87/9.49
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 34.87/9.49
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 34.87/9.49
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.49
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.49
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 34.87/9.49
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 34.87/9.49
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 34.87/9.49
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 34.87/9.49
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.49
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 34.87/9.49
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 34.87/9.49
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 34.87/9.49
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.51
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.51
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.51
Concat(Id, z0) → z0 35.35/9.51
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.51
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.51
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.51
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.51
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.51
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.51
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.51
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [2]x1 35.35/9.51
POL(Case(x1, x2, x3)) = [4] + x1 + x3 35.35/9.51
POL(Concat(x1, x2)) = [4]x1 + [2]x2 35.35/9.51
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3 35.35/9.51
POL(Cons_usual(x1, x2, x3)) = [4] + x1 + x2 + x3 35.35/9.51
POL(FROZEN(x1, x2, x3, x4)) = [4] + [2]x1 + [2]x3 35.35/9.51
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4 35.35/9.51
POL(Id) = 0 35.35/9.51
POL(Left) = 0 35.35/9.51
POL(Right) = 0 35.35/9.51
POL(SUM_SUB(x1, x2)) = 0 35.35/9.51
POL(Sum_constant(x1)) = 0 35.35/9.51
POL(Sum_sub(x1, x2)) = 0 35.35/9.51
POL(Sum_term_var(x1)) = x1 35.35/9.51
POL(TERM_SUB(x1, x2)) = [2] + [2]x1 35.35/9.51
POL(Term_app(x1, x2)) = [4] + x1 + x2 35.35/9.51
POL(Term_inl(x1)) = x1 35.35/9.51
POL(Term_inr(x1)) = x1 35.35/9.51
POL(Term_pair(x1, x2)) = [1] + x1 + x2 35.35/9.51
POL(Term_sub(x1, x2)) = [2]x1 + [2]x2 35.35/9.51
POL(Term_var(x1)) = x1 35.35/9.51
POL(c(x1, x2)) = x1 + x2 35.35/9.51
POL(c1(x1, x2)) = x1 + x2 35.35/9.51
POL(c10(x1)) = x1 35.35/9.51
POL(c11(x1)) = x1 35.35/9.51
POL(c12(x1, x2)) = x1 + x2 35.35/9.51
POL(c15(x1)) = x1 35.35/9.51
POL(c16(x1)) = x1 35.35/9.51
POL(c17(x1, x2)) = x1 + x2 35.35/9.51
POL(c18(x1, x2)) = x1 + x2 35.35/9.51
POL(c19(x1)) = x1 35.35/9.51
POL(c2(x1, x2)) = x1 + x2 35.35/9.51
POL(c3(x1)) = x1 35.35/9.51
POL(c4(x1)) = x1 35.35/9.51
POL(c7(x1)) = x1 35.35/9.51
POL(c8(x1)) = x1 35.35/9.51
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.51
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.51
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.51
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.51
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.51
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.51
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.51
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.51
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.51
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.51
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.51
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.51
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.51
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.51
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.51
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.51
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.57
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.57
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.57
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.57
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.57
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.57
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.57
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.57
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.57
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.57
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.57
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.57
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.57
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.57
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.57
Concat(Id, z0) → z0 35.35/9.57
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.57
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.57
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.57
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.57
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.57
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.57
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.57
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.57
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.57
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.57
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.57
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.57
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.57
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.57
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.57
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.57
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.57
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.57
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.57
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.57
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.57
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.57
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.57
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [4]x1 35.35/9.57
POL(Case(x1, x2, x3)) = [1] + x1 + x3 35.35/9.57
POL(Concat(x1, x2)) = [4]x1 + [4]x2 35.35/9.57
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3 35.35/9.57
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3 35.35/9.57
POL(FROZEN(x1, x2, x3, x4)) = [2] + [4]x1 + [4]x3 35.35/9.57
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4 35.35/9.57
POL(Id) = 0 35.35/9.57
POL(Left) = 0 35.35/9.57
POL(Right) = 0 35.35/9.57
POL(SUM_SUB(x1, x2)) = 0 35.35/9.57
POL(Sum_constant(x1)) = 0 35.35/9.57
POL(Sum_sub(x1, x2)) = 0 35.35/9.57
POL(Sum_term_var(x1)) = x1 35.35/9.57
POL(TERM_SUB(x1, x2)) = [4]x1 35.35/9.57
POL(Term_app(x1, x2)) = x1 + x2 35.35/9.57
POL(Term_inl(x1)) = x1 35.35/9.57
POL(Term_inr(x1)) = x1 35.35/9.57
POL(Term_pair(x1, x2)) = x1 + x2 35.35/9.57
POL(Term_sub(x1, x2)) = [4] + [4]x1 + [4]x2 35.35/9.57
POL(Term_var(x1)) = x1 35.35/9.57
POL(c(x1, x2)) = x1 + x2 35.35/9.57
POL(c1(x1, x2)) = x1 + x2 35.35/9.57
POL(c10(x1)) = x1 35.35/9.57
POL(c11(x1)) = x1 35.35/9.57
POL(c12(x1, x2)) = x1 + x2 35.35/9.57
POL(c15(x1)) = x1 35.35/9.57
POL(c16(x1)) = x1 35.35/9.57
POL(c17(x1, x2)) = x1 + x2 35.35/9.57
POL(c18(x1, x2)) = x1 + x2 35.35/9.57
POL(c19(x1)) = x1 35.35/9.57
POL(c2(x1, x2)) = x1 + x2 35.35/9.57
POL(c3(x1)) = x1 35.35/9.57
POL(c4(x1)) = x1 35.35/9.57
POL(c7(x1)) = x1 35.35/9.57
POL(c8(x1)) = x1 35.35/9.57
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.57
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.57
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.57
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.57
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.57
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.57
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.57
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.57
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.57
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.57
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.57
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.57
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.57
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.57
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.57
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.57
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.57
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.57
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.57
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.57
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.57
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [2]x1 35.35/9.58
POL(Case(x1, x2, x3)) = x1 + x3 35.35/9.58
POL(Concat(x1, x2)) = [1] + [4]x1 + [2]x2 35.35/9.58
POL(Cons_sum(x1, x2, x3)) = x1 + x3 35.35/9.58
POL(Cons_usual(x1, x2, x3)) = x1 + x2 + x3 35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [2]x1 + [2]x3 35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4 35.35/9.58
POL(Id) = [2] 35.35/9.58
POL(Left) = 0 35.35/9.58
POL(Right) = 0 35.35/9.58
POL(SUM_SUB(x1, x2)) = 0 35.35/9.58
POL(Sum_constant(x1)) = [2] 35.35/9.58
POL(Sum_sub(x1, x2)) = [4] + [2]x2 35.35/9.58
POL(Sum_term_var(x1)) = 0 35.35/9.58
POL(TERM_SUB(x1, x2)) = [2]x1 35.35/9.58
POL(Term_app(x1, x2)) = x1 + x2 35.35/9.58
POL(Term_inl(x1)) = x1 35.35/9.58
POL(Term_inr(x1)) = x1 35.35/9.58
POL(Term_pair(x1, x2)) = x1 + x2 35.35/9.58
POL(Term_sub(x1, x2)) = [2]x1 + [2]x2 35.35/9.58
POL(Term_var(x1)) = x1 35.35/9.58
POL(c(x1, x2)) = x1 + x2 35.35/9.58
POL(c1(x1, x2)) = x1 + x2 35.35/9.58
POL(c10(x1)) = x1 35.35/9.58
POL(c11(x1)) = x1 35.35/9.58
POL(c12(x1, x2)) = x1 + x2 35.35/9.58
POL(c15(x1)) = x1 35.35/9.58
POL(c16(x1)) = x1 35.35/9.58
POL(c17(x1, x2)) = x1 + x2 35.35/9.58
POL(c18(x1, x2)) = x1 + x2 35.35/9.58
POL(c19(x1)) = x1 35.35/9.58
POL(c2(x1, x2)) = x1 + x2 35.35/9.58
POL(c3(x1)) = x1 35.35/9.58
POL(c4(x1)) = x1 35.35/9.58
POL(c7(x1)) = x1 35.35/9.58
POL(c8(x1)) = x1 35.35/9.58
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [4]x1 35.35/9.58
POL(Case(x1, x2, x3)) = [4] + x1 + x3 35.35/9.58
POL(Concat(x1, x2)) = [2]x1 + x2 35.35/9.58
POL(Cons_sum(x1, x2, x3)) = x1 + x3 35.35/9.58
POL(Cons_usual(x1, x2, x3)) = x1 + x2 + x3 35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [4]x1 + [4]x3 35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4 35.35/9.58
POL(Id) = [4] 35.35/9.58
POL(Left) = 0 35.35/9.58
POL(Right) = 0 35.35/9.58
POL(SUM_SUB(x1, x2)) = 0 35.35/9.58
POL(Sum_constant(x1)) = [2] 35.35/9.58
POL(Sum_sub(x1, x2)) = [4] + x2 35.35/9.58
POL(Sum_term_var(x1)) = 0 35.35/9.58
POL(TERM_SUB(x1, x2)) = [4]x1 35.35/9.58
POL(Term_app(x1, x2)) = x1 + x2 35.35/9.58
POL(Term_inl(x1)) = x1 35.35/9.58
POL(Term_inr(x1)) = [4] + x1 35.35/9.58
POL(Term_pair(x1, x2)) = [4] + x1 + x2 35.35/9.58
POL(Term_sub(x1, x2)) = [4]x1 + x2 35.35/9.58
POL(Term_var(x1)) = x1 35.35/9.58
POL(c(x1, x2)) = x1 + x2 35.35/9.58
POL(c1(x1, x2)) = x1 + x2 35.35/9.58
POL(c10(x1)) = x1 35.35/9.58
POL(c11(x1)) = x1 35.35/9.58
POL(c12(x1, x2)) = x1 + x2 35.35/9.58
POL(c15(x1)) = x1 35.35/9.58
POL(c16(x1)) = x1 35.35/9.58
POL(c17(x1, x2)) = x1 + x2 35.35/9.58
POL(c18(x1, x2)) = x1 + x2 35.35/9.58
POL(c19(x1)) = x1 35.35/9.58
POL(c2(x1, x2)) = x1 + x2 35.35/9.58
POL(c3(x1)) = x1 35.35/9.58
POL(c4(x1)) = x1 35.35/9.58
POL(c7(x1)) = x1 35.35/9.58
POL(c8(x1)) = x1 35.35/9.58
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [2] + [4]x1 35.35/9.58
POL(Case(x1, x2, x3)) = [1] + x1 + x3 35.35/9.58
POL(Concat(x1, x2)) = [2] + [4]x1 + [2]x2 35.35/9.58
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3 35.35/9.58
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3 35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [4] + [4]x1 + [4]x3 35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4 35.35/9.58
POL(Id) = [4] 35.35/9.58
POL(Left) = 0 35.35/9.58
POL(Right) = 0 35.35/9.58
POL(SUM_SUB(x1, x2)) = 0 35.35/9.58
POL(Sum_constant(x1)) = [2] 35.35/9.58
POL(Sum_sub(x1, x2)) = [4] + x2 35.35/9.58
POL(Sum_term_var(x1)) = 0 35.35/9.58
POL(TERM_SUB(x1, x2)) = [4]x1 35.35/9.58
POL(Term_app(x1, x2)) = [1] + x1 + x2 35.35/9.58
POL(Term_inl(x1)) = [4] + x1 35.35/9.58
POL(Term_inr(x1)) = x1 35.35/9.58
POL(Term_pair(x1, x2)) = x1 + x2 35.35/9.58
POL(Term_sub(x1, x2)) = [2] + x1 + [4]x2 35.35/9.58
POL(Term_var(x1)) = x1 35.35/9.58
POL(c(x1, x2)) = x1 + x2 35.35/9.58
POL(c1(x1, x2)) = x1 + x2 35.35/9.58
POL(c10(x1)) = x1 35.35/9.58
POL(c11(x1)) = x1 35.35/9.58
POL(c12(x1, x2)) = x1 + x2 35.35/9.58
POL(c15(x1)) = x1 35.35/9.58
POL(c16(x1)) = x1 35.35/9.58
POL(c17(x1, x2)) = x1 + x2 35.35/9.58
POL(c18(x1, x2)) = x1 + x2 35.35/9.58
POL(c19(x1)) = x1 35.35/9.58
POL(c2(x1, x2)) = x1 + x2 35.35/9.58
POL(c3(x1)) = x1 35.35/9.58
POL(c4(x1)) = x1 35.35/9.58
POL(c7(x1)) = x1 35.35/9.58
POL(c8(x1)) = x1 35.35/9.58
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [2] + [2]x1 35.35/9.58
POL(Case(x1, x2, x3)) = [4] + x1 + x3 35.35/9.58
POL(Concat(x1, x2)) = [4] + [4]x1 + [2]x2 35.35/9.58
POL(Cons_sum(x1, x2, x3)) = [4] + x1 + x2 + x3 35.35/9.58
POL(Cons_usual(x1, x2, x3)) = [2] + x1 + x2 + x3 35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [2]x1 + [2]x3 35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4 35.35/9.58
POL(Id) = [4] 35.35/9.58
POL(Left) = 0 35.35/9.58
POL(Right) = 0 35.35/9.58
POL(SUM_SUB(x1, x2)) = 0 35.35/9.58
POL(Sum_constant(x1)) = 0 35.35/9.58
POL(Sum_sub(x1, x2)) = [2] + x2 35.35/9.58
POL(Sum_term_var(x1)) = 0 35.35/9.58
POL(TERM_SUB(x1, x2)) = [2]x1 35.35/9.58
POL(Term_app(x1, x2)) = [3] + x1 + x2 35.35/9.58
POL(Term_inl(x1)) = x1 35.35/9.58
POL(Term_inr(x1)) = x1 35.35/9.58
POL(Term_pair(x1, x2)) = [3] + x1 + x2 35.35/9.58
POL(Term_sub(x1, x2)) = [1] + x1 + [2]x2 35.35/9.58
POL(Term_var(x1)) = x1 35.35/9.58
POL(c(x1, x2)) = x1 + x2 35.35/9.58
POL(c1(x1, x2)) = x1 + x2 35.35/9.58
POL(c10(x1)) = x1 35.35/9.58
POL(c11(x1)) = x1 35.35/9.58
POL(c12(x1, x2)) = x1 + x2 35.35/9.58
POL(c15(x1)) = x1 35.35/9.58
POL(c16(x1)) = x1 35.35/9.58
POL(c17(x1, x2)) = x1 + x2 35.35/9.58
POL(c18(x1, x2)) = x1 + x2 35.35/9.58
POL(c19(x1)) = x1 35.35/9.58
POL(c2(x1, x2)) = x1 + x2 35.35/9.58
POL(c3(x1)) = x1 35.35/9.58
POL(c4(x1)) = x1 35.35/9.58
POL(c7(x1)) = x1 35.35/9.58
POL(c8(x1)) = x1 35.35/9.58
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = x1 + [2]x1·x2 35.35/9.58
POL(Case(x1, x2, x3)) = [2] + x1 + x3 35.35/9.58
POL(Concat(x1, x2)) = x1 + x2 + [2]x1·x2 35.35/9.58
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3 35.35/9.58
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3 35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = x1 + x3 + [2]x3·x4 + [2]x1·x4 35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [2] + x1 + x3 + [2]x4 + [2]x3·x4 + [2]x1·x4 35.35/9.58
POL(Id) = 0 35.35/9.58
POL(Left) = 0 35.35/9.58
POL(Right) = 0 35.35/9.58
POL(SUM_SUB(x1, x2)) = [2] 35.35/9.58
POL(Sum_constant(x1)) = 0 35.35/9.58
POL(Sum_sub(x1, x2)) = [3]x12 35.35/9.58
POL(Sum_term_var(x1)) = 0 35.35/9.58
POL(TERM_SUB(x1, x2)) = x1 + [2]x1·x2 35.35/9.58
POL(Term_app(x1, x2)) = [2] + x1 + x2 35.35/9.58
POL(Term_inl(x1)) = x1 35.35/9.58
POL(Term_inr(x1)) = x1 35.35/9.58
POL(Term_pair(x1, x2)) = [1] + x1 + x2 35.35/9.58
POL(Term_sub(x1, x2)) = x1 + x2 + [2]x1·x2 35.35/9.58
POL(Term_var(x1)) = [1] 35.35/9.58
POL(c(x1, x2)) = x1 + x2 35.35/9.58
POL(c1(x1, x2)) = x1 + x2 35.35/9.58
POL(c10(x1)) = x1 35.35/9.58
POL(c11(x1)) = x1 35.35/9.58
POL(c12(x1, x2)) = x1 + x2 35.35/9.58
POL(c15(x1)) = x1 35.35/9.58
POL(c16(x1)) = x1 35.35/9.58
POL(c17(x1, x2)) = x1 + x2 35.35/9.58
POL(c18(x1, x2)) = x1 + x2 35.35/9.58
POL(c19(x1)) = x1 35.35/9.58
POL(c2(x1, x2)) = x1 + x2 35.35/9.58
POL(c3(x1)) = x1 35.35/9.58
POL(c4(x1)) = x1 35.35/9.58
POL(c7(x1)) = x1 35.35/9.58
POL(c8(x1)) = x1 35.35/9.58
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [2]x1·x2 + x12 35.35/9.58
POL(Case(x1, x2, x3)) = [1] + x1 + x3 35.35/9.58
POL(Concat(x1, x2)) = x1 + x2 + x1·x2 35.35/9.58
POL(Cons_sum(x1, x2, x3)) = [1] + x1 + x2 + x3 35.35/9.58
POL(Cons_usual(x1, x2, x3)) = [3] + x1 + x2 + x3 35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [2]x3·x4 + [2]x1·x4 + x12 + [2]x1·x3 + x32 35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [1] + x1 + x3 + x3·x4 + x2·x4 + x1·x4 35.35/9.58
POL(Id) = 0 35.35/9.58
POL(Left) = 0 35.35/9.58
POL(Right) = 0 35.35/9.58
POL(SUM_SUB(x1, x2)) = 0 35.35/9.58
POL(Sum_constant(x1)) = [1] 35.35/9.58
POL(Sum_sub(x1, x2)) = [2] 35.35/9.58
POL(Sum_term_var(x1)) = [2] 35.35/9.58
POL(TERM_SUB(x1, x2)) = [2]x1·x2 + x12 35.35/9.58
POL(Term_app(x1, x2)) = [1] + x1 + x2 35.35/9.58
POL(Term_inl(x1)) = x1 35.35/9.58
POL(Term_inr(x1)) = x1 35.35/9.58
POL(Term_pair(x1, x2)) = [1] + x1 + x2 35.35/9.58
POL(Term_sub(x1, x2)) = x1 + x2 + x1·x2 35.35/9.58
POL(Term_var(x1)) = [2] 35.35/9.58
POL(c(x1, x2)) = x1 + x2 35.35/9.58
POL(c1(x1, x2)) = x1 + x2 35.35/9.58
POL(c10(x1)) = x1 35.35/9.58
POL(c11(x1)) = x1 35.35/9.58
POL(c12(x1, x2)) = x1 + x2 35.35/9.58
POL(c15(x1)) = x1 35.35/9.58
POL(c16(x1)) = x1 35.35/9.58
POL(c17(x1, x2)) = x1 + x2 35.35/9.58
POL(c18(x1, x2)) = x1 + x2 35.35/9.58
POL(c19(x1)) = x1 35.35/9.58
POL(c2(x1, x2)) = x1 + x2 35.35/9.58
POL(c3(x1)) = x1 35.35/9.58
POL(c4(x1)) = x1 35.35/9.58
POL(c7(x1)) = x1 35.35/9.58
POL(c8(x1)) = x1 35.35/9.58
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0
S tuples:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.59
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19
We considered the (Usable) Rules:
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.59
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
And the Tuples:
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.59
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.59
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.59
Concat(Id, z0) → z0 35.35/9.59
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.59
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.59
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.59
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.59
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.59
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.59
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.59
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.59
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.59
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.59
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.59
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.59
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.59
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.59
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.59
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.59
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
The order we found is given by the following interpretation:
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.59
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.59
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.59
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.59
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.59
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.59
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
POL(CONCAT(x1, x2)) = [2]x1·x2 + x12 35.35/9.59
POL(Case(x1, x2, x3)) = [1] + x1 + x3 35.35/9.59
POL(Concat(x1, x2)) = x1 + x2 + [3]x1·x2 + [2]x12 35.35/9.59
POL(Cons_sum(x1, x2, x3)) = [3] + x1 + x3 35.35/9.59
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3 35.35/9.59
POL(FROZEN(x1, x2, x3, x4)) = [1] + x2 + [2]x3·x4 + [2]x1·x4 + x12 + [2]x1·x3 + x32 35.35/9.59
POL(Frozen(x1, x2, x3, x4)) = [2] + [2]x1 + [2]x2 + [2]x3 + [2]x4 + [3]x3·x4 + [3]x1·x4 + [2]x12 + [2]x32 35.35/9.59
POL(Id) = 0 35.35/9.59
POL(Left) = 0 35.35/9.59
POL(Right) = 0 35.35/9.59
POL(SUM_SUB(x1, x2)) = x2 35.35/9.59
POL(Sum_constant(x1)) = [3] 35.35/9.59
POL(Sum_sub(x1, x2)) = x2 35.35/9.59
POL(Sum_term_var(x1)) = 0 35.35/9.59
POL(TERM_SUB(x1, x2)) = [2]x1·x2 + x12 35.35/9.59
POL(Term_app(x1, x2)) = [1] + x1 + x2 35.35/9.59
POL(Term_inl(x1)) = x1 35.35/9.59
POL(Term_inr(x1)) = x1 35.35/9.59
POL(Term_pair(x1, x2)) = [1] + x1 + x2 35.35/9.59
POL(Term_sub(x1, x2)) = x1 + x2 + [3]x1·x2 + [2]x12 35.35/9.59
POL(Term_var(x1)) = 0 35.35/9.59
POL(c(x1, x2)) = x1 + x2 35.35/9.59
POL(c1(x1, x2)) = x1 + x2 35.35/9.59
POL(c10(x1)) = x1 35.35/9.59
POL(c11(x1)) = x1 35.35/9.59
POL(c12(x1, x2)) = x1 + x2 35.35/9.59
POL(c15(x1)) = x1 35.35/9.59
POL(c16(x1)) = x1 35.35/9.59
POL(c17(x1, x2)) = x1 + x2 35.35/9.59
POL(c18(x1, x2)) = x1 + x2 35.35/9.59
POL(c19(x1)) = x1 35.35/9.59
POL(c2(x1, x2)) = x1 + x2 35.35/9.59
POL(c3(x1)) = x1 35.35/9.59
POL(c4(x1)) = x1 35.35/9.59
POL(c7(x1)) = x1 35.35/9.59
POL(c8(x1)) = x1 35.35/9.59
POL(c9(x1, x2)) = x1 + x2
Tuples:
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.59
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.59
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.59
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.59
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.59
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.59
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.59
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.59
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.59
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.59
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.59
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.59
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.59
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.59
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.59
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.59
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.59
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.59
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.59
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.59
Concat(Id, z0) → z0
S tuples:none
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.59
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.59
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.59
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.59
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.59
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.59
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
Defined Rule Symbols:
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.59
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.59
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.59
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.59
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.59
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.59
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
Term_sub, Frozen, Sum_sub, Concat
TERM_SUB, FROZEN, SUM_SUB, CONCAT
c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19