Certification Problem

Input (COPS 243)

We consider the TRS containing the following rules:

The underlying signature is as follows:

Property / Task

Answer / Result

Proof (by csi @ CoCo 2020)

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:

      {9}

    • transitions:

      g(10)	→	11
      g(10)	→	10
      g(11)	→	11
      g(11)	→	32
      g(9)	→	9
      g(32)	→	9
      b	→	10
      h(10)	→	32
      h(10)	→	11
      h(10)	→	10
      h(9)	→	9
      h(32)	→	9
      h(11)	→	9
      h(11)	→	32
      h(11)	→	11

    The automaton is closed under rewriting as it is compatible.

  • Automaton 2

    • final states:

      {7}

    • transitions:

      c	→	8
      h(8)	→	7

    The automaton is closed under rewriting as it is compatible.