Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z050)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Bounds

• final states:

  {0, 1}

• transitions:

  a0(0)	→	0
  a0(1)	→	0
  b0(0)	→	1
  b0(1)	→	1
  a1(0)	→	7
  b1(7)	→	6
  a1(6)	→	5
  b1(5)	→	4
  b1(4)	→	3
  a1(3)	→	2
  a1(2)	→	0
  a1(1)	→	7
  a1(4)	→	7
  2	→	0