Certification Problem

Input (COPS 1109)

We consider two TRSs R and S where R contains the rules

and S contains the following rules:

The underlying signature is as follows:

Property / Task

Answer / Result

Proof (by ACP @ 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:

      {q_0}

    • transitions:

      a	→	q_{c}
      b	→	q_{b}
      b	→	q_{c}
      c	→	q_{c}
      f(q_{b})	→	q_{f(b)}
      f(q_{c})	→	q_{c}
      f(q_{f(b)})	→	q_0
      f(q_{f(b)})	→	q_{b}
      f(q_{h(c,b)})	→	q_1
      f(q_{h(c,b)})	→	q_{b}
      f(q_{h(c,b)})	→	q_{c}
      h(q_{c},q_{b})	→	q_{h(c,b)}

    The automaton is closed under rewriting as can be seen by the decision procedure.

  • Automaton 2

    • final states:

      {q_1}

    • transitions:

      a	→	q_{c}
      b	→	q_{b}
      b	→	q_{c}
      c	→	q_{c}
      f(q_{b})	→	q_{f(b)}
      f(q_{c})	→	q_{c}
      f(q_{f(b)})	→	q_0
      f(q_{f(b)})	→	q_{b}
      f(q_{h(c,b)})	→	q_1
      f(q_{h(c,b)})	→	q_{b}
      f(q_{h(c,b)})	→	q_{c}
      h(q_{c},q_{b})	→	q_{h(c,b)}

    The automaton is closed under rewriting as can be seen by the decision procedure.