Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z052)

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:

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