Certification Problem

Input (COPS 955)

We consider the TRS containing the following rules:

The underlying signature is as follows:

Property / Task

Answer / Result

Proof (by csi @ CoCo 2023)

1 Non-Joinable Fork

• The reachable terms of these two terms are approximated via the following two tree automata, and the tree automata have an empty intersection.

  • Automaton 1

    • final states:

      {1}

    • transitions:

      b(548)	→	454
      b(93)	→	643
      b(2)	→	93
      b(207)	→	376
      b(3)	→	4
      b(6)	→	7
      b(376)	→	208
      b(7)	→	8
      b(5)	→	6
      b(453)	→	548
      b(4)	→	5
      b(94)	→	453
      b(95)	→	207
      b(8)	→	1
      a(207)	→	208
      a(2)	→	3
      a(454)	→	207
      a(95)	→	6
      a(94)	→	95
      a(93)	→	94
      a(643)	→	644
      a(453)	→	454
      a(644)	→	453
      a(208)	→	209
      a(209)	→	1
      f3	→	2

    The automaton is closed under rewriting as it is compatible.

  • Automaton 2

    • final states:

      {9}

    • transitions:

      b(11)	→	12
      b(12)	→	13
      a(14)	→	15
      a(15)	→	9
      a(10)	→	11
      a(13)	→	14
      f3	→	10

    The automaton is closed under rewriting as it is compatible.