Certification Problem

Input (TPDB TRS_Standard/SK90/4.46)

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, 3}

• transitions:

  f0(0)	→	0
  f0(1)	→	0
  f0(2)	→	0
  f0(3)	→	0
  a0	→	1
  b0	→	2
  g0(0)	→	3
  g0(1)	→	3
  g0(2)	→	3
  g0(3)	→	3
  b1	→	4
  f1(4)	→	0
  a1	→	5
  g1(5)	→	3