Certification Problem

Input (TPDB TRS_Standard/AG01/#3.17)

The rewrite relation of the following TRS is considered.

app(nil,k) k (1)
app(l,nil) l (2)
app(cons(x,l),k) cons(x,app(l,k)) (3)
sum(cons(x,nil)) cons(x,nil) (4)
sum(cons(x,cons(y,l))) sum(cons(plus(x,y),l)) (5)
sum(app(l,cons(x,cons(y,k)))) sum(app(l,sum(cons(x,cons(y,k))))) (6)
plus(0,y) y (7)
plus(s(x),y) s(plus(x,y)) (8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[app(x1, x2)] = 1 · x1 + 1 · x2
[nil] = 0
[cons(x1, x2)] = 1 · x1 + 1 · x2
[sum(x1)] = 1 · x1
[plus(x1, x2)] = 1 · x1 + 1 · x2
[0] = 2
[s(x1)] = 1 · x1
all of the following rules can be deleted.
plus(0,y) y (7)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[app(x1, x2)] = 2 · x1 + 2 · x2
[nil] = 1
[cons(x1, x2)] = 1 · x1 + 1 · x2
[sum(x1)] = 1 · x1
[plus(x1, x2)] = 1 · x1 + 1 · x2
[s(x1)] = 1 · x1
all of the following rules can be deleted.
app(nil,k) k (1)
app(l,nil) l (2)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[app(x1, x2)] = 2 · x1 + 1 · x2
[cons(x1, x2)] = 1 + 2 · x1 + 1 · x2
[sum(x1)] = 1 · x1
[nil] = 0
[plus(x1, x2)] = 1 · x1 + 1 · x2
[s(x1)] = 1 · x1
all of the following rules can be deleted.
app(cons(x,l),k) cons(x,app(l,k)) (3)
sum(cons(x,cons(y,l))) sum(cons(plus(x,y),l)) (5)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[sum(x1)] = 1 · x1
[cons(x1, x2)] = 1 · x1 + 2 · x2
[nil] = 0
[app(x1, x2)] = 1 · x1 + 2 · x2
[plus(x1, x2)] = 2 + 2 · x1 + 2 · x2
[s(x1)] = 1 + 1 · x1
all of the following rules can be deleted.
plus(s(x),y) s(plus(x,y)) (8)

1.1.1.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.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
sum#(app(l,cons(x,cons(y,k)))) sum#(app(l,sum(cons(x,cons(y,k))))) (9)
sum#(app(l,cons(x,cons(y,k)))) sum#(cons(x,cons(y,k))) (10)

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.