Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds_L)

The rewrite relation of the following TRS is considered.

U11(tt)	→	N	(1)
U21(tt)	→	s(plus(N,M))	(2)
and(tt)	→	X	(3)
isNat	→	tt	(4)
isNat	→	and(isNat)	(5)
isNat	→	isNat	(6)
plus(N,0)	→	U11(isNat)	(7)
plus(N,s(M))	→	U21(and(isNat))	(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.