Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Glenstrup/deeprev_typed)

The rewrite relation of the following TRS is considered.

revconsapp(C(x1,x2),r)	→	revconsapp(x2,C(x1,r))	(1)
deeprevapp(C(x1,x2),rest)	→	deeprevapp(x2,C(x1,rest))	(2)
deeprevapp(V(n),rest)	→	revconsapp(rest,V(n))	(3)
deeprevapp(N,rest)	→	rest	(4)
revconsapp(V(n),r)	→	r	(5)
revconsapp(N,r)	→	r	(6)
deeprev(C(x1,x2))	→	deeprevapp(C(x1,x2),N)	(7)
deeprev(V(n))	→	V(n)	(8)
deeprev(N)	→	N	(9)
second(V(n))	→	N	(10)
second(C(x1,x2))	→	x2	(11)
isVal(C(x1,x2))	→	False	(12)
isVal(V(n))	→	True	(13)
isVal(N)	→	False	(14)
isNotEmptyT(C(x1,x2))	→	True	(15)
isNotEmptyT(V(n))	→	False	(16)
isNotEmptyT(N)	→	False	(17)
isEmptyT(C(x1,x2))	→	False	(18)
isEmptyT(V(n))	→	False	(19)
isEmptyT(N)	→	True	(20)
first(V(n))	→	N	(21)
first(C(x1,x2))	→	x1	(22)
goal(x)	→	deeprev(x)	(23)

The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n).

Proof (by AProVE @ termCOMP 2023)

1 Bounds

The given TRS is match-(raise)-bounded by 3. This is shown by the following automaton.

final states:

{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}

transitions:

C₀(0,0)	→	0
V₀(0)	→	0
N₀	→	0
False₀	→	0
True₀	→	0
revconsapp₀(0,0)	→	1
deeprevapp₀(0,0)	→	2
deeprev₀(0)	→	3
second₀(0)	→	4
isVal₀(0)	→	5
isNotEmptyT₀(0)	→	6
isEmptyT₀(0)	→	7
first₀(0)	→	8
goal₀(0)	→	9
C₁(0,0)	→	10
revconsapp₁(0,10)	→	1
C₁(0,0)	→	11
deeprevapp₁(0,11)	→	2
V₁(0)	→	12
revconsapp₁(0,12)	→	2
C₁(0,0)	→	13
N₁	→	14
deeprevapp₁(13,14)	→	3
V₁(0)	→	3
N₁	→	3
N₁	→	4
False₁	→	5
True₁	→	5
True₁	→	6
False₁	→	6
False₁	→	7
True₁	→	7
N₁	→	8
deeprev₁(0)	→	9
C₁(0,10)	→	10
C₁(0,12)	→	10
revconsapp₁(0,10)	→	2
C₁(0,11)	→	11
C₂(0,14)	→	15
deeprevapp₂(0,15)	→	3
revconsapp₁(11,12)	→	2
deeprevapp₁(13,14)	→	9
V₁(0)	→	9
N₁	→	9
C₂(0,12)	→	16
revconsapp₂(0,16)	→	2
revconsapp₂(11,16)	→	2
deeprevapp₂(0,15)	→	9
C₁(0,15)	→	11
deeprevapp₁(0,11)	→	3
revconsapp₁(15,12)	→	3
revconsapp₂(15,16)	→	2
revconsapp₁(11,12)	→	3
revconsapp₂(14,16)	→	3
deeprevapp₁(0,11)	→	9
revconsapp₁(15,12)	→	9
C₁(0,16)	→	10
C₂(0,16)	→	16
revconsapp₂(0,16)	→	3
revconsapp₂(11,16)	→	3
revconsapp₂(15,16)	→	3
revconsapp₁(11,12)	→	9
revconsapp₂(14,16)	→	9
C₃(0,16)	→	17
revconsapp₃(14,17)	→	2
revconsapp₂(0,16)	→	9
revconsapp₂(11,16)	→	9
revconsapp₂(15,16)	→	9
revconsapp₁(0,10)	→	3
revconsapp₃(14,17)	→	3
revconsapp₁(0,10)	→	9
revconsapp₃(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