125.93/45.58
125.93/45.58
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(f(f(X))) → mark(c(f(g(f(X)))))
125.93/45.58
active(c(X)) → mark(d(X))
125.93/45.58
active(h(X)) → mark(c(d(X)))
125.93/45.58
active(f(X)) → f(active(X))
125.93/45.58
active(h(X)) → h(active(X))
125.93/45.58
f(mark(X)) → mark(f(X))
125.93/45.58
h(mark(X)) → mark(h(X))
125.93/45.58
proper(f(X)) → f(proper(X))
125.93/45.58
proper(c(X)) → c(proper(X))
125.93/45.58
proper(g(X)) → g(proper(X))
125.93/45.58
proper(d(X)) → d(proper(X))
125.93/45.58
proper(h(X)) → h(proper(X))
125.93/45.58
f(ok(X)) → ok(f(X))
125.93/45.58
c(ok(X)) → ok(c(X))
125.93/45.58
g(ok(X)) → ok(g(X))
125.93/45.58
d(ok(X)) → ok(d(X))
125.93/45.58
h(ok(X)) → ok(h(X))
125.93/45.58
top(mark(X)) → top(proper(X))
125.93/45.58
top(ok(X)) → top(active(X))
Rewrite Strategy: INNERMOST
125.93/45.58
125.93/45.58
(1) 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: 5176
Accept states: [5177, 5178, 5179, 5180, 5181, 5182, 5183, 5184]
Transitions:
5176→5177[active_1|0]
5176→5178[f_1|0]
5176→5179[h_1|0]
5176→5180[proper_1|0]
5176→5181[c_1|0]
5176→5182[g_1|0]
5176→5183[d_1|0]
5176→5184[top_1|0]
5176→5176[mark_1|0, ok_1|0]
5176→5185[f_1|1]
5176→5186[h_1|1]
5176→5187[proper_1|1]
5176→5188[f_1|1]
5176→5189[h_1|1]
5176→5190[c_1|1]
5176→5191[g_1|1]
5176→5192[d_1|1]
5176→5193[active_1|1]
5185→5178[mark_1|1]
5185→5185[mark_1|1]
5185→5188[mark_1|1]
5186→5179[mark_1|1]
5186→5186[mark_1|1]
5186→5189[mark_1|1]
5187→5184[top_1|1]
5188→5178[ok_1|1]
5188→5185[ok_1|1]
5188→5188[ok_1|1]
5189→5179[ok_1|1]
5189→5186[ok_1|1]
5189→5189[ok_1|1]
5190→5181[ok_1|1]
5190→5190[ok_1|1]
5191→5182[ok_1|1]
5191→5191[ok_1|1]
5192→5183[ok_1|1]
5192→5192[ok_1|1]
5193→5184[top_1|1]
125.93/45.58
125.93/45.58
(2) BOUNDS(O(1), O(n^1))
125.93/45.58