Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z037)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

• final states:

  {2, 1}

• transitions:

  81	→	39
  119	→	42
  119	→	90
  57	→	8
  57	→	42
  9	→	48
  37	→	5
  95	→	49
  1	→	34
  123	→	87
  13	→	1
  13	→	8
  13	→	5
  109	→	49
  143	→	90
  53	→	108
  53	→	110
  2	→	4
  118	→	122
  12	→	36
  12	→	38
  35	→	5
  115	→	134
  83	→	5
  47	→	5
  47	→	9
  47	→	35
  56	→	80
  56	→	82
  56	→	86
  a4(141)	→	142
  a4(135)	→	136
  a4(142)	→	143
  a4(136)	→	137
  a4(139)	→	140
  b4(140)	→	141
  b4(134)	→	135
  b4(137)	→	138
  b4(138)	→	139
  b3(114)	→	115
  b3(86)	→	87
  b3(110)	→	111
  b3(92)	→	93
  b3(90)	→	91
  b3(113)	→	114
  b3(116)	→	117
  b3(122)	→	123
  b3(89)	→	90
  b1(82)	→	83
  b1(7)	→	8
  b1(8)	→	9
  b1(10)	→	11
  b1(36)	→	37
  b1(4)	→	5
  b1(34)	→	35
  a1(11)	→	12
  a1(12)	→	13
  a1(9)	→	10
  a1(6)	→	7
  a1(5)	→	6
  a0(1)	→	2
  a0(2)	→	2
  b2(44)	→	45
  b2(51)	→	52
  b2(80)	→	81
  b2(54)	→	55
  b2(38)	→	39
  b2(52)	→	53
  b2(108)	→	109
  b2(48)	→	49
  b2(42)	→	43
  b2(41)	→	42
  a3(117)	→	118
  a3(91)	→	92
  a3(87)	→	88
  a3(118)	→	119
  a3(94)	→	95
  a3(111)	→	112
  a3(112)	→	113
  a3(93)	→	94
  a3(88)	→	89
  a3(115)	→	116
  b0(1)	→	1
  b0(2)	→	1
  a2(53)	→	54
  a2(56)	→	57
  a2(45)	→	46
  a2(55)	→	56
  a2(46)	→	47
  a2(49)	→	50
  a2(39)	→	40
  a2(43)	→	44
  a2(50)	→	51
  a2(40)	→	41