Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z059)

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
  15	→	42
  3	→	12
  65	→	47
  49	→	31
  13	→	66
  73	→	63
  21	→	13
  16	→	26
  14	→	58
  17	→	20
  19	→	3
  19	→	17
  a1(20)	→	21
  a1(12)	→	13
  a1(18)	→	19
  b1(17)	→	18
  b1(15)	→	16
  b1(16)	→	17
  b1(14)	→	15
  b1(13)	→	14
  a0(3)	→	3
  b2(61)	→	62
  b2(28)	→	29
  b2(44)	→	45
  b2(70)	→	71
  b2(29)	→	30
  b2(63)	→	64
  b2(59)	→	60
  b2(31)	→	32
  b2(45)	→	46
  b2(43)	→	44
  b2(27)	→	28
  b2(47)	→	48
  b2(60)	→	61
  b2(46)	→	47
  b2(71)	→	72
  b2(62)	→	63
  b2(69)	→	70
  b2(67)	→	68
  b2(30)	→	31
  b2(68)	→	69
  b0(3)	→	3
  a2(64)	→	65
  a2(66)	→	67
  a2(58)	→	59
  a2(26)	→	27
  a2(48)	→	49
  a2(42)	→	43
  a2(72)	→	73
  a2(32)	→	33