Certification Problem

Input (TPDB TRS_Relative/INVY_15/#3.1_gen)

The relative rewrite relation R/S is considered where R is the following TRS

-(x,0) x (1)
-(s(x),s(y)) -(x,y) (2)
quot(0,s(y)) 0 (3)
quot(s(x),s(y)) s(quot(-(x,y),s(y))) (4)

and S is the following TRS.

gen 0 (5)
gen s(gen) (6)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves that R/S is not relative terminating.

t0 = -(gen,gen)
S -(gen,s(gen))
S -(s(gen),s(gen))
R -(gen,gen)
= t3
where t3 = t0