Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z054)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

1.1 Bounds

• final states:

  {3}

• transitions:

  23	→	50
  25	→	42
  51	→	21
  15	→	44
  3	→	12
  55	→	21
  31	→	13
  13	→	54
  21	→	56
  45	→	21
  63	→	24
  17	→	20
  17	→	30
  19	→	3
  19	→	16
  19	→	14
  19	→	24
  43	→	13
  27	→	16
  27	→	18
  27	→	24
  b3(59)	→	60
  b3(57)	→	58
  b3(61)	→	62
  a1(16)	→	17
  a1(42)	→	43
  a1(12)	→	13
  a1(14)	→	15
  a1(30)	→	31
  a1(18)	→	19
  b1(17)	→	18
  b1(15)	→	16
  b1(13)	→	14
  a0(3)	→	3
  b2(23)	→	24
  b2(25)	→	26
  b2(21)	→	22
  a3(56)	→	57
  a3(62)	→	63
  a3(60)	→	61
  a3(58)	→	59
  b0(3)	→	3
  a2(44)	→	45
  a2(22)	→	23
  a2(24)	→	25
  a2(54)	→	55
  a2(26)	→	27
  a2(20)	→	21
  a2(50)	→	51