Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z01)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

• final states:

  {4}

• transitions:

  a4(107,146)	→	147
  a4(107,117)	→	163
  a4(111,110)	→	112
  a4(107,147)	→	148
  a4(107,100)	→	108
  a4(111,167)	→	119
  a4(111,128)	→	70
  a4(111,112)	→	113
  a4(111,149)	→	150
  a4(111,123)	→	81
  a4(107,163)	→	164
  a4(107,108)	→	109
  a4(107,95)	→	124
  a4(111,126)	→	127
  a4(111,113)	→	71
  a4(107,119)	→	120
  a4(107,94)	→	146
  a4(107,109)	→	110
  a4(111,122)	→	123
  a4(107,127)	→	163
  a4(107,124)	→	125
  a4(111,121)	→	122
  a4(107,125)	→	126
  a4(111,150)	→	115
  a4(107,164)	→	165
  a4(111,127)	→	128
  a4(107,120)	→	121
  a4(107,71)	→	119
  a4(111,165)	→	166
  a4(111,148)	→	149
  a4(111,166)	→	167
  a5(139,166)	→	173
  a5(139,140)	→	141
  a5(139,112)	→	140
  a5(143,175)	→	176
  a5(139,141)	→	142
  a5(143,144)	→	145
  a5(143,142)	→	144
  a5(143,176)	→	177
  a5(139,173)	→	174
  a5(143,145)	→	120
  a5(139,174)	→	175
  a5(143,177)	→	121
  g5	→	143
  f4	→	107
  g2	→	33
  f2	→	29
  a2(29,58)	→	59
  a2(33,78)	→	79
  a2(29,44)	→	45
  a2(33,77)	→	78
  a2(29,35)	→	43
  a2(29,76)	→	77
  a2(29,31)	→	32
  a2(33,62)	→	43
  a2(33,45)	→	46
  a2(29,17)	→	30
  a2(29,43)	→	44
  a2(33,34)	→	35
  a2(33,32)	→	34
  a2(29,59)	→	60
  a2(29,22)	→	30
  a2(29,15)	→	43
  a2(33,60)	→	61
  a2(33,46)	→	47
  a2(29,21)	→	30
  a2(33,61)	→	62
  a2(29,30)	→	31
  a2(29,75)	→	76
  a2(33,47)	→	20
  a2(33,47)	→	31
  a2(33,79)	→	30
  a2(29,46)	→	75
  a2(33,35)	→	14
  a2(33,35)	→	15
  a2(33,35)	→	43
  a2(29,34)	→	58
  f0	→	4
  g0	→	4
  a3(72,83)	→	84
  a3(72,84)	→	76
  a3(72,84)	→	98
  a3(68,61)	→	69
  a3(68,93)	→	94
  a3(72,118)	→	59
  a3(72,118)	→	70
  a3(72,73)	→	74
  a3(68,46)	→	97
  a3(68,70)	→	71
  a3(68,96)	→	114
  a3(72,101)	→	69
  a3(68,114)	→	115
  a3(72,96)	→	32
  a3(72,74)	→	44
  a3(72,74)	→	45
  a3(72,95)	→	96
  a3(68,34)	→	69
  a3(72,117)	→	118
  a3(68,115)	→	116
  a3(72,116)	→	117
  a3(72,71)	→	73
  a3(68,81)	→	82
  a3(68,78)	→	92
  a3(68,92)	→	93
  a3(68,32)	→	69
  a3(68,74)	→	80
  a3(72,82)	→	83
  a3(72,94)	→	95
  a3(72,100)	→	101
  a3(68,80)	→	81
  a3(68,97)	→	98
  a3(68,69)	→	70
  a3(68,98)	→	99
  a3(72,99)	→	100
  g3	→	72
  a0(4,4)	→	4
  g1	→	16
  f1	→	12
  g4	→	111
  f3	→	68
  a1(16,15)	→	17
  a1(16,21)	→	22
  a1(12,18)	→	19
  a1(16,23)	→	13
  a1(16,23)	→	4
  a1(16,23)	→	14
  a1(16,22)	→	23
  a1(16,18)	→	4
  a1(16,18)	→	13
  a1(16,18)	→	14
  a1(12,4)	→	13
  a1(12,14)	→	15
  a1(12,19)	→	20
  a1(12,20)	→	21
  a1(16,17)	→	18
  a1(12,13)	→	14
  a1(12,23)	→	13
  a1(12,17)	→	19
  a1(12,22)	→	13
  f5	→	139