YES Termination proof of AProVE_24_lessleaves.ari

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
    ↳5 RelADPP
        ↳6 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳7 QDP
        ↳8 MRRProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 PisEmptyProof (⇔, 0 ms)
        ↳11 YES
    ↳12 RelADPP
        ↳13 RelADPReductionPairProof (⇔, 29 ms)
        ↳14 RelADPP
        ↳15 DAbsisEmptyProof (⇔, 0 ms)
        ↳16 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

concat(leaf, y) → y
concat(node(u, v), y) → node(u, concat(v, y))
lessleaves(x, leaf) → false
lessleaves(leaf, node(w, z)) → true
lessleaves(node(u, v), node(w, z)) → lessleaves(concat(u, v), concat(w, z))

The relative TRS consists of the following S rules:

lessleaves(node(u, v), node(w, z)) → lessleaves(node(v, u), node(w, z))
lessleaves(node(u, v), node(w, z)) → lessleaves(node(u, v), node(z, w))

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

concat(leaf, y) → y
concat(node(u, v), y) → node(u, CONCAT(v, y))
lessleaves(x, leaf) → false
lessleaves(leaf, node(w, z)) → true
lessleaves(node(u, v), node(w, z)) → LESSLEAVES(concat(u, v), concat(w, z))
lessleaves(node(u, v), node(w, z)) → lessleaves(CONCAT(u, v), concat(w, z))
lessleaves(node(u, v), node(w, z)) → lessleaves(concat(u, v), CONCAT(w, z))

and relative ADPs:

lessleaves(node(u, v), node(w, z)) → LESSLEAVES(node(v, u), node(w, z))
lessleaves(node(u, v), node(w, z)) → LESSLEAVES(node(u, v), node(z, w))

(3) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
2 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 2 subproblems.

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

concat(node(u, v), y) → node(u, CONCAT(v, y))

and relative ADPs:

lessleaves(node(u, v), node(w, z)) → lessleaves(node(v, u), node(w, z))
lessleaves(node(u, v), node(w, z)) → lessleaves(node(u, v), node(z, w))
lessleaves(leaf, node(w, z)) → true
concat(leaf, y) → y
lessleaves(node(u, v), node(w, z)) → lessleaves(concat(u, v), concat(w, z))
lessleaves(x, leaf) → false

(6) RelADPDerelatifyingProof (EQUIVALENT transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CONCAT(node(u, v), y) → CONCAT(v, y)

The TRS R consists of the following rules:

concat(node(u, v), y) → node(u, concat(v, y))
lessleaves(node(u, v), node(w, z)) → lessleaves(node(v, u), node(w, z))
lessleaves(node(u, v), node(w, z)) → lessleaves(node(u, v), node(z, w))
lessleaves(leaf, node(w, z)) → true
concat(leaf, y) → y
lessleaves(node(u, v), node(w, z)) → lessleaves(concat(u, v), concat(w, z))
lessleaves(x, leaf) → false

Q is empty.
We have to consider all (P,Q,R)-chains.

(8) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

CONCAT(node(u, v), y) → CONCAT(v, y)

Strictly oriented rules of the TRS R:

lessleaves(leaf, node(w, z)) → true
concat(leaf, y) → y
lessleaves(node(u, v), node(w, z)) → lessleaves(concat(u, v), concat(w, z))
lessleaves(x, leaf) → false

Used ordering: Polynomial interpretation [POLO]:

POL(CONCAT(x1, x2)) = x1 + x2   
POL(concat(x1, x2)) = x1 + x2   
POL(false) = 2   
POL(leaf) = 2   
POL(lessleaves(x1, x2)) = x1 + 2·x2   
POL(node(x1, x2)) = 1 + x1 + x2   
POL(true) = 1   

(9) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

concat(node(u, v), y) → node(u, concat(v, y))
lessleaves(node(u, v), node(w, z)) → lessleaves(node(v, u), node(w, z))
lessleaves(node(u, v), node(w, z)) → lessleaves(node(u, v), node(z, w))

Q is empty.
We have to consider all (P,Q,R)-chains.

(10) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(11) YES

(12) Obligation:

Relative ADP Problem with
absolute ADPs:

lessleaves(node(u, v), node(w, z)) → LESSLEAVES(concat(u, v), concat(w, z))

and relative ADPs:

lessleaves(node(u, v), node(w, z)) → LESSLEAVES(node(v, u), node(w, z))
lessleaves(node(u, v), node(w, z)) → LESSLEAVES(node(u, v), node(z, w))
concat(node(u, v), y) → node(u, concat(v, y))
lessleaves(leaf, node(w, z)) → true
concat(leaf, y) → y
lessleaves(node(u, v), node(w, z)) → lessleaves(concat(u, v), concat(w, z))
lessleaves(x, leaf) → false

(13) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:


lessleaves(node(u, v), node(w, z)) → LESSLEAVES(concat(u, v), concat(w, z))

Relative ADPs:

concat(node(u, v), y) → node(u, concat(v, y))
lessleaves(leaf, node(w, z)) → true
concat(leaf, y) → y
lessleaves(node(u, v), node(w, z)) → lessleaves(concat(u, v), concat(w, z))
lessleaves(x, leaf) → false


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(CONCAT(x1, x2)) = 2 + 2·x1·x2   
POL(LESSLEAVES(x1, x2)) = x1   
POL(concat(x1, x2)) = x1 + x2   
POL(false) = 0   
POL(leaf) = 0   
POL(lessleaves(x1, x2)) = 0   
POL(node(x1, x2)) = 1 + x1 + x2   
POL(true) = 0   

(14) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

lessleaves(node(u, v), node(w, z)) → LESSLEAVES(node(v, u), node(w, z))
lessleaves(node(u, v), node(w, z)) → LESSLEAVES(node(u, v), node(z, w))
concat(node(u, v), y) → node(u, concat(v, y))
lessleaves(leaf, node(w, z)) → true
concat(leaf, y) → y
lessleaves(node(u, v), node(w, z)) → lessleaves(concat(u, v), concat(w, z))
lessleaves(x, leaf) → false

(15) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(16) YES