Certification Problem

Input (COPS 668)

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:

      h(4,3)	→	5
      h(5,2)	→	6
      h(10,9)	→	1
      h(2,2)	→	3
      h(2,2)	→	7
      h(2,2)	→	2
      h(7,6)	→	8
      h(2,6)	→	7
      h(2,6)	→	2
      h(2,6)	→	3
      f(8)	→	9
      c	→	3
      c	→	7
      c	→	2
      a	→	2
      a	→	3
      a	→	7
      b	→	4
      b	→	10

    The automaton is closed under rewriting as it is compatible.

  • Automaton 2

    • final states:

      {11}

    • transitions:

      b

      →

      11

    The automaton is closed under rewriting as it is compatible.