KILLED



    


Runtime Complexity (innermost) proof of /tmp/tmpM6NuYv/Ex6_GM04_C.xml


(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST

(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: 1
Accept states: [2]
Transitions:
1→2[active_1|0, proper_1|0, f_1|0, g_1|0, top_1|0]
1→3[mark_1|1]
1→6[ok_1|1]
1→7[ok_1|1]
1→8[ok_1|1]
1→9[top_1|1]
1→10[top_1|1]
1→11[top_1|2]
1→12[top_1|2]
1→17[top_1|3]
1→25[top_1|3]
1→29[top_1|4]
1→30[top_1|4]
1→33[top_1|5]
1→35[top_1|5]
1→38[top_1|6]
2→2[c|0, mark_1|0, ok_1|0]
3→4[f_1|1]
4→5[g_1|1]
5→2[c|1]
6→2[c|1]
7→2[f_1|1]
7→7[ok_1|1]
8→2[g_1|1]
8→8[ok_1|1]
9→2[proper_1|1]
9→6[ok_1|1]
10→2[active_1|1]
10→3[mark_1|1]
11→6[active_1|2]
11→13[mark_1|2]
12→3[proper_1|2]
12→16[f_1|2]
12→23[ok_1|3]
13→14[f_1|2]
14→15[g_1|2]
15→2[c|2]
16→4[proper_1|2]
16→18[g_1|2]
16→21[ok_1|3]
17→13[proper_1|3]
17→19[f_1|3]
17→27[ok_1|4]
18→5[proper_1|2]
18→20[ok_1|2]
19→14[proper_1|3]
19→22[g_1|3]
19→26[ok_1|4]
20→2[c|2]
21→20[g_1|3]
22→15[proper_1|3]
22→24[ok_1|3]
23→21[f_1|3]
24→2[c|3]
25→23[active_1|3]
25→28[mark_1|4]
26→24[g_1|4]
27→26[f_1|4]
28→20[g_1|4]
29→27[active_1|4]
29→31[mark_1|5]
30→28[proper_1|4]
30→32[g_1|5]
30→26[ok_1|4]
31→24[g_1|5]
32→20[proper_1|5]
32→24[ok_1|3]
33→31[proper_1|5]
33→34[g_1|6]
33→37[ok_1|5]
34→24[proper_1|6]
34→36[ok_1|4]
35→26[active_1|5]
36→2[c|4]
37→36[g_1|5]
38→37[active_1|6]

(2) BOUNDS(1, n^1)