Certification Problem

Input (TPDB TRS_Standard/Applicative_05/Ex9Maps)

The rewrite relation of the following TRS is considered.

app(app(map_1,f),app(app(cons,h),t)) → app(app(cons,app(f,h)),app(app(map_1,f),t)) (1)
app(app(app(map_2,f),c),app(app(cons,h),t)) → app(app(cons,app(app(f,h),c)),app(app(app(map_2,f),c),t)) (2)
app(app(app(app(map_3,f),g),c),app(app(cons,h),t)) → app(app(cons,app(app(app(f,g),h),c)),app(app(app(app(map_3,f),g),c),t)) (3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Uncurrying

We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.

map_1 is mapped to map_1, map_11(x1), map_12(x1, x2)
cons is mapped to cons, cons1(x1), cons2(x1, x2)
map_2 is mapped to map_2, map_21(x1), map_22(x1, x2), map_23(x1, x2, x3)
map_3 is mapped to map_3, map_31(x1), map_32(x1, x2), map_33(x1, x2, x3), map_34(x1,...,x4)
g is mapped to g


There are no uncurry rules.
No rules have to be added for the eta-expansion.

Uncurrying the rules and adding the uncurrying rules yields the new set of rules
map_12(f,cons2(h,t)) → cons2(app(f,h),map_12(f,t)) (15)
map_23(f,c,cons2(h,t)) → cons2(app(app(f,h),c),map_23(f,c,t)) (16)
map_34(f,g,c,cons2(h,t)) → cons2(app(app(app(f,g),h),c),map_34(f,g,c,t)) (17)
app(map_1,y1) → map_11(y1) (4)
app(map_11(x0),y1) → map_12(x0,y1) (5)
app(cons,y1) → cons1(y1) (6)
app(cons1(x0),y1) → cons2(x0,y1) (7)
app(map_2,y1) → map_21(y1) (8)
app(map_21(x0),y1) → map_22(x0,y1) (9)
app(map_22(x0,x1),y1) → map_23(x0,x1,y1) (10)
app(map_3,y1) → map_31(y1) (11)
app(map_31(x0),y1) → map_32(x0,y1) (12)
app(map_32(x0,x1),y1) → map_33(x0,x1,y1) (13)
app(map_33(x0,x1,x2),y1) → map_34(x0,x1,x2,y1) (14)

1.1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
map_12#(f,cons2(h,t)) → app#(f,h) (18)
map_12#(f,cons2(h,t)) → map_12#(f,t) (19)
map_23#(f,c,cons2(h,t)) → app#(app(f,h),c) (20)
map_23#(f,c,cons2(h,t)) → app#(f,h) (21)
map_23#(f,c,cons2(h,t)) → map_23#(f,c,t) (22)
map_34#(f,g,c,cons2(h,t)) → app#(app(app(f,g),h),c) (23)
map_34#(f,g,c,cons2(h,t)) → app#(app(f,g),h) (24)
map_34#(f,g,c,cons2(h,t)) → app#(f,g) (25)
map_34#(f,g,c,cons2(h,t)) → map_34#(f,g,c,t) (26)
app#(map_11(x0),y1) → map_12#(x0,y1) (27)
app#(map_22(x0,x1),y1) → map_23#(x0,x1,y1) (28)
app#(map_33(x0,x1,x2),y1) → map_34#(x0,x1,x2,y1) (29)

1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[map_12#(x1, x2)] =
0
+
0
· x1 +
1
· x2
[cons2(x1, x2)] =
1
+
0
· x1 +
0
· x2
[app#(x1, x2)] =
0
+
0
· x1 +
1
· x2
[map_23#(x1, x2, x3)] =
0
+
0
· x1 +
1
· x2 +
1
· x3
[app(x1, x2)] =
1
+
0
· x1 +
1
· x2
[map_34#(x1,...,x4)] =
-∞
+
1
· x1 +
-∞
· x2 +
1
· x3 +
1
· x4
[g] =
0
[map_11(x1)] =
-∞
+
0
· x1
[map_22(x1, x2)] =
-∞
+
0
· x1 +
1
· x2
[map_33(x1, x2, x3)] =
-∞
+
1
· x1 +
0
· x2 +
1
· x3
[map_1] =
0
[map_12(x1, x2)] =
-∞
+
0
· x1 +
1
· x2
[cons] =
2
[cons1(x1)] =
0
+
1
· x1
[map_2] =
0
[map_21(x1)] =
-∞
+
0
· x1
[map_23(x1, x2, x3)] =
0
+
0
· x1 +
1
· x2 +
1
· x3
[map_3] =
0
[map_31(x1)] =
-∞
+
1
· x1
[map_32(x1, x2)] =
-∞
+
1
· x1 +
1
· x2
[map_34(x1,...,x4)] =
0
+
0
· x1 +
0
· x2 +
1
· x3 +
1
· x4
the pair
map_34#(f,g,c,cons2(h,t)) → app#(f,g) (25)
could be deleted.

1.1.1.1.1 Narrowing Processor

We consider all narrowings of the pair below position 1 to get the following set of pairs
map_23#(map_1,y1,cons2(x0,y3)) → app#(map_11(x0),y1) (30)
map_23#(map_11(x0),y1,cons2(x1,y3)) → app#(map_12(x0,x1),y1) (31)
map_23#(cons,y1,cons2(x0,y3)) → app#(cons1(x0),y1) (32)
map_23#(cons1(x0),y1,cons2(x1,y3)) → app#(cons2(x0,x1),y1) (33)
map_23#(map_2,y1,cons2(x0,y3)) → app#(map_21(x0),y1) (34)
map_23#(map_21(x0),y1,cons2(x1,y3)) → app#(map_22(x0,x1),y1) (35)
map_23#(map_22(x0,x1),y1,cons2(x2,y3)) → app#(map_23(x0,x1,x2),y1) (36)
map_23#(map_3,y1,cons2(x0,y3)) → app#(map_31(x0),y1) (37)
map_23#(map_31(x0),y1,cons2(x1,y3)) → app#(map_32(x0,x1),y1) (38)
map_23#(map_32(x0,x1),y1,cons2(x2,y3)) → app#(map_33(x0,x1,x2),y1) (39)
map_23#(map_33(x0,x1,x2),y1,cons2(x3,y3)) → app#(map_34(x0,x1,x2,x3),y1) (40)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.