Certification Problem

Input (TPDB TRS_Standard/Rubio_04/bintrees)

The rewrite relation of the following TRS is considered.

concat(leaf,Y) → Y (1)
concat(cons(U,V),Y) → cons(U,concat(V,Y)) (2)
lessleaves(X,leaf) → false (3)
lessleaves(leaf,cons(W,Z)) → true (4)
lessleaves(cons(U,V),cons(W,Z)) → lessleaves(concat(U,V),concat(W,Z)) (5)

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(leaf) = 0 weight(leaf) = 1
prec(false) = 3 weight(false) = 2
prec(true) = 4 weight(true) = 4
prec(concat) = 2 weight(concat) = 0
prec(cons) = 1 weight(cons) = 1
prec(lessleaves) = 5 weight(lessleaves) = 0
all of the following rules can be deleted.
concat(leaf,Y) → Y (1)
concat(cons(U,V),Y) → cons(U,concat(V,Y)) (2)
lessleaves(X,leaf) → false (3)
lessleaves(leaf,cons(W,Z)) → true (4)
lessleaves(cons(U,V),cons(W,Z)) → lessleaves(concat(U,V),concat(W,Z)) (5)

1.1 R is empty

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