(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r))
deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest))
deeprevapp(V(n), rest) → revconsapp(rest, V(n))
deeprevapp(N, rest) → rest
revconsapp(V(n), r) → r
revconsapp(N, r) → r
deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N)
deeprev(V(n)) → V(n)
deeprev(N) → N
second(V(n)) → N
second(C(x1, x2)) → x2
isVal(C(x1, x2)) → False
isVal(V(n)) → True
isVal(N) → False
isNotEmptyT(C(x1, x2)) → True
isNotEmptyT(V(n)) → False
isNotEmptyT(N) → False
isEmptyT(C(x1, x2)) → False
isEmptyT(V(n)) → False
isEmptyT(N) → True
first(V(n)) → N
first(C(x1, x2)) → x1
goal(x) → deeprev(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, 4, 5, 6, 7, 8, 9]
transitions:
C0(0, 0) → 0
V0(0) → 0
N0() → 0
False0() → 0
True0() → 0
revconsapp0(0, 0) → 1
deeprevapp0(0, 0) → 2
deeprev0(0) → 3
second0(0) → 4
isVal0(0) → 5
isNotEmptyT0(0) → 6
isEmptyT0(0) → 7
first0(0) → 8
goal0(0) → 9
C1(0, 0) → 10
revconsapp1(0, 10) → 1
C1(0, 0) → 11
deeprevapp1(0, 11) → 2
V1(0) → 12
revconsapp1(0, 12) → 2
C1(0, 0) → 13
N1() → 14
deeprevapp1(13, 14) → 3
V1(0) → 3
N1() → 3
N1() → 4
False1() → 5
True1() → 5
True1() → 6
False1() → 6
False1() → 7
True1() → 7
N1() → 8
deeprev1(0) → 9
C1(0, 10) → 10
C1(0, 12) → 10
revconsapp1(0, 10) → 2
C1(0, 11) → 11
C2(0, 14) → 15
deeprevapp2(0, 15) → 3
revconsapp1(11, 12) → 2
deeprevapp1(13, 14) → 9
V1(0) → 9
N1() → 9
C2(0, 12) → 16
revconsapp2(0, 16) → 2
revconsapp2(11, 16) → 2
deeprevapp2(0, 15) → 9
C1(0, 15) → 11
deeprevapp1(0, 11) → 3
revconsapp1(15, 12) → 3
revconsapp2(15, 16) → 2
revconsapp1(11, 12) → 3
revconsapp2(14, 16) → 3
deeprevapp1(0, 11) → 9
revconsapp1(15, 12) → 9
C1(0, 16) → 10
C2(0, 16) → 16
revconsapp2(0, 16) → 3
revconsapp2(11, 16) → 3
revconsapp2(15, 16) → 3
revconsapp1(11, 12) → 9
revconsapp2(14, 16) → 9
C3(0, 16) → 17
revconsapp3(14, 17) → 2
revconsapp2(0, 16) → 9
revconsapp2(11, 16) → 9
revconsapp2(15, 16) → 9
revconsapp1(0, 10) → 3
revconsapp3(14, 17) → 3
revconsapp1(0, 10) → 9
revconsapp3(14, 17) → 9
0 → 2
0 → 1
0 → 4
0 → 8
11 → 2
11 → 3
11 → 9
10 → 1
10 → 2
10 → 3
10 → 9
12 → 2
15 → 3
15 → 9
16 → 2
16 → 3
16 → 9
17 → 2
17 → 3
17 → 9
(2) BOUNDS(1, n^1)