Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z03)

The rewrite relation of the following TRS is considered.

a(f,a(g,a(f,x)))	→	a(f,a(g,a(g,a(f,x))))	(1)
a(g,a(f,a(g,x)))	→	a(g,a(f,a(f,a(g,x))))	(2)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

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

final states:

{3, 2, 1}

transitions:

a₄(76,80)	→	59
a₄(76,80)	→	69
a₄(76,80)	→	97
a₄(76,80)	→	6
a₄(76,80)	→	55
a₄(76,80)	→	102
a₄(76,80)	→	130
a₄(76,80)	→	1
a₄(76,80)	→	119
a₄(76,80)	→	66
a₄(76,80)	→	37
a₄(76,80)	→	24
a₄(78,103)	→	104
a₄(76,104)	→	37
a₄(76,104)	→	66
a₄(76,104)	→	6
a₄(76,104)	→	69
a₄(76,104)	→	59
a₄(76,104)	→	119
a₄(76,104)	→	55
a₄(76,104)	→	102
a₄(76,104)	→	1
a₄(76,104)	→	24
a₄(76,104)	→	130
a₄(76,136)	→	6
a₄(76,122)	→	59
a₄(76,92)	→	69
a₄(76,92)	→	37
a₄(76,92)	→	66
a₄(76,92)	→	6
a₄(76,92)	→	59
a₄(76,92)	→	119
a₄(76,92)	→	55
a₄(76,92)	→	102
a₄(76,92)	→	1
a₄(76,92)	→	24
a₄(76,92)	→	130
a₄(76,66)	→	77
a₄(78,121)	→	65
a₄(78,57)	→	99
a₄(76,147)	→	6
a₄(76,47)	→	102
a₄(76,91)	→	59
a₄(76,30)	→	102
a₄(76,61)	→	102
a₄(78,67)	→	96
a₄(78,38)	→	65
a₄(76,1)	→	102
a₄(76,37)	→	102
a₄(76,150)	→	6
a₄(76,97)	→	98
a₄(78,129)	→	65
a₄(78,1)	→	65
a₄(78,68)	→	80
a₄(78,135)	→	65
a₄(76,3)	→	102
a₄(78,102)	→	103
a₄(78,6)	→	68
a₄(78,23)	→	65
a₄(76,96)	→	97
a₄(78,29)	→	65
a₄(76,69)	→	77
a₄(76,119)	→	59
a₄(78,79)	→	80
a₄(76,59)	→	77
a₄(78,2)	→	65
a₄(76,58)	→	90
a₄(78,77)	→	79
a₄(78,77)	→	57
a₄(78,77)	→	38
a₄(78,77)	→	65
a₄(78,77)	→	68
a₄(78,77)	→	60
a₄(78,77)	→	103
a₄(78,77)	→	91
a₄(78,77)	→	121
a₄(78,77)	→	129
a₄(78,77)	→	1
a₄(78,91)	→	92
a₄(76,99)	→	100
a₄(78,59)	→	91
a₄(78,59)	→	1
a₄(78,90)	→	91
a₄(78,101)	→	68
a₄(78,101)	→	57
a₄(78,101)	→	38
a₄(78,101)	→	65
a₄(78,101)	→	60
a₄(78,101)	→	91
a₄(78,101)	→	121
a₄(78,101)	→	103
a₄(78,101)	→	1
a₄(78,101)	→	129
a₄(78,60)	→	65
a₄(76,2)	→	102
a₄(76,130)	→	59
a₄(76,65)	→	59
a₄(76,65)	→	24
a₄(76,65)	→	37
a₄(76,65)	→	66
a₄(76,65)	→	1
a₄(76,65)	→	55
a₄(76,65)	→	6
a₄(76,65)	→	102
a₄(76,65)	→	119
a₄(78,131)	→	65
a₄(78,98)	→	60
a₄(78,98)	→	57
a₄(78,98)	→	38
a₄(78,98)	→	65
a₄(78,98)	→	68
a₄(78,98)	→	103
a₄(78,98)	→	91
a₄(78,98)	→	129
a₄(78,98)	→	121
a₄(78,98)	→	1
a₄(76,100)	→	101
a₄(78,3)	→	65
a₄(76,6)	→	102
a₄(78,70)	→	65
g₆	→	134
a₅(118,59)	→	119
a₅(118,66)	→	119
a₅(120,101)	→	129
a₅(118,65)	→	119
a₅(118,58)	→	119
a₅(120,121)	→	122
a₅(118,69)	→	119
a₅(120,3)	→	129
a₅(120,79)	→	129
a₅(118,104)	→	119
a₅(118,92)	→	119
a₅(118,97)	→	119
a₅(120,77)	→	129
a₅(120,23)	→	129
a₅(120,70)	→	129
a₅(120,103)	→	122
a₅(120,119)	→	121
a₅(120,119)	→	68
a₅(120,59)	→	129
a₅(118,119)	→	131
a₅(118,91)	→	119
a₅(118,122)	→	59
a₅(118,122)	→	119
a₅(118,122)	→	6
a₅(118,122)	→	55
a₅(118,122)	→	102
a₅(118,122)	→	1
a₅(118,122)	→	66
a₅(118,122)	→	37
a₅(118,122)	→	24
a₅(118,122)	→	130
a₅(120,1)	→	129
a₅(118,130)	→	131
a₅(120,135)	→	58
a₅(120,129)	→	58
a₅(120,29)	→	129
a₅(120,90)	→	129
a₅(120,60)	→	129
a₅(120,131)	→	91
a₅(120,131)	→	121
a₅(120,131)	→	65
a₅(120,131)	→	103
a₅(120,131)	→	68
a₅(120,131)	→	129
a₅(120,131)	→	1
a₅(118,129)	→	130
a₅(120,68)	→	129
a₅(120,98)	→	129
a₅(120,38)	→	129
a₅(120,2)	→	129
a₅(118,80)	→	119
a₅(118,100)	→	119
a₅(120,91)	→	122
g₅	→	120
f₄	→	76
g₂	→	28
f₂	→	26
f₆	→	132
a₂(26,39)	→	24
a₂(26,39)	→	1
a₂(26,39)	→	6
a₂(26,39)	→	37
a₂(26,39)	→	59
a₂(26,39)	→	66
a₂(26,39)	→	69
a₂(26,39)	→	55
a₂(26,39)	→	102
a₂(26,39)	→	119
a₂(26,39)	→	130
a₂(26,1)	→	6
a₂(26,1)	→	59
a₂(26,1)	→	66
a₂(26,1)	→	1
a₂(26,1)	→	37
a₂(26,1)	→	24
a₂(26,1)	→	55
a₂(26,1)	→	69
a₂(26,1)	→	102
a₂(26,1)	→	119
a₂(26,1)	→	130
a₂(28,67)	→	1
a₂(28,103)	→	1
a₂(28,38)	→	39
a₂(26,91)	→	1
a₂(28,91)	→	1
a₂(26,119)	→	1
a₂(26,47)	→	48
a₂(28,68)	→	1
a₂(26,122)	→	1
a₂(28,27)	→	29
a₂(26,150)	→	1
a₂(28,129)	→	1
a₂(28,37)	→	38
a₂(28,42)	→	8
a₂(28,42)	→	23
a₂(28,42)	→	60
a₂(28,42)	→	1
a₂(28,42)	→	38
a₂(28,42)	→	68
a₂(28,42)	→	57
a₂(28,42)	→	65
a₂(28,42)	→	103
a₂(28,42)	→	91
a₂(28,42)	→	129
a₂(28,42)	→	121
a₂(28,77)	→	1
a₂(28,90)	→	1
a₂(28,1)	→	1
a₂(28,1)	→	60
a₂(28,1)	→	68
a₂(28,1)	→	65
a₂(28,1)	→	57
a₂(28,1)	→	103
a₂(28,1)	→	91
a₂(28,1)	→	121
a₂(28,1)	→	129
a₂(28,79)	→	1
a₂(26,104)	→	1
a₂(28,59)	→	1
a₂(28,60)	→	1
a₂(26,41)	→	42
a₂(26,92)	→	1
a₂(28,29)	→	30
a₂(26,30)	→	6
a₂(26,30)	→	41
a₂(26,30)	→	59
a₂(26,30)	→	37
a₂(26,30)	→	55
a₂(26,30)	→	24
a₂(26,30)	→	66
a₂(26,30)	→	1
a₂(26,30)	→	69
a₂(26,30)	→	102
a₂(26,30)	→	119
a₂(26,30)	→	130
a₂(28,6)	→	23
a₂(28,6)	→	8
a₂(28,6)	→	1
a₂(28,6)	→	38
a₂(28,6)	→	60
a₂(28,48)	→	23
a₂(28,48)	→	8
a₂(28,48)	→	38
a₂(28,48)	→	1
a₂(28,48)	→	68
a₂(28,48)	→	65
a₂(28,48)	→	60
a₂(28,48)	→	57
a₂(28,48)	→	103
a₂(28,48)	→	91
a₂(28,48)	→	129
a₂(28,48)	→	121
a₂(28,121)	→	1
a₂(26,23)	→	37
a₂(28,8)	→	46
a₂(26,69)	→	1
a₂(26,80)	→	1
a₂(26,65)	→	1
a₂(26,40)	→	41
a₂(26,59)	→	1
a₂(28,23)	→	39
a₂(26,136)	→	1
a₂(28,25)	→	40
a₂(28,2)	→	1
a₂(26,100)	→	1
a₂(28,131)	→	1
a₂(28,3)	→	1
a₂(26,3)	→	6
a₂(26,61)	→	1
a₂(26,6)	→	6
a₂(26,24)	→	27
a₂(26,37)	→	6
a₂(26,46)	→	47
a₂(26,147)	→	1
a₂(26,58)	→	1
a₂(28,135)	→	1
a₂(28,70)	→	1
a₂(28,98)	→	1
a₂(26,9)	→	37
a₂(26,97)	→	1
a₂(28,101)	→	1
a₂(28,57)	→	1
a₂(26,2)	→	6
a₂(26,130)	→	1
a₂(26,66)	→	1
f₀	→	2
g₀	→	3
a₃(54,147)	→	1
a₃(54,6)	→	59
a₃(54,104)	→	6
a₃(54,3)	→	59
a₃(56,57)	→	58
a₃(54,69)	→	70
a₃(54,59)	→	67
a₃(54,47)	→	59
a₃(56,91)	→	1
a₃(56,60)	→	61
a₃(56,77)	→	1
a₃(56,59)	→	60
a₃(56,59)	→	57
a₃(56,59)	→	38
a₃(56,59)	→	68
a₃(56,59)	→	65
a₃(56,59)	→	103
a₃(56,59)	→	91
a₃(56,59)	→	121
a₃(56,59)	→	129
a₃(56,3)	→	65
a₃(54,2)	→	59
a₃(56,135)	→	1
a₃(54,65)	→	66
a₃(54,65)	→	6
a₃(54,65)	→	37
a₃(56,42)	→	68
a₃(54,37)	→	59
a₃(54,119)	→	1
a₃(56,121)	→	1
a₃(56,2)	→	65
a₃(56,67)	→	8
a₃(56,67)	→	1
a₃(56,67)	→	23
a₃(56,67)	→	38
a₃(56,67)	→	68
a₃(54,30)	→	59
a₃(56,6)	→	68
a₃(54,39)	→	55
a₃(54,1)	→	59
a₃(54,1)	→	55
a₃(54,1)	→	24
a₃(54,1)	→	37
a₃(54,1)	→	66
a₃(54,1)	→	1
a₃(54,1)	→	6
a₃(54,1)	→	69
a₃(54,1)	→	102
a₃(54,1)	→	119
a₃(54,1)	→	130
a₃(56,129)	→	1
a₃(56,103)	→	1
a₃(56,38)	→	65
a₃(56,48)	→	68
a₃(54,150)	→	1
a₃(54,130)	→	1
a₃(56,55)	→	57
a₃(56,23)	→	65
a₃(54,61)	→	37
a₃(54,61)	→	59
a₃(54,61)	→	6
a₃(54,61)	→	69
a₃(56,79)	→	1
a₃(54,136)	→	1
a₃(56,98)	→	1
a₃(56,29)	→	65
a₃(54,122)	→	1
a₃(54,66)	→	67
a₃(56,70)	→	38
a₃(56,70)	→	60
a₃(56,70)	→	8
a₃(56,70)	→	1
a₃(56,70)	→	23
a₃(56,70)	→	68
a₃(56,70)	→	57
a₃(56,70)	→	65
a₃(56,70)	→	103
a₃(56,70)	→	91
a₃(56,70)	→	121
a₃(56,70)	→	129
a₃(54,92)	→	6
a₃(54,100)	→	6
a₃(54,41)	→	55
a₃(56,101)	→	1
a₃(56,131)	→	1
a₃(56,90)	→	1
a₃(56,68)	→	1
a₃(54,58)	→	6
a₃(54,58)	→	37
a₃(54,58)	→	59
a₃(54,58)	→	66
a₃(54,58)	→	69
a₃(54,58)	→	55
a₃(54,58)	→	24
a₃(54,58)	→	1
a₃(54,58)	→	102
a₃(54,58)	→	119
a₃(54,58)	→	130
a₃(54,80)	→	6
a₃(56,1)	→	65
a₃(56,1)	→	103
a₃(54,68)	→	69
a₃(54,97)	→	6
a₃(54,91)	→	6
g₃	→	56
a₀(3,3)	→	1
a₀(3,1)	→	1
a₀(1,3)	→	1
a₀(2,2)	→	1
a₀(2,1)	→	1
a₀(1,1)	→	1
a₀(3,2)	→	1
a₀(2,3)	→	1
a₀(1,2)	→	1
g₁	→	7
f₁	→	5
g₄	→	78
f₃	→	54
a₆(134,148)	→	121
a₆(134,148)	→	68
a₆(134,133)	→	135
a₆(134,133)	→	129
a₆(134,133)	→	144
a₆(134,103)	→	136
a₆(132,146)	→	147
a₆(132,145)	→	130
a₆(134,91)	→	136
a₆(134,131)	→	146
a₆(132,149)	→	150
a₆(132,122)	→	143
a₆(134,144)	→	145
a₆(132,136)	→	119
a₆(132,136)	→	130
a₆(132,136)	→	147
a₆(134,129)	→	136
a₆(132,119)	→	133
a₆(134,143)	→	144
a₆(134,151)	→	129
a₆(134,151)	→	121
a₆(134,151)	→	68
a₆(134,151)	→	144
a₆(134,135)	→	136
a₆(132,147)	→	148
a₆(132,150)	→	151
a₆(134,121)	→	149
a₆(132,130)	→	133
a₁(5,9)	→	1
a₁(5,9)	→	6
a₁(5,9)	→	24
a₁(7,79)	→	1
a₁(5,130)	→	1
a₁(7,90)	→	1
a₁(7,3)	→	23
a₁(7,25)	→	1
a₁(7,91)	→	1
a₁(7,77)	→	1
a₁(7,121)	→	1
a₁(7,103)	→	1
a₁(7,135)	→	1
a₁(7,98)	→	1
a₁(5,1)	→	6
a₁(5,1)	→	37
a₁(5,1)	→	59
a₁(5,1)	→	66
a₁(5,1)	→	55
a₁(5,1)	→	69
a₁(5,1)	→	102
a₁(5,1)	→	119
a₁(5,1)	→	130
a₁(5,24)	→	25
a₁(7,129)	→	1
a₁(7,2)	→	23
a₁(5,147)	→	1
a₁(7,23)	→	1
a₁(7,23)	→	23
a₁(5,37)	→	1
a₁(5,58)	→	1
a₁(7,60)	→	1
a₁(5,150)	→	1
a₁(5,3)	→	6
a₁(5,122)	→	1
a₁(5,23)	→	24
a₁(5,23)	→	1
a₁(5,2)	→	6
a₁(5,92)	→	1
a₁(5,66)	→	1
a₁(7,57)	→	1
a₁(7,59)	→	1
a₁(5,91)	→	1
a₁(5,47)	→	1
a₁(5,39)	→	1
a₁(5,119)	→	1
a₁(5,65)	→	1
a₁(5,41)	→	1
a₁(7,48)	→	1
a₁(7,70)	→	1
a₁(7,131)	→	1
a₁(5,59)	→	1
a₁(5,100)	→	1
a₁(7,42)	→	1
a₁(7,38)	→	1
a₁(7,6)	→	8
a₁(7,6)	→	23
a₁(7,6)	→	60
a₁(7,6)	→	38
a₁(7,6)	→	68
a₁(7,6)	→	65
a₁(7,6)	→	57
a₁(7,6)	→	103
a₁(7,6)	→	91
a₁(7,6)	→	129
a₁(7,6)	→	121
a₁(7,68)	→	1
a₁(7,29)	→	1
a₁(7,8)	→	9
a₁(5,97)	→	1
a₁(5,80)	→	1
a₁(7,101)	→	1
a₁(7,1)	→	23
a₁(7,1)	→	65
a₁(7,1)	→	68
a₁(7,1)	→	60
a₁(7,1)	→	57
a₁(7,1)	→	103
a₁(7,1)	→	91
a₁(7,1)	→	129
a₁(7,1)	→	121
a₁(5,136)	→	1
a₁(5,6)	→	23
a₁(5,104)	→	1
a₁(5,30)	→	1
a₁(5,61)	→	1
a₁(5,69)	→	1
a₁(7,67)	→	1
f₅	→	118

The automaton is closed under rewriting as it is compatible.