Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwtpa1)

The rewrite relation of the following TRS is considered.

f(f(a,x),y)

→

f(y,f(x,f(a,f(h(a),a))))

(1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

The given TRS is match-(raise)-bounded by 2. This is shown by the following automaton.

final states:

{4}

transitions:

a₂	→	15
h₂(15)	→	16
f₂(13,19)	→	14
f₂(16,15)	→	17
f₂(14,19)	→	14
f₂(15,17)	→	18
f₂(12,18)	→	19
f₂(19,19)	→	14
a₀	→	4
h₀(4)	→	4
f₀(4,4)	→	4
a₁	→	10
h₁(10)	→	11
f₁(4,14)	→	4
f₁(19,14)	→	14
f₁(11,10)	→	12
f₁(13,14)	→	14
f₁(4,13)	→	14
f₁(13,13)	→	14
f₁(10,12)	→	13
f₁(14,13)	→	14
f₁(14,14)	→	4

The automaton is closed under rewriting as it is compatible.