Certification Problem

Input (COPS 676)

We consider the TRS containing the following rules:

The underlying signature is as follows:

Property / Task

Answer / Result

Proof (by csi @ CoCo 2021)

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	→	16
      a	→	2
      a	→	6
      a	→	9
      a	→	12
      f(48)	→	11
      f(2)	→	3
      f(3)	→	4
      f(6)	→	7
      f(11)	→	48
      f(7)	→	8
      f(4)	→	5
      f(9)	→	10
      f(12)	→	13
      c	→	11
      h(18,5)	→	1
      h(13,11)	→	14
      h(14,3)	→	16
      h(16,15)	→	17
      h(14,10)	→	15
      h(17,8)	→	18

    The automaton is closed under rewriting as it is compatible.

  • Automaton 2

    • final states:

      {19}

    • transitions:

      a

      →

      19

    The automaton is closed under rewriting as it is compatible.