Certification Problem

Input (COPS 703)

We consider the TRS containing the following rules:

The underlying signature is as follows:

Property / Task

Answer / Result

Proof (by csi @ CoCo 2022)

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:

      {72}

    • transitions:

      h(104,103)	→	105
      h(92,87)	→	93
      h(82,79)	→	83
      h(85,83)	→	86
      h(78,77)	→	79
      h(98,97)	→	99
      h(105,94)	→	106
      h(93,86)	→	94
      h(99,96)	→	100
      h(106,76)	→	72
      h(75,73)	→	76
      h(89,88)	→	90
      h(101,95)	→	102
      b	→	77
      b	→	95
      c	→	73
      c	→	78
      c	→	80
      c	→	87
      c	→	88
      c	→	96
      c	→	97
      c	→	98
      c	→	104
      a	→	74
      a	→	84
      a	→	89
      f(90)	→	91
      f(91)	→	92
      f(91)	→	84
      f(91)	→	74
      f(91)	→	89
      f(102)	→	103
      f(84)	→	85
      f(80)	→	81
      f(100)	→	101
      f(81)	→	82
      f(74)	→	75

    The automaton is closed under rewriting as it is compatible.

  • Automaton 2

    • final states:

      {36}

    • transitions:

      c

      →

      36

    The automaton is closed under rewriting as it is compatible.