Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z30)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

• final states:

  {4}

• transitions:

  a2	→	27
  b2	→	25
  f2(25,34)	→	26
  f2(27,37)	→	38
  f2(27,50)	→	19
  f2(27,50)	→	37
  f2(27,50)	→	89
  f2(27,39)	→	40
  f2(27,40)	→	41
  f2(25,45)	→	35
  f2(27,31)	→	32
  f2(25,33)	→	34
  f2(27,47)	→	48
  f2(25,21)	→	43
  f2(27,34)	→	23
  f2(27,34)	→	41
  f2(25,50)	→	43
  f2(25,49)	→	50
  f2(25,48)	→	26
  f2(27,28)	→	29
  f2(25,30)	→	31
  f2(27,43)	→	44
  f2(27,44)	→	45
  f2(27,29)	→	30
  f2(25,24)	→	43
  f2(27,32)	→	33
  f2(27,48)	→	49
  f2(25,22)	→	26
  f2(25,16)	→	43
  f2(25,42)	→	35
  f2(25,46)	→	47
  f2(27,45)	→	46
  f2(27,35)	→	36
  f2(27,26)	→	28
  f2(27,36)	→	37
  f2(25,38)	→	39
  f2(27,42)	→	20
  f2(27,42)	→	38
  f2(25,19)	→	35
  f2(25,41)	→	42
  f2(25,18)	→	43
  a0	→	4
  b0	→	4
  f3(77,82)	→	83
  f3(77,48)	→	78
  f3(79,78)	→	80
  f3(79,84)	→	85
  f3(77,85)	→	86
  f3(79,94)	→	38
  f3(79,94)	→	90
  f3(79,89)	→	90
  f3(79,91)	→	92
  f3(79,83)	→	84
  f3(79,81)	→	82
  f3(79,80)	→	81
  f3(79,87)	→	88
  f3(79,92)	→	93
  f3(79,86)	→	41
  f3(79,86)	→	93
  f3(77,45)	→	87
  f3(79,88)	→	89
  f3(77,93)	→	94
  f3(77,90)	→	91
  a3	→	79
  f0(4,4)	→	4
  a1	→	17
  b1	→	15
  b3	→	77
  f1(17,19)	→	20
  f1(15,4)	→	16
  f1(15,19)	→	16
  f1(17,21)	→	22
  f1(15,42)	→	16
  f1(17,24)	→	4
  f1(17,24)	→	19
  f1(17,24)	→	37
  f1(15,20)	→	21
  f1(15,34)	→	16
  f1(17,16)	→	18
  f1(15,22)	→	16
  f1(15,24)	→	16
  f1(17,22)	→	23
  f1(15,23)	→	24
  f1(17,18)	→	19