WORST_CASE(?,O(n^1))
proof of input_OuD99ELDL3.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(2) CpxTRS
(3) CpxTrsMatchBoundsProof [FINISHED, 0 ms]
(4) BOUNDS(1, n^1)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-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)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(2)
Obligation:
The Runtime Complexity (parallel-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)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsMatchBoundsProof (FINISHED)
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.

"[12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23]
{(12,13,[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]), (12,14,[a__c_1|1, d_1|2, c_1|2]), (12,17,[a__c_1|1, d_1|2, c_1|2]), (12,18,[a__f_1|1, f_1|2]), (12,19,[a__h_1|1, h_1|2]), (12,20,[a__c_1|2, d_1|3, c_1|3]), (12,21,[a__c_1|2, d_1|3, c_1|3]), (13,13,[f_1|0, g_1|0, d_1|0, c_1|0, h_1|0]), (14,15,[f_1|1]), (15,16,[g_1|1]), (16,13,[f_1|1]), (17,13,[d_1|1]), (18,13,[mark_1|1, a__c_1|1, g_1|1, d_1|1, d_1|2, c_1|2]), (18,18,[a__f_1|1, f_1|2]), (18,19,[a__h_1|1, h_1|2]), (18,20,[a__c_1|2, d_1|3, c_1|3]), (18,21,[a__c_1|2, d_1|3, c_1|3]), (19,13,[mark_1|1, a__c_1|1, g_1|1, d_1|1, d_1|2, c_1|2]), (19,18,[a__f_1|1, f_1|2]), (19,19,[a__h_1|1, h_1|2]), (19,20,[a__c_1|2, d_1|3, c_1|3]), (19,21,[a__c_1|2, d_1|3, c_1|3]), (20,19,[d_1|2]), (21,22,[f_1|2]), (22,23,[g_1|2]), (23,18,[f_1|2])}"
----------------------------------------

(4)
BOUNDS(1, n^1)