131.81/45.54
131.81/45.54
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(f(f(a))) → mark(c(f(g(f(a)))))
131.81/45.54
active(f(X)) → f(active(X))
131.81/45.54
active(g(X)) → g(active(X))
131.81/45.54
f(mark(X)) → mark(f(X))
131.81/45.54
g(mark(X)) → mark(g(X))
131.81/45.54
proper(f(X)) → f(proper(X))
131.81/45.54
proper(a) → ok(a)
131.81/45.54
proper(c(X)) → c(proper(X))
131.81/45.54
proper(g(X)) → g(proper(X))
131.81/45.54
f(ok(X)) → ok(f(X))
131.81/45.54
c(ok(X)) → ok(c(X))
131.81/45.54
g(ok(X)) → ok(g(X))
131.81/45.54
top(mark(X)) → top(proper(X))
131.81/45.54
top(ok(X)) → top(active(X))
Rewrite Strategy: INNERMOST
131.81/45.54
131.81/45.54
(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 2.
The certificate found is represented by the following graph.
Start state: 3460
Accept states: [3461, 3462, 3463, 3464, 3465, 3466]
Transitions:
3460→3461[active_1|0]
3460→3462[f_1|0]
3460→3463[g_1|0]
3460→3464[proper_1|0]
3460→3465[c_1|0]
3460→3466[top_1|0]
3460→3460[a|0, mark_1|0, ok_1|0]
3460→3467[a|1]
3460→3468[f_1|1]
3460→3469[g_1|1]
3460→3470[proper_1|1]
3460→3471[f_1|1]
3460→3472[g_1|1]
3460→3473[c_1|1]
3460→3474[active_1|1]
3467→3464[ok_1|1]
3467→3470[ok_1|1]
3467→3475[active_1|2]
3468→3462[mark_1|1]
3468→3468[mark_1|1]
3468→3471[mark_1|1]
3469→3463[mark_1|1]
3469→3469[mark_1|1]
3469→3472[mark_1|1]
3470→3466[top_1|1]
3471→3462[ok_1|1]
3471→3468[ok_1|1]
3471→3471[ok_1|1]
3472→3463[ok_1|1]
3472→3469[ok_1|1]
3472→3472[ok_1|1]
3473→3465[ok_1|1]
3473→3473[ok_1|1]
3474→3466[top_1|1]
3475→3466[top_1|2]
131.81/45.54
131.81/45.54
(2) BOUNDS(O(1), O(n^1))
131.81/45.54