Certification Problem

Input (TPDB TRS_Innermost/raML/rationalPotential.raml)

The rewrite relation of the following TRS is considered.

group3(@l) → group3#1(@l) (1)
group3#1(::(@x,@xs)) → group3#2(@xs,@x) (2)
group3#1(nil) → nil (3)
group3#2(::(@y,@ys),@x) → group3#3(@ys,@x,@y) (4)
group3#2(nil,@x) → nil (5)
group3#3(::(@z,@zs),@x,@y) → ::(tuple#3(@x,@y,@z),group3(@zs)) (6)
group3#3(nil,@x,@y) → nil (7)
zip3(@l1,@l2,@l3) → zip3#1(@l1,@l2,@l3) (8)
zip3#1(::(@x,@xs),@l2,@l3) → zip3#2(@l2,@l3,@x,@xs) (9)
zip3#1(nil,@l2,@l3) → nil (10)
zip3#2(::(@y,@ys),@l3,@x,@xs) → zip3#3(@l3,@x,@xs,@y,@ys) (11)
zip3#2(nil,@l3,@x,@xs) → nil (12)
zip3#3(::(@z,@zs),@x,@xs,@y,@ys) → ::(tuple#3(@x,@y,@z),zip3(@xs,@ys,@zs)) (13)
zip3#3(nil,@x,@xs,@y,@ys) → nil (14)
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) = 9 weight(nil) = 1
prec(group3) = 6 weight(group3) = 2
prec(group3#1) = 0 weight(group3#1) = 1
prec(::) = 5 weight(::) = 2
prec(group3#2) = 8 weight(group3#2) = 1
prec(group3#3) = 1 weight(group3#3) = 3
prec(tuple#3) = 2 weight(tuple#3) = 0
prec(zip3) = 3 weight(zip3) = 1
prec(zip3#1) = 7 weight(zip3#1) = 0
prec(zip3#2) = 10 weight(zip3#2) = 1
prec(zip3#3) = 4 weight(zip3#3) = 2
all of the following rules can be deleted.
group3(@l) → group3#1(@l) (1)
group3#1(::(@x,@xs)) → group3#2(@xs,@x) (2)
group3#1(nil) → nil (3)
group3#2(::(@y,@ys),@x) → group3#3(@ys,@x,@y) (4)
group3#2(nil,@x) → nil (5)
group3#3(::(@z,@zs),@x,@y) → ::(tuple#3(@x,@y,@z),group3(@zs)) (6)
group3#3(nil,@x,@y) → nil (7)
zip3(@l1,@l2,@l3) → zip3#1(@l1,@l2,@l3) (8)
zip3#1(::(@x,@xs),@l2,@l3) → zip3#2(@l2,@l3,@x,@xs) (9)
zip3#1(nil,@l2,@l3) → nil (10)
zip3#2(::(@y,@ys),@l3,@x,@xs) → zip3#3(@l3,@x,@xs,@y,@ys) (11)
zip3#2(nil,@l3,@x,@xs) → nil (12)
zip3#3(::(@z,@zs),@x,@xs,@y,@ys) → ::(tuple#3(@x,@y,@z),zip3(@xs,@ys,@zs)) (13)
zip3#3(nil,@x,@xs,@y,@ys) → nil (14)

1.1 R is empty

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