127.68/45.54
127.68/45.54
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
127.68/45.54
active(f(g(X))) → mark(g(X))
127.68/45.54
proper(c) → ok(c)
127.68/45.54
proper(f(X)) → f(proper(X))
127.68/45.54
proper(g(X)) → g(proper(X))
127.68/45.54
f(ok(X)) → ok(f(X))
127.68/45.54
g(ok(X)) → ok(g(X))
127.68/45.54
top(mark(X)) → top(proper(X))
127.68/45.54
top(ok(X)) → top(active(X))
Rewrite Strategy: INNERMOST
127.68/45.54
127.68/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 6.
The certificate found is represented by the following graph.
Start state: 2934
Accept states: [2935, 2936, 2937, 2938, 2939]
Transitions:
2934→2935[active_1|0]
2934→2936[proper_1|0]
2934→2937[f_1|0]
2934→2938[g_1|0]
2934→2939[top_1|0]
2934→2934[c|0, mark_1|0, ok_1|0]
2934→2940[c|1]
2934→2943[c|1]
2934→2944[f_1|1]
2934→2945[g_1|1]
2934→2946[active_1|1]
2934→2947[proper_1|1]
2934→2950[c|2]
2934→2956[c|2]
2934→2960[c|3]
2934→2972[c|4]
2940→2941[g_1|1]
2940→2954[proper_1|2]
2941→2942[f_1|1]
2941→2953[proper_1|2]
2942→2935[mark_1|1]
2942→2946[mark_1|1]
2942→2948[proper_1|2]
2943→2936[ok_1|1]
2943→2947[ok_1|1]
2943→2949[active_1|2]
2944→2937[ok_1|1]
2944→2944[ok_1|1]
2945→2938[ok_1|1]
2945→2945[ok_1|1]
2946→2939[top_1|1]
2947→2939[top_1|1]
2948→2939[top_1|2]
2949→2939[top_1|2]
2950→2951[g_1|2]
2950→2958[proper_1|3]
2951→2952[f_1|2]
2951→2957[proper_1|3]
2952→2949[mark_1|2]
2952→2955[proper_1|3]
2953→2948[f_1|2]
2954→2953[g_1|2]
2955→2939[top_1|3]
2956→2954[ok_1|2]
2956→2959[g_1|3]
2956→2964[g_1|4]
2956→2968[proper_1|5]
2957→2955[f_1|3]
2958→2957[g_1|3]
2959→2953[ok_1|3]
2959→2961[f_1|3]
2960→2958[ok_1|3]
2960→2962[g_1|4]
2960→2969[g_1|5]
2960→2968[ok_1|3]
2960→2971[proper_1|6]
2961→2948[ok_1|3]
2961→2963[active_1|3]
2962→2957[ok_1|4]
2962→2965[f_1|4]
2962→2966[ok_1|4]
2962→2973[active_1|5]
2963→2939[top_1|3]
2964→2963[mark_1|4]
2964→2966[proper_1|4]
2965→2955[ok_1|4]
2965→2967[active_1|4]
2966→2939[top_1|4]
2967→2939[top_1|4]
2968→2966[g_1|5]
2969→2967[mark_1|5]
2969→2970[proper_1|5]
2970→2939[top_1|5]
2971→2970[g_1|6]
2972→2971[ok_1|4]
2972→2974[g_1|5]
2973→2939[top_1|5]
2974→2970[ok_1|5]
2974→2975[active_1|6]
2975→2939[top_1|6]
127.68/45.54
127.68/45.54
(2) BOUNDS(O(1), O(n^1))
127.68/45.54