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

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 2 ms)
    ↳4 CdtProblem
    ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
↳15 CpxTrsMatchBoundsProof (⇔, 0 ms)
↳16 BOUNDS(O(1), O(n^1))

(0) Obligation:

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

h(f(f(x))) → h(f(g(f(x))))
f(g(f(x))) → f(f(x))

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(f(f(z0))) → h(f(g(f(z0))))
f(g(f(z0))) → f(f(z0))
Tuples:

H(f(f(z0))) → c(H(f(g(f(z0)))), F(g(f(z0))), F(z0))
F(g(f(z0))) → c1(F(f(z0)), F(z0))
S tuples:

H(f(f(z0))) → c(H(f(g(f(z0)))), F(g(f(z0))), F(z0))
F(g(f(z0))) → c1(F(f(z0)), F(z0))
K tuples:none
Defined Rule Symbols:

h, f

Defined Pair Symbols:

H, F

Compound Symbols:

c, c1

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace H(f(f(z0))) → c(H(f(g(f(z0)))), F(g(f(z0))), F(z0)) by

H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
H(f(f(x0))) → c

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(f(f(z0))) → h(f(g(f(z0))))
f(g(f(z0))) → f(f(z0))
Tuples:

F(g(f(z0))) → c1(F(f(z0)), F(z0))
H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
H(f(f(x0))) → c
S tuples:

F(g(f(z0))) → c1(F(f(z0)), F(z0))
H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
H(f(f(x0))) → c
K tuples:none
Defined Rule Symbols:

h, f

Defined Pair Symbols:

F, H

Compound Symbols:

c1, c, c

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

H(f(f(x0))) → c

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(f(f(z0))) → h(f(g(f(z0))))
f(g(f(z0))) → f(f(z0))
Tuples:

F(g(f(z0))) → c1(F(f(z0)), F(z0))
H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
S tuples:

F(g(f(z0))) → c1(F(f(z0)), F(z0))
H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
K tuples:none
Defined Rule Symbols:

h, f

Defined Pair Symbols:

F, H

Compound Symbols:

c1, c

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(g(f(z0))) → c1(F(f(z0)), F(z0)) by

F(g(f(x0))) → c1(F(x0))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(f(f(z0))) → h(f(g(f(z0))))
f(g(f(z0))) → f(f(z0))
Tuples:

H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
F(g(f(x0))) → c1(F(x0))
S tuples:

H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
F(g(f(x0))) → c1(F(x0))
K tuples:none
Defined Rule Symbols:

h, f

Defined Pair Symbols:

H, F

Compound Symbols:

c, c1

(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(g(f(x0))) → c1(F(x0)) by

F(g(f(g(f(y0))))) → c1(F(g(f(y0))))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(f(f(z0))) → h(f(g(f(z0))))
f(g(f(z0))) → f(f(z0))
Tuples:

H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
F(g(f(g(f(y0))))) → c1(F(g(f(y0))))
S tuples:

H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
F(g(f(g(f(y0))))) → c1(F(g(f(y0))))
K tuples:none
Defined Rule Symbols:

h, f

Defined Pair Symbols:

H, F

Compound Symbols:

c, c1

(11) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(g(f(g(f(y0))))) → c1(F(g(f(y0))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(f(f(z0))) → h(f(g(f(z0))))
f(g(f(z0))) → f(f(z0))
Tuples:

H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
S tuples:

H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0))
K tuples:none
Defined Rule Symbols:

h, f

Defined Pair Symbols:

H

Compound Symbols:

c

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace H(f(f(z0))) → c(H(f(f(z0))), F(g(f(z0))), F(z0)) by

H(f(f(x0))) → c(H(f(f(x0))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(f(f(z0))) → h(f(g(f(z0))))
f(g(f(z0))) → f(f(z0))
Tuples:

H(f(f(x0))) → c(H(f(f(x0))))
S tuples:

H(f(f(x0))) → c(H(f(f(x0))))
K tuples:none
Defined Rule Symbols:

h, f

Defined Pair Symbols:

H

Compound Symbols:

c

(15) 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 0.
The certificate found is represented by the following graph.
Start state: 198
Accept states: [199, 200]
Transitions:
198→199[h_1|0]
198→200[f_1|0]
198→198[g_1|0]

(16) BOUNDS(O(1), O(n^1))