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) |
final states:
{0, 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 |