The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 14 ms)
↳2 CpxTRS
↳3 RcToIrcProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTRS
↳5 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 CdtProblem
↳11 CdtUsableRulesProof (⇔, 0 ms)
↳12 CdtProblem
↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 120 ms)
↳14 CdtProblem
↳15 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Rewrite Strategy: FULL

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

(2) Obligation:

The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

circ(s, id) → s
circ(id, s) → s
circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
subst(a, id) → a
msubst(a, id) → a
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))

Rewrite Strategy: FULL

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

Converted rc-obligation to irc-obligation.

As the TRS does not nest defined symbols, we have rc = irc.

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

circ(s, id) → s
circ(id, s) → s
circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
subst(a, id) → a
msubst(a, id) → a
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
subst(z0, id) → z0
msubst(z0, id) → z0
Tuples:

CIRC(z0, id) → c
CIRC(id, z0) → c1
CIRC(cons(z0, z1), z2) → c2(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
SUBST(z0, id) → c5
MSUBST(z0, id) → c6
S tuples:

CIRC(z0, id) → c
CIRC(id, z0) → c1
CIRC(cons(z0, z1), z2) → c2(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
SUBST(z0, id) → c5
MSUBST(z0, id) → c6
K tuples:none
Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC, SUBST, MSUBST

Compound Symbols:

c, c1, c2, c3, c4, c5, c6

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing nodes:

MSUBST(z0, id) → c6
SUBST(z0, id) → c5
CIRC(id, z0) → c1
CIRC(z0, id) → c

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
subst(z0, id) → z0
msubst(z0, id) → z0
Tuples:

CIRC(cons(z0, z1), z2) → c2(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
S tuples:

CIRC(cons(z0, z1), z2) → c2(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
K tuples:none
Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC

Compound Symbols:

c2, c3, c4

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

Removed 1 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
subst(z0, id) → z0
msubst(z0, id) → z0
Tuples:

CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
CIRC(cons(z0, z1), z2) → c2(CIRC(z1, z2))
S tuples:

CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
CIRC(cons(z0, z1), z2) → c2(CIRC(z1, z2))
K tuples:none
Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC

Compound Symbols:

c3, c4, c2

(11) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
subst(z0, id) → z0
msubst(z0, id) → z0

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
CIRC(cons(z0, z1), z2) → c2(CIRC(z1, z2))
S tuples:

CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
CIRC(cons(z0, z1), z2) → c2(CIRC(z1, z2))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

CIRC

Compound Symbols:

c3, c4, c2

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

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

CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
CIRC(cons(z0, z1), z2) → c2(CIRC(z1, z2))
We considered the (Usable) Rules:none
And the Tuples:

CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
CIRC(cons(z0, z1), z2) → c2(CIRC(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CIRC(x1, x2)) = x2 + x1·x2 + x12   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(cons(x1, x2)) = [1] + x2   
POL(lift) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
CIRC(cons(z0, z1), z2) → c2(CIRC(z1, z2))
S tuples:none
K tuples:

CIRC(cons(lift, z0), cons(lift, z1)) → c3(CIRC(z0, z1))
CIRC(cons(lift, z0), cons(z1, z2)) → c4(CIRC(z0, z2))
CIRC(cons(z0, z1), z2) → c2(CIRC(z1, z2))
Defined Rule Symbols:none

Defined Pair Symbols:

CIRC

Compound Symbols:

c3, c4, c2

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

The set S is empty

(16) BOUNDS(1, 1)