The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

a__f(f(X)) → a__c(f(g(f(X))))
a__c(X) → d(X)
a__h(X) → a__c(d(X))
mark(f(X)) → a__f(mark(X))
mark(c(X)) → a__c(X)
mark(h(X)) → a__h(mark(X))
mark(g(X)) → g(X)
mark(d(X)) → d(X)
a__f(X) → f(X)
a__c(X) → c(X)
a__h(X) → h(X)

Rewrite Strategy: FULL

(1) RcToIrcProof (BOTH BOUNDS(ID, ID) transformation)

Converted rc-obligation to irc-obligation.

As the TRS is a non-duplicating overlay system, we have rc = irc.

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

a__f(f(X)) → a__c(f(g(f(X))))
a__c(X) → d(X)
a__h(X) → a__c(d(X))
mark(f(X)) → a__f(mark(X))
mark(c(X)) → a__c(X)
mark(h(X)) → a__h(mark(X))
mark(g(X)) → g(X)
mark(d(X)) → d(X)
a__f(X) → f(X)
a__c(X) → c(X)
a__h(X) → h(X)

Rewrite Strategy: INNERMOST

(3) 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 3.
The certificate found is represented by the following graph.

Start state: 5
Accept states: [6]
Transitions:
5→6[a__f_1|0, a__c_1|0, a__h_1|0, mark_1|0, f_1|1, d_1|1, c_1|1, h_1|1, a__c_1|1, g_1|1, d_1|2, c_1|2]
5→7[a__c_1|1, d_1|2, c_1|2]
5→10[a__c_1|1, d_1|2, c_1|2]
5→11[a__f_1|1, f_1|2]
5→12[a__h_1|1, h_1|2]
5→13[a__c_1|2, d_1|3, c_1|3]
5→14[a__c_1|2, d_1|3, c_1|3]
6→6[f_1|0, g_1|0, d_1|0, c_1|0, h_1|0]
7→8[f_1|1]
8→9[g_1|1]
9→6[f_1|1]
10→6[d_1|1]
11→6[mark_1|1, a__c_1|1, g_1|1, d_1|1, d_1|2, c_1|2]
11→11[a__f_1|1, f_1|2]
11→12[a__h_1|1, h_1|2]
11→13[a__c_1|2, d_1|3, c_1|3]
11→14[a__c_1|2, d_1|3, c_1|3]
12→6[mark_1|1, a__c_1|1, g_1|1, d_1|1, d_1|2, c_1|2]
12→11[a__f_1|1, f_1|2]
12→12[a__h_1|1, h_1|2]
12→13[a__c_1|2, d_1|3, c_1|3]
12→14[a__c_1|2, d_1|3, c_1|3]
13→12[d_1|2]
14→15[f_1|2]
15→16[g_1|2]
16→11[f_1|2]

(4) BOUNDS(1, n^1)