Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex49_GM04_L)

The rewrite relation of the following TRS is considered.

if(true) → X (1)
if(false) → Y (2)
minus → 0 (3)
minus → minus (4)
geq → true (5)
geq → false (6)
geq → geq (7)
div(0) → 0 (8)
div(s(X)) → if(geq) (9)

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.