Certification Problem

Input (TPDB TRS_Innermost/raML/subtrees.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)
subtrees(@t) → subtrees#1(@t) (4)
subtrees#1(leaf) → nil (5)
subtrees#1(node(@x,@t1,@t2)) → subtrees#2(subtrees(@t1),@t1,@t2,@x) (6)
subtrees#2(@l1,@t1,@t2,@x) → subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x) (7)
subtrees#3(@l2,@l1,@t1,@t2,@x) → ::(node(@x,@t1,@t2),append(@l1,@l2)) (8)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(append) = 1 stat(append) = mul
prec(append#1) = 1 stat(append#1) = mul
prec(::) = 0 stat(::) = mul
prec(nil) = 3 stat(nil) = mul
prec(subtrees) = 3 stat(subtrees) = lex
prec(subtrees#1) = 3 stat(subtrees#1) = lex
prec(leaf) = 4 stat(leaf) = mul
prec(node) = 2 stat(node) = mul
prec(subtrees#2) = 3 stat(subtrees#2) = lex
prec(subtrees#3) = 2 stat(subtrees#3) = mul

π(append) = [1,2]
π(append#1) = [1,2]
π(::) = [1,2]
π(nil) = []
π(subtrees) = [1]
π(subtrees#1) = [1]
π(leaf) = []
π(node) = [1,2,3]
π(subtrees#2) = [3,1,2,4]
π(subtrees#3) = [1,2,3,4,5]

all of the following rules can be deleted.
append#1(::(@x,@xs),@l2) → ::(@x,append(@xs,@l2)) (2)
append#1(nil,@l2) → @l2 (3)
subtrees#1(leaf) → nil (5)
subtrees#1(node(@x,@t1,@t2)) → subtrees#2(subtrees(@t1),@t1,@t2,@x) (6)
subtrees#2(@l1,@t1,@t2,@x) → subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x) (7)
subtrees#3(@l2,@l1,@t1,@t2,@x) → ::(node(@x,@t1,@t2),append(@l1,@l2)) (8)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(subtrees) = 3 weight(subtrees) = 1
prec(subtrees#1) = 2 weight(subtrees#1) = 1
prec(append) = 1 weight(append) = 0
prec(append#1) = 0 weight(append#1) = 0
all of the following rules can be deleted.
append(@l1,@l2) → append#1(@l1,@l2) (1)
subtrees(@t) → subtrees#1(@t) (4)

1.1.1 R is empty

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