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:

f(X) → if(X, c, n__f(true))
if(true, X, Y) → X
if(false, X, Y) → activate(Y)
f(X) → n__f(X)
activate(n__f(X)) → f(X)
activate(X) → X

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 3.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3]
transitions:
c0() → 0
n__f0(0) → 0
true0() → 0
false0() → 0
f0(0) → 1
if0(0, 0, 0) → 2
activate0(0) → 3
c1() → 4
true1() → 6
n__f1(6) → 5
if1(0, 4, 5) → 1
activate1(0) → 2
n__f1(0) → 1
f1(0) → 3
c2() → 7
true2() → 9
n__f2(9) → 8
if2(0, 7, 8) → 3
activate1(5) → 1
n__f2(0) → 3
f1(0) → 2
if2(0, 7, 8) → 2
n__f2(0) → 2
f2(6) → 1
activate1(8) → 3
activate1(8) → 2
f2(9) → 3
c3() → 10
true3() → 12
n__f3(12) → 11
if3(6, 10, 11) → 1
n__f3(6) → 1
f2(9) → 2
if3(9, 10, 11) → 3
n__f3(9) → 3
if3(9, 10, 11) → 2
n__f3(9) → 2
0 → 2
0 → 3
4 → 1
5 → 1
7 → 3
7 → 2
8 → 3
8 → 2
10 → 1
10 → 3
10 → 2

(2) BOUNDS(1, n^1)

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(true))
f(z0) → n__f(z0)
if(true, z0, z1) → z0
if(false, z0, z1) → activate(z1)
activate(n__f(z0)) → f(z0)
activate(z0) → z0

Tuples:

F(z0) → c1(IF(z0, c, n__f(true)))
F(z0) → c2
IF(true, z0, z1) → c3
IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))
ACTIVATE(z0) → c6

S tuples:

F(z0) → c1(IF(z0, c, n__f(true)))
F(z0) → c2
IF(true, z0, z1) → c3
IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))
ACTIVATE(z0) → c6

K tuples:none
Defined Rule Symbols:

f, if, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c2, c3, c4, c5, c6

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

Removed 3 trailing nodes:

F(z0) → c2
IF(true, z0, z1) → c3
ACTIVATE(z0) → c6

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(true))
f(z0) → n__f(z0)
if(true, z0, z1) → z0
if(false, z0, z1) → activate(z1)
activate(n__f(z0)) → f(z0)
activate(z0) → z0

Tuples:

F(z0) → c1(IF(z0, c, n__f(true)))
IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))

S tuples:

F(z0) → c1(IF(z0, c, n__f(true)))
IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))

K tuples:none
Defined Rule Symbols:

f, if, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c5

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

f(z0) → if(z0, c, n__f(true))
f(z0) → n__f(z0)
if(true, z0, z1) → z0
if(false, z0, z1) → activate(z1)
activate(n__f(z0)) → f(z0)
activate(z0) → z0

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(z0) → c1(IF(z0, c, n__f(true)))
IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))

S tuples:

F(z0) → c1(IF(z0, c, n__f(true)))
IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))

K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c5

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

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

IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))

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

F(z0) → c1(IF(z0, c, n__f(true)))
IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))

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

POL(ACTIVATE(x₁)) = [3] + [3]x₁   
POL(F(x₁)) = [3]x₁   
POL(IF(x₁, x₂, x₃)) = [2]x₁ + [3]x₃   
POL(c) = 0   
POL(c1(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(false) = [2]   
POL(n__f(x₁)) = x₁   
POL(true) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(z0) → c1(IF(z0, c, n__f(true)))
IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))

S tuples:

F(z0) → c1(IF(z0, c, n__f(true)))

K tuples:

IF(false, z0, z1) → c4(ACTIVATE(z1))
ACTIVATE(n__f(z0)) → c5(F(z0))

Defined Rule Symbols:none

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c5

(11) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F(z0) → c1(IF(z0, c, n__f(true)))
IF(false, z0, z1) → c4(ACTIVATE(z1))

Now S is empty

(12) BOUNDS(1, 1)