Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z064)

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:

  {4}

• transitions:

  15	→	37
  34	→	21
  34	→	17
  20	→	4
  20	→	17
  44	→	31
  22	→	14
  4	→	13
  16	→	27
  17	→	21
  a2(37)	→	38
  a2(32)	→	33
  a2(27)	→	28
  a2(42)	→	43
  b2(41)	→	42
  b2(31)	→	32
  b2(39)	→	40
  b2(29)	→	30
  b2(30)	→	31
  b2(40)	→	41
  c2(33)	→	34
  c2(38)	→	39
  c2(43)	→	44
  c2(28)	→	29
  c0(4)	→	4
  a0(4)	→	4
  b0(4)	→	4
  a1(18)	→	19
  a1(13)	→	14
  a1(21)	→	22
  b1(17)	→	18
  b1(15)	→	16
  b1(16)	→	17
  c1(14)	→	15
  c1(19)	→	20