Certification Problem

Input (TPDB TRS_Standard/Applicative_05/Ex2_8_1ConstSubstFix)

The rewrite relation of the following TRS is considered.

app(app(const,x),y) → x (1)
app(app(app(subst,f),g),x) → app(app(f,x),app(g,x)) (2)
app(app(fix,f),x) → app(app(f,app(fix,f)),x) (3)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = app(app(fix,app(subst,f)),x48)
→ app(app(app(subst,f),app(fix,app(subst,f))),x48)
→ app(app(f,x48),app(app(fix,app(subst,f)),x48))
= t2
where t2 = C[t0σ] and σ = {x48/x48, f/f} and C = app(app(f,x48),☐)