Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z056)

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:

  33	→	20
  33	→	17
  29	→	66
  15	→	46
  3	→	12
  55	→	27
  31	→	42
  73	→	42
  73	→	31
  21	→	13
  53	→	31
  16	→	26
  30	→	54
  17	→	20
  19	→	3
  19	→	17
  43	→	13
  b3(70)	→	71
  b3(69)	→	70
  b3(71)	→	72
  b3(67)	→	68
  a1(42)	→	43
  a1(20)	→	21
  a1(12)	→	13
  a1(14)	→	15
  a1(18)	→	19
  b1(17)	→	18
  b1(15)	→	16
  b1(16)	→	17
  b1(13)	→	14
  a0(3)	→	3
  b2(50)	→	51
  b2(51)	→	52
  b2(29)	→	30
  b2(49)	→	50
  b2(31)	→	32
  b2(27)	→	28
  b2(47)	→	48
  b2(30)	→	31
  a3(66)	→	67
  a3(68)	→	69
  a3(72)	→	73
  b0(3)	→	3
  a2(54)	→	55
  a2(26)	→	27
  a2(48)	→	49
  a2(28)	→	29
  a2(46)	→	47
  a2(32)	→	33
  a2(52)	→	53