Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nosorts-noand_L)

The rewrite relation of the following TRS is considered.

U12(tt) → s(plus(N,M)) (1)
U11(tt) → U12(tt) (2)
plus(N,0) → N (3)
plus(N,s(M)) → U11(tt) (4)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Variable Condition Violated

The TRS violates one of the two variable conditions. Thus, it is not terminating.