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

(0) Obligation:

The Runtime Complexity (full) 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: 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:
rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(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(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

(2) Obligation:

The Runtime Complexity (full) 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: 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^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: 9
Accept states: [10]
Transitions:
9→10[check_1|0, rec_1|0, no_1|0, sent_1|0]
9→11[up_1|1]
9→12[up_1|1]
9→14[up_1|1]
9→15[up_1|1]
9→16[up_1|1]
10→10[up_1|0, bot|0]
11→10[check_1|1]
11→11[up_1|1]
12→13[sent_1|1]
13→10[bot|1]
14→10[rec_1|1]
14→12[up_1|1]
14→14[up_1|1]
15→10[no_1|1]
15→15[up_1|1]
16→10[sent_1|1]
16→16[up_1|1]

(6) BOUNDS(1, n^1)