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

(0) 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:

active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
proper(g(X)) → g(proper(X))
proper(h(X)) → h(proper(X))
proper(c) → ok(c)
proper(d) → ok(d)
g(ok(X)) → ok(g(X))
h(ok(X)) → ok(h(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST

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

The following defined symbols can occur below the 0th argument of top: proper, active
The following defined symbols can occur below the 0th argument of proper: proper, active
The following defined symbols can occur below the 0th argument of active: proper, active

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
active(g(X)) → mark(h(X))
active(h(d)) → mark(g(c))
proper(g(X)) → g(proper(X))
proper(h(X)) → h(proper(X))

(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:

g(ok(X)) → ok(g(X))
top(ok(X)) → top(active(X))
proper(c) → ok(c)
proper(d) → ok(d)
active(c) → mark(d)
top(mark(X)) → top(proper(X))
h(ok(X)) → ok(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 4.
The certificate found is represented by the following graph.

Start state: 6
Accept states: [7]
Transitions:
6→7[g_1|0, top_1|0, proper_1|0, active_1|0, h_1|0]
6→8[ok_1|1]
6→9[top_1|1]
6→10[top_1|1]
6→11[ok_1|1]
6→12[ok_1|1]
6→13[mark_1|1]
6→14[ok_1|1]
6→15[top_1|2]
6→16[top_1|2]
6→19[top_1|3]
6→20[top_1|3]
6→22[top_1|4]
7→7[ok_1|0, c|0, d|0, mark_1|0]
8→7[g_1|1]
8→8[ok_1|1]
9→7[active_1|1]
9→13[mark_1|1]
10→7[proper_1|1]
10→11[ok_1|1]
10→12[ok_1|1]
11→7[c|1]
12→7[d|1]
13→7[d|1]
14→7[h_1|1]
14→14[ok_1|1]
15→13[proper_1|2]
15→17[ok_1|2]
16→11[active_1|2]
16→12[active_1|2]
16→18[mark_1|2]
17→7[d|2]
18→7[d|2]
19→17[active_1|3]
20→18[proper_1|3]
20→21[ok_1|3]
21→7[d|3]
22→21[active_1|4]

(4) BOUNDS(1, n^1)

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

Converted Cpx (relative) TRS to CDT

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(ok(z0)) → ok(g(z0))
top(ok(z0)) → top(active(z0))
top(mark(z0)) → top(proper(z0))
proper(c) → ok(c)
proper(d) → ok(d)
active(c) → mark(d)
h(ok(z0)) → ok(h(z0))

Tuples:

G(ok(z0)) → c1(G(z0))
TOP(ok(z0)) → c2(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c3(TOP(proper(z0)), PROPER(z0))
PROPER(c) → c4
PROPER(d) → c5
ACTIVE(c) → c6
H(ok(z0)) → c7(H(z0))

S tuples:

G(ok(z0)) → c1(G(z0))
TOP(ok(z0)) → c2(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c3(TOP(proper(z0)), PROPER(z0))
PROPER(c) → c4
PROPER(d) → c5
ACTIVE(c) → c6
H(ok(z0)) → c7(H(z0))

K tuples:none
Defined Rule Symbols:

g, top, proper, active, h

Defined Pair Symbols:

G, TOP, PROPER, ACTIVE, H

Compound Symbols:

c1, c2, c3, c4, c5, c6, c7

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

Removed 3 trailing nodes:

ACTIVE(c) → c6
PROPER(c) → c4
PROPER(d) → c5

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(ok(z0)) → ok(g(z0))
top(ok(z0)) → top(active(z0))
top(mark(z0)) → top(proper(z0))
proper(c) → ok(c)
proper(d) → ok(d)
active(c) → mark(d)
h(ok(z0)) → ok(h(z0))

Tuples:

G(ok(z0)) → c1(G(z0))
TOP(ok(z0)) → c2(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c3(TOP(proper(z0)), PROPER(z0))
H(ok(z0)) → c7(H(z0))

S tuples:

G(ok(z0)) → c1(G(z0))
TOP(ok(z0)) → c2(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c3(TOP(proper(z0)), PROPER(z0))
H(ok(z0)) → c7(H(z0))

K tuples:none
Defined Rule Symbols:

g, top, proper, active, h

Defined Pair Symbols:

G, TOP, H

Compound Symbols:

c1, c2, c3, c7

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

Removed 2 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(ok(z0)) → ok(g(z0))
top(ok(z0)) → top(active(z0))
top(mark(z0)) → top(proper(z0))
proper(c) → ok(c)
proper(d) → ok(d)
active(c) → mark(d)
h(ok(z0)) → ok(h(z0))

Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

S tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

K tuples:none
Defined Rule Symbols:

g, top, proper, active, h

Defined Pair Symbols:

G, H, TOP

Compound Symbols:

c1, c7, c2, c3

(11) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

g(ok(z0)) → ok(g(z0))
top(ok(z0)) → top(active(z0))
top(mark(z0)) → top(proper(z0))
h(ok(z0)) → ok(h(z0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(d)
proper(c) → ok(c)
proper(d) → ok(d)

Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

S tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

K tuples:none
Defined Rule Symbols:

active, proper

Defined Pair Symbols:

G, H, TOP

Compound Symbols:

c1, c7, c2, c3

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

H(ok(z0)) → c7(H(z0))

We considered the (Usable) Rules:

proper(c) → ok(c)
proper(d) → ok(d)
active(c) → mark(d)

And the Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(G(x₁)) = 0   
POL(H(x₁)) = [2]x₁   
POL(TOP(x₁)) = x₁²   
POL(active(x₁)) = [2]   
POL(c) = 0   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(d) = 0   
POL(mark(x₁)) = [2] + x₁   
POL(ok(x₁)) = [2] + x₁   
POL(proper(x₁)) = [2]   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(d)
proper(c) → ok(c)
proper(d) → ok(d)

Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

S tuples:

G(ok(z0)) → c1(G(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

K tuples:

H(ok(z0)) → c7(H(z0))

Defined Rule Symbols:

active, proper

Defined Pair Symbols:

G, H, TOP

Compound Symbols:

c1, c7, c2, c3

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G(ok(z0)) → c1(G(z0))

We considered the (Usable) Rules:none
And the Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(G(x₁)) = x₁   
POL(H(x₁)) = 0   
POL(TOP(x₁)) = 0   
POL(active(x₁)) = 0   
POL(c) = 0   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(d) = 0   
POL(mark(x₁)) = 0   
POL(ok(x₁)) = [1] + x₁   
POL(proper(x₁)) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(d)
proper(c) → ok(c)
proper(d) → ok(d)

Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

S tuples:

TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

K tuples:

H(ok(z0)) → c7(H(z0))
G(ok(z0)) → c1(G(z0))

Defined Rule Symbols:

active, proper

Defined Pair Symbols:

G, H, TOP

Compound Symbols:

c1, c7, c2, c3

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TOP(mark(z0)) → c3(TOP(proper(z0)))

We considered the (Usable) Rules:

proper(c) → ok(c)
proper(d) → ok(d)
active(c) → mark(d)

And the Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(G(x₁)) = 0   
POL(H(x₁)) = [2]x₁²   
POL(TOP(x₁)) = [2]x₁   
POL(active(x₁)) = x₁   
POL(c) = [1]   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(d) = 0   
POL(mark(x₁)) = [1] + x₁   
POL(ok(x₁)) = x₁   
POL(proper(x₁)) = x₁   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(d)
proper(c) → ok(c)
proper(d) → ok(d)

Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

S tuples:

TOP(ok(z0)) → c2(TOP(active(z0)))

K tuples:

H(ok(z0)) → c7(H(z0))
G(ok(z0)) → c1(G(z0))
TOP(mark(z0)) → c3(TOP(proper(z0)))

Defined Rule Symbols:

active, proper

Defined Pair Symbols:

G, H, TOP

Compound Symbols:

c1, c7, c2, c3

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TOP(ok(z0)) → c2(TOP(active(z0)))

We considered the (Usable) Rules:

proper(c) → ok(c)
proper(d) → ok(d)
active(c) → mark(d)

And the Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(G(x₁)) = [2]x₁   
POL(H(x₁)) = 0   
POL(TOP(x₁)) = [2]x₁   
POL(active(x₁)) = x₁   
POL(c) = [1]   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(d) = 0   
POL(mark(x₁)) = [1] + x₁   
POL(ok(x₁)) = [1] + x₁   
POL(proper(x₁)) = [1] + x₁   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(d)
proper(c) → ok(c)
proper(d) → ok(d)

Tuples:

G(ok(z0)) → c1(G(z0))
H(ok(z0)) → c7(H(z0))
TOP(ok(z0)) → c2(TOP(active(z0)))
TOP(mark(z0)) → c3(TOP(proper(z0)))

S tuples:none
K tuples:

H(ok(z0)) → c7(H(z0))
G(ok(z0)) → c1(G(z0))
TOP(mark(z0)) → c3(TOP(proper(z0)))
TOP(ok(z0)) → c2(TOP(active(z0)))

Defined Rule Symbols:

active, proper

Defined Pair Symbols:

G, H, TOP

Compound Symbols:

c1, c7, c2, c3

(21) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(22) BOUNDS(1, 1)