Certification Problem

Input (TPDB TRS_Standard/SK90/4.35)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Bounds

• final states:

  {0, 1, 2}

• transitions:

  a0(0)	→	0
  a0(1)	→	0
  a0(2)	→	0
  b0(0)	→	1
  b0(1)	→	1
  b0(2)	→	1
  c0(0)	→	2
  c0(1)	→	2
  c0(2)	→	2
  b1(0)	→	4
  c1(4)	→	3
  a1(3)	→	0
  b1(1)	→	4
  b1(2)	→	4