YES(O(1), O(n^1)) 3.97/1.43 YES(O(1), O(n^1)) 3.97/1.48 3.97/1.48 3.97/1.48
3.97/1.48 3.97/1.480 CpxTRS3.97/1.48
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))3.97/1.48
↳2 CdtProblem3.97/1.48
↳3 CdtUnreachableProof (⇔)3.97/1.48
↳4 CdtProblem3.97/1.48
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))3.97/1.48
↳6 CdtProblem3.97/1.48
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))3.97/1.48
↳8 CdtProblem3.97/1.48
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))3.97/1.48
↳10 BOUNDS(O(1), O(1))3.97/1.48
circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t)) 3.97/1.48
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t)) 3.97/1.48
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t)) 3.97/1.48
circ(circ(s, t), u) → circ(s, circ(t, u)) 3.97/1.48
circ(s, id) → s 3.97/1.48
circ(id, s) → s 3.97/1.48
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u) 3.97/1.48
subst(a, id) → a 3.97/1.48
msubst(a, id) → a 3.97/1.48
msubst(msubst(a, s), t) → msubst(a, circ(s, t))
Tuples:
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2)) 3.97/1.48
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2)) 3.97/1.48
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1)) 3.97/1.48
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2)) 3.97/1.48
circ(z0, id) → z0 3.97/1.48
circ(id, z0) → z0 3.97/1.48
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2) 3.97/1.48
subst(z0, id) → z0 3.97/1.48
msubst(z0, id) → z0 3.97/1.48
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))
S tuples:
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 3.97/1.48
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 3.97/1.48
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 3.97/1.48
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 3.97/1.48
CIRC(cons(lift, z0), circ(cons(lift, z1), z2)) → c6(CIRC(cons(lift, circ(z0, z1)), z2), CIRC(z0, z1)) 3.97/1.48
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
K tuples:none
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 3.97/1.48
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 3.97/1.48
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 3.97/1.48
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 3.97/1.48
CIRC(cons(lift, z0), circ(cons(lift, z1), z2)) → c6(CIRC(cons(lift, circ(z0, z1)), z2), CIRC(z0, z1)) 3.97/1.48
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
circ, subst, msubst
CIRC, MSUBST
c, c1, c2, c3, c6, c9
CIRC(cons(lift, z0), circ(cons(lift, z1), z2)) → c6(CIRC(cons(lift, circ(z0, z1)), z2), CIRC(z0, z1))
Tuples:
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2)) 4.34/1.52
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2)) 4.34/1.52
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1)) 4.34/1.52
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2)) 4.34/1.52
circ(z0, id) → z0 4.34/1.52
circ(id, z0) → z0 4.34/1.52
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2) 4.34/1.52
subst(z0, id) → z0 4.34/1.52
msubst(z0, id) → z0 4.34/1.52
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))
S tuples:
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
K tuples:none
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
circ, subst, msubst
CIRC, MSUBST
c, c1, c2, c3, c9
We considered the (Usable) Rules:
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
And the Tuples:
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2)) 4.34/1.52
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2)) 4.34/1.52
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1)) 4.34/1.52
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2)) 4.34/1.52
circ(z0, id) → z0 4.34/1.52
circ(id, z0) → z0 4.34/1.52
msubst(z0, id) → z0 4.34/1.52
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))
The order we found is given by the following interpretation:
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
POL(CIRC(x1, x2)) = [4]x1 4.34/1.52
POL(MSUBST(x1, x2)) = [4]x1 4.34/1.52
POL(c(x1, x2)) = x1 + x2 4.34/1.52
POL(c1(x1)) = x1 4.34/1.52
POL(c2(x1)) = x1 4.34/1.52
POL(c3(x1, x2)) = x1 + x2 4.34/1.52
POL(c9(x1, x2)) = x1 + x2 4.34/1.52
POL(circ(x1, x2)) = [1] + [4]x1 + x2 4.34/1.52
POL(cons(x1, x2)) = x1 + x2 4.34/1.52
POL(id) = 0 4.34/1.52
POL(lift) = 0 4.34/1.52
POL(msubst(x1, x2)) = x1 + [2]x2
Tuples:
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2)) 4.34/1.52
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2)) 4.34/1.52
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1)) 4.34/1.52
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2)) 4.34/1.52
circ(z0, id) → z0 4.34/1.52
circ(id, z0) → z0 4.34/1.52
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2) 4.34/1.52
subst(z0, id) → z0 4.34/1.52
msubst(z0, id) → z0 4.34/1.52
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))
S tuples:
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
K tuples:
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
Defined Rule Symbols:
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
circ, subst, msubst
CIRC, MSUBST
c, c1, c2, c3, c9
We considered the (Usable) Rules:
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
And the Tuples:
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2)) 4.34/1.52
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2)) 4.34/1.52
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1)) 4.34/1.52
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2)) 4.34/1.52
circ(z0, id) → z0 4.34/1.52
circ(id, z0) → z0 4.34/1.52
msubst(z0, id) → z0 4.34/1.52
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))
The order we found is given by the following interpretation:
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
POL(CIRC(x1, x2)) = [2]x1 4.34/1.52
POL(MSUBST(x1, x2)) = [5] + x1 4.34/1.52
POL(c(x1, x2)) = x1 + x2 4.34/1.52
POL(c1(x1)) = x1 4.34/1.52
POL(c2(x1)) = x1 4.34/1.52
POL(c3(x1, x2)) = x1 + x2 4.34/1.52
POL(c9(x1, x2)) = x1 + x2 4.34/1.52
POL(circ(x1, x2)) = [1] + [2]x1 + x2 4.34/1.52
POL(cons(x1, x2)) = [4] + x1 + x2 4.34/1.52
POL(id) = 0 4.34/1.52
POL(lift) = 0 4.34/1.52
POL(msubst(x1, x2)) = [2] + [5]x1 + [4]x2
Tuples:
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2)) 4.34/1.52
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2)) 4.34/1.52
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1)) 4.34/1.52
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2)) 4.34/1.52
circ(z0, id) → z0 4.34/1.52
circ(id, z0) → z0 4.34/1.52
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2) 4.34/1.52
subst(z0, id) → z0 4.34/1.52
msubst(z0, id) → z0 4.34/1.52
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))
S tuples:none
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
Defined Rule Symbols:
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2)) 4.34/1.52
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1)) 4.34/1.52
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
circ, subst, msubst
CIRC, MSUBST
c, c1, c2, c3, c9