(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)