YES

The TRS could be proven terminating. The proof took 55 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (4ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

admit#(x, .(u, .(v, .(w, z)))) → cond#(=(sum(x, u, v), w), .(u, .(v, .(w, admit(carry(x, u, v), z)))))admit#(x, .(u, .(v, .(w, z)))) → admit#(carry(x, u, v), z)

Rewrite Rules

admit(x, nil) → niladmit(x, .(u, .(v, .(w, z)))) → cond(=(sum(x, u, v), w), .(u, .(v, .(w, admit(carry(x, u, v), z)))))
cond(true, y) → y

Original Signature

Termination of terms over the following signature is verified: w, sum, true, ., admit, cond, carry, =, nil

Strategy

The following SCCs where found

admit#(x, .(u, .(v, .(w, z)))) → admit#(carry(x, u, v), z)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

admit#(x, .(u, .(v, .(w, z)))) → admit#(carry(x, u, v), z)

Rewrite Rules

admit(x, nil) → niladmit(x, .(u, .(v, .(w, z)))) → cond(=(sum(x, u, v), w), .(u, .(v, .(w, admit(carry(x, u, v), z)))))
cond(true, y) → y

Original Signature

Termination of terms over the following signature is verified: w, sum, true, ., admit, cond, carry, =, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

admit#(x, .(u, .(v, .(w, z)))) → admit#(carry(x, u, v), z)