Certification Problem

Input (TPDB TRS_Innermost/raML/appendAll.raml)

The rewrite relation of the following TRS is considered.

append(@l1,@l2) → append#1(@l1,@l2) (1)
append#1(::(@x,@xs),@l2) → ::(@x,append(@xs,@l2)) (2)
append#1(nil,@l2) → @l2 (3)
appendAll(@l) → appendAll#1(@l) (4)
appendAll#1(::(@l1,@ls)) → append(@l1,appendAll(@ls)) (5)
appendAll#1(nil) → nil (6)
appendAll2(@l) → appendAll2#1(@l) (7)
appendAll2#1(::(@l1,@ls)) → append(appendAll(@l1),appendAll2(@ls)) (8)
appendAll2#1(nil) → nil (9)
appendAll3(@l) → appendAll3#1(@l) (10)
appendAll3#1(::(@l1,@ls)) → append(appendAll2(@l1),appendAll3(@ls)) (11)
appendAll3#1(nil) → nil (12)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(nil) = 0 weight(nil) = 1
prec(appendAll) = 2 weight(appendAll) = 2
prec(appendAll#1) = 1 weight(appendAll#1) = 2
prec(appendAll2) = 4 weight(appendAll2) = 2
prec(appendAll2#1) = 7 weight(appendAll2#1) = 1
prec(appendAll3) = 8 weight(appendAll3) = 1
prec(appendAll3#1) = 9 weight(appendAll3#1) = 0
prec(append) = 6 weight(append) = 0
prec(append#1) = 5 weight(append#1) = 0
prec(::) = 3 weight(::) = 3
all of the following rules can be deleted.
append(@l1,@l2) → append#1(@l1,@l2) (1)
append#1(::(@x,@xs),@l2) → ::(@x,append(@xs,@l2)) (2)
append#1(nil,@l2) → @l2 (3)
appendAll(@l) → appendAll#1(@l) (4)
appendAll#1(::(@l1,@ls)) → append(@l1,appendAll(@ls)) (5)
appendAll#1(nil) → nil (6)
appendAll2(@l) → appendAll2#1(@l) (7)
appendAll2#1(::(@l1,@ls)) → append(appendAll(@l1),appendAll2(@ls)) (8)
appendAll2#1(nil) → nil (9)
appendAll3(@l) → appendAll3#1(@l) (10)
appendAll3#1(::(@l1,@ls)) → append(appendAll2(@l1),appendAll3(@ls)) (11)
appendAll3#1(nil) → nil (12)

1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.