(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(f(x)) → mark(f(f(x)))
chk(no(f(x))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
mat(f(x), f(y)) → f(mat(x, y))
chk(no(c)) → active(c)
mat(f(x), c) → no(c)
f(active(x)) → active(f(x))
f(no(x)) → no(f(x))
f(mark(x)) → mark(f(x))
tp(mark(x)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
Rewrite Strategy: INNERMOST
(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)
The following defined symbols can occur below the 0th argument of f: chk, f, mat
The following defined symbols can occur below the 0th argument of tp: chk, f, mat
The following defined symbols can occur below the 0th argument of chk: chk, f, mat
The following defined symbols can occur below the 0th argument of mat: chk, f, mat
The following defined symbols can occur below the 1th argument of mat: chk, f, mat
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
active(f(x)) → mark(f(f(x)))
f(active(x)) → active(f(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:
mat(f(x), f(y)) → f(mat(x, y))
tp(mark(x)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) → active(c)
f(no(x)) → no(f(x))
chk(no(f(x))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
f(mark(x)) → mark(f(x))
mat(f(x), c) → no(c)
Rewrite Strategy: INNERMOST
(3) 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 2.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4]
transitions:
y0() → 0
mark0(0) → 0
X0() → 0
no0(0) → 0
c0() → 0
active0(0) → 0
mat0(0, 0) → 1
tp0(0) → 2
chk0(0) → 3
f0(0) → 4
X1() → 10
f1(10) → 9
f1(9) → 8
f1(8) → 8
f1(8) → 7
mat1(7, 0) → 6
chk1(6) → 5
tp1(5) → 2
c1() → 11
active1(11) → 3
f1(0) → 12
no1(12) → 4
f1(0) → 13
mark1(13) → 4
no1(12) → 12
no1(12) → 13
mark1(13) → 12
mark1(13) → 13
c1() → 14
no1(14) → 6
c2() → 15
active2(15) → 5
(4) BOUNDS(1, n^1)