Certification Problem

Input (TPDB TRS_Standard/Applicative_05/nonTermF)

The rewrite relation of the following TRS is considered.

ap(ap(f,x),x) → ap(ap(x,ap(f,x)),ap(ap(cons,x),nil)) (1)
ap(ap(ap(foldr,g),h),nil) → h (2)
ap(ap(ap(foldr,g),h),ap(ap(cons,x),xs)) → ap(ap(g,x),ap(ap(ap(foldr,g),h),xs)) (3)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = ap(ap(ap(foldr,ap(f,foldr)),ap(ap(cons,foldr),nil)),ap(ap(cons,foldr),nil))
→ ap(ap(ap(f,foldr),foldr),ap(ap(ap(foldr,ap(f,foldr)),ap(ap(cons,foldr),nil)),nil))
→ ap(ap(ap(foldr,ap(f,foldr)),ap(ap(cons,foldr),nil)),ap(ap(ap(foldr,ap(f,foldr)),ap(ap(cons,foldr),nil)),nil))
→ ap(ap(ap(foldr,ap(f,foldr)),ap(ap(cons,foldr),nil)),ap(ap(cons,foldr),nil))
= t3
where t3 = t0