Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z02)

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(25,15)	→	26
  a4(25,13)	→	26
  a4(27,26)	→	28
  a4(25,32)	→	26
  a4(25,23)	→	26
  a4(25,28)	→	14
  g4	→	27
  f2	→	13
  g2	→	9
  a2(13,9)	→	8
  a2(9,4)	→	15
  a2(6,9)	→	8
  a2(6,9)	→	14
  a2(13,30)	→	22
  a2(13,23)	→	4
  a2(13,32)	→	4
  a2(32,9)	→	22
  a2(32,9)	→	8
  a2(32,9)	→	4
  a2(32,9)	→	14
  a2(32,9)	→	26
  a2(32,9)	→	31
  a2(9,14)	→	15
  a2(23,9)	→	8
  a2(13,21)	→	29
  a2(13,6)	→	14
  a2(15,9)	→	8
  a2(13,13)	→	4
  a2(9,29)	→	30
  a2(13,4)	→	14
  a2(13,15)	→	4
  a2(13,15)	→	8
  a2(13,15)	→	14
  a2(13,15)	→	31
  a2(13,15)	→	26
  a2(13,15)	→	22
  f0	→	4
  g0	→	4
  a3(21,13)	→	22
  a3(23,17)	→	14
  a3(21,32)	→	22
  a3(21,23)	→	8
  a3(21,23)	→	14
  a3(21,23)	→	26
  a3(21,23)	→	4
  a3(21,23)	→	22
  a3(21,23)	→	31
  a3(15,17)	→	14
  a3(13,17)	→	14
  a3(32,17)	→	14
  a3(17,22)	→	23
  a3(21,15)	→	22
  a3(21,6)	→	22
  f3	→	21
  a0(4,4)	→	4
  f1	→	7
  f1	→	4
  g1	→	6
  f4	→	25
  g3	→	17
  a1(4,13)	→	8
  a1(15,6)	→	4
  a1(23,6)	→	4
  a1(4,9)	→	31
  a1(4,32)	→	15
  a1(6,8)	→	6
  a1(32,6)	→	22
  a1(32,6)	→	8
  a1(32,6)	→	4
  a1(32,6)	→	14
  a1(32,6)	→	26
  a1(32,6)	→	31
  a1(7,4)	→	8
  a1(4,6)	→	4
  a1(4,6)	→	8
  a1(4,6)	→	14
  a1(6,31)	→	32
  a1(13,6)	→	4
  a1(6,6)	→	4
  a1(6,6)	→	8
  a1(6,6)	→	14
  a1(4,7)	→	8