Certification Problem

Input (TPDB SRS_Standard/Bouchare_06/08)

The rewrite relation of the following TRS is considered.

a(b(a(x1)))	→	b(b(b(x1)))	(1)
b(a(b(x1)))	→	a(b(a(x1)))	(2)

Prove or disprove termination.

No.

The following loop proves nontermination.

where t₆ = t₀σ and σ = {x1/x1}