Certification Problem

Input (COPS 1038)

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_1}

    • transitions:

      a	→	q_0
      a	→	q_{*}
      a	→	q_{a}
      a	→	q_{f(*)}
      f(q_{g(f(a))})	→	q_0
      f(q_{*})	→	q_{*}
      f(q_{*})	→	q_{f(*)}
      f(q_{a})	→	q_1
      f(q_{a})	→	q_{f(a)}
      g(q_{*})	→	q_{*}
      g(q_{*})	→	q_{f(*)}
      g(q_{f(*)})	→	q_0
      g(q_{f(*)})	→	q_{f(*)}
      g(q_{f(a)})	→	q_{g(f(a))}

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

  • Automaton 2

    • final states:

      {q_0}

    • transitions:

      a	→	q_0
      a	→	q_{*}
      a	→	q_{a}
      a	→	q_{f(*)}
      f(q_{g(f(a))})	→	q_0
      f(q_{*})	→	q_{*}
      f(q_{*})	→	q_{f(*)}
      f(q_{a})	→	q_1
      f(q_{a})	→	q_{f(a)}
      g(q_{*})	→	q_{*}
      g(q_{*})	→	q_{f(*)}
      g(q_{f(*)})	→	q_0
      g(q_{f(*)})	→	q_{f(*)}
      g(q_{f(a)})	→	q_{g(f(a))}

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