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

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

(0) Obligation:

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


The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Rewrite Strategy: INNERMOST

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

The following rules are not reachable from basic terms in the dependency graph and can be removed:
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))

(2) Obligation:

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


The TRS R consists of the following rules:

check(no(x)) → no(x)
rec(sent(x)) → sent(rec(x))
check(sent(x)) → sent(check(x))
check(up(x)) → up(check(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
rec(rec(x)) → sent(rec(x))
check(no(x)) → no(check(x))
no(up(x)) → up(no(x))
rec(no(x)) → sent(rec(x))
sent(up(x)) → up(sent(x))
check(rec(x)) → rec(check(x))

Rewrite Strategy: INNERMOST

(3) 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:
check(no(x)) → no(x)
rec(sent(x)) → sent(rec(x))
check(sent(x)) → sent(check(x))
rec(rec(x)) → sent(rec(x))
check(no(x)) → no(check(x))
rec(no(x)) → sent(rec(x))
check(rec(x)) → rec(check(x))

(4) Obligation:

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


The TRS R consists of the following rules:

check(up(x)) → up(check(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
no(up(x)) → up(no(x))
sent(up(x)) → up(sent(x))

Rewrite Strategy: INNERMOST

(5) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1.
The certificate found is represented by the following graph.
Start state: 5
Accept states: [6]
Transitions:
5→6[check_1|0, rec_1|0, no_1|0, sent_1|0]
5→7[up_1|1]
5→8[up_1|1]
5→10[up_1|1]
5→11[up_1|1]
5→12[up_1|1]
6→6[up_1|0, bot|0]
7→6[check_1|1]
7→7[up_1|1]
8→9[sent_1|1]
9→6[bot|1]
10→6[rec_1|1]
10→8[up_1|1]
10→10[up_1|1]
11→6[no_1|1]
11→11[up_1|1]
12→6[sent_1|1]
12→12[up_1|1]

(6) BOUNDS(1, n^1)

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

Converted Cpx (relative) TRS to CDT

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

check(up(z0)) → up(check(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
no(up(z0)) → up(no(z0))
sent(up(z0)) → up(sent(z0))
Tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(bot) → c1(SENT(bot))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
S tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(bot) → c1(SENT(bot))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
K tuples:none
Defined Rule Symbols:

check, rec, no, sent

Defined Pair Symbols:

CHECK, REC, NO, SENT

Compound Symbols:

c, c1, c2, c3, c4

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

Removed 1 trailing nodes:

REC(bot) → c1(SENT(bot))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

check(up(z0)) → up(check(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
no(up(z0)) → up(no(z0))
sent(up(z0)) → up(sent(z0))
Tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
S tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
K tuples:none
Defined Rule Symbols:

check, rec, no, sent

Defined Pair Symbols:

CHECK, REC, NO, SENT

Compound Symbols:

c, c2, c3, c4

(11) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

check(up(z0)) → up(check(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
no(up(z0)) → up(no(z0))
sent(up(z0)) → up(sent(z0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
S tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

CHECK, REC, NO, SENT

Compound Symbols:

c, c2, c3, c4

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

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

REC(up(z0)) → c2(REC(z0))
SENT(up(z0)) → c4(SENT(z0))
We considered the (Usable) Rules:none
And the Tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x1)) = 0   
POL(NO(x1)) = 0   
POL(REC(x1)) = x1   
POL(SENT(x1)) = x1   
POL(c(x1)) = x1   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(up(x1)) = [2] + x1   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
S tuples:

CHECK(up(z0)) → c(CHECK(z0))
NO(up(z0)) → c3(NO(z0))
K tuples:

REC(up(z0)) → c2(REC(z0))
SENT(up(z0)) → c4(SENT(z0))
Defined Rule Symbols:none

Defined Pair Symbols:

CHECK, REC, NO, SENT

Compound Symbols:

c, c2, c3, c4

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

CHECK(up(z0)) → c(CHECK(z0))
NO(up(z0)) → c3(NO(z0))
We considered the (Usable) Rules:none
And the Tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x1)) = [2]x1   
POL(NO(x1)) = [2]x1   
POL(REC(x1)) = 0   
POL(SENT(x1)) = 0   
POL(c(x1)) = x1   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(up(x1)) = [2] + x1   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

CHECK(up(z0)) → c(CHECK(z0))
REC(up(z0)) → c2(REC(z0))
NO(up(z0)) → c3(NO(z0))
SENT(up(z0)) → c4(SENT(z0))
S tuples:none
K tuples:

REC(up(z0)) → c2(REC(z0))
SENT(up(z0)) → c4(SENT(z0))
CHECK(up(z0)) → c(CHECK(z0))
NO(up(z0)) → c3(NO(z0))
Defined Rule Symbols:none

Defined Pair Symbols:

CHECK, REC, NO, SENT

Compound Symbols:

c, c2, c3, c4

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

The set S is empty

(18) BOUNDS(1, 1)