Certification Problem

Input (TPDB SRS_Standard/Secret_06_SRS/multum4)

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:

  41	→	3
  41	→	30
  3	→	23
  31	→	74
  26	→	42
  79	→	24
  54	→	29
  75	→	26
  28	→	76
  45	→	78
  77	→	24
  69	→	43
  30	→	23
  30	→	3
  30	→	24
  30	→	44
  27	→	68
  b1(49)	→	50
  b1(36)	→	37
  b1(46)	→	47
  b1(26)	→	27
  b1(35)	→	36
  b1(27)	→	28
  b1(40)	→	41
  b1(32)	→	33
  b1(38)	→	39
  b1(43)	→	44
  b1(25)	→	26
  b1(33)	→	34
  b1(78)	→	79
  b1(51)	→	52
  b1(29)	→	30
  b1(76)	→	77
  b1(74)	→	75
  b1(30)	→	31
  b1(47)	→	48
  b1(44)	→	45
  b1(23)	→	24
  b1(53)	→	54
  b1(39)	→	40
  b1(50)	→	51
  b1(37)	→	38
  b1(24)	→	25
  b1(52)	→	53
  a1(45)	→	46
  a1(31)	→	32
  a1(42)	→	43
  a1(68)	→	69
  a1(48)	→	49
  a1(28)	→	29
  a1(34)	→	35
  a0(3)	→	3
  b0(3)	→	3