*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
b(r(x)) -> r(b(x))
b(w(x)) -> w(b(x))
w(r(x)) -> r(w(x))
Weak DP Rules:
Weak TRS Rules:
Signature:
{b/1,w/1} / {r/1}
Obligation:
Innermost
basic terms: {b,w}/{r}
Applied Processor:
Bounds {initialAutomaton = minimal, enrichment = match}
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with follwoing automaton.
b_0(2) -> 1
b_1(2) -> 3
r_0(2) -> 2
r_1(3) -> 1
r_1(3) -> 3
w_0(2) -> 1
w_1(2) -> 3
*** 1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
b(r(x)) -> r(b(x))
b(w(x)) -> w(b(x))
w(r(x)) -> r(w(x))
Signature:
{b/1,w/1} / {r/1}
Obligation:
Innermost
basic terms: {b,w}/{r}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).