Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_GM03_L)

The rewrite relation of the following TRS is considered.

if(true) → X (1)
if(false) → Y (2)
p(0) → 0 (3)
p(s(X)) → X (4)
leq(0,Y) → true (5)
leq(s(X),0) → false (6)
leq(s(X),s(Y)) → leq(X,Y) (7)
diff(X,Y) → if(leq(X,Y)) (8)

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.