Certification Problem

Input (COPS 68)

We consider the TRS containing the following rules:

The underlying signature is as follows:

Property / Task

Answer / Result

Proof (by csi @ CoCo 2023)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

All redundant rules that were added or removed can be simulated in 2 steps .

1.1 Decreasing Diagrams

1.1.2 Rule Labeling

• w(w(x))

  →

  w(x)

  (4)

  ↦ 0

• b(b(x))

  →

  w(w(w(w(x))))

  (3)

  ↦ 4

• w(b(x))

  →

  b(x)

  (2)

  ↦ 0

• b(w(x))

  →

  w(w(w(b(x))))

  (1)

  ↦ 5

• b(b(x))

  →

  w(w(w(x)))

  (5)

  ↦ 4

• b(w(x))

  →

  w(w(b(x)))

  (6)

  ↦ 4

• The critical peak s = w(w(x113))←→_ε w(w(x113)) = t can be joined as follows.
  s ↔ t
• The critical peak s = b(w(x114))←→_ε w(w(w(b(w(x114))))) = t can be joined as follows.
  s ↔ b(w(x114)) ↔ w(b(w(x114))) ↔ w(w(b(w(x114)))) ↔ t
• The critical peak s = b(w(x114))←→_ε w(w(w(b(w(x114))))) = t can be joined as follows.
  s ↔ w(w(w(b(x114)))) ↔ w(b(w(x114))) ↔ w(w(b(w(x114)))) ↔ t
• The critical peak s = b(w(x114))←→_ε w(w(w(b(w(x114))))) = t can be joined as follows.
  s ↔ w(w(w(b(x114)))) ↔ w(w(w(w(b(x114))))) ↔ w(w(b(w(x114)))) ↔ t
• The critical peak s = b(w(x114))←→_ε w(w(w(b(w(x114))))) = t can be joined as follows.
  s ↔ w(w(w(b(x114)))) ↔ w(w(w(w(b(x114))))) ↔ w(w(w(w(w(b(x114)))))) ↔ t
• The critical peak s = b(w(x115))←→_ε w(w(b(w(x115)))) = t can be joined as follows.
  s ↔ b(w(x115)) ↔ w(b(w(x115))) ↔ t
• The critical peak s = b(w(x115))←→_ε w(w(b(w(x115)))) = t can be joined as follows.
  s ↔ w(w(w(b(x115)))) ↔ w(b(w(x115))) ↔ t
• The critical peak s = b(w(x115))←→_ε w(w(b(w(x115)))) = t can be joined as follows.
  s ↔ w(w(w(b(x115)))) ↔ w(w(w(w(b(x115))))) ↔ t
• The critical peak s = b(w(w(w(w(x116)))))←→_ε w(w(w(w(b(x116))))) = t can be joined as follows.
  s ↔ b(w(w(w(x116)))) ↔ b(w(w(x116))) ↔ b(w(x116)) ↔ w(w(w(b(x116)))) ↔ t
• The critical peak s = b(w(w(w(w(x116)))))←→_ε w(w(w(w(b(x116))))) = t can be joined as follows.
  s ↔ b(w(w(w(x116)))) ↔ b(w(w(x116))) ↔ b(w(x116)) ↔ w(w(b(x116))) ↔ w(w(w(b(x116)))) ↔ t
• The critical peak s = b(w(w(w(w(x116)))))←→_ε w(w(w(w(b(x116))))) = t can be joined as follows.
  s ↔ b(w(w(w(x116)))) ↔ b(w(w(x116))) ↔ w(w(b(w(x116)))) ↔ t
• The critical peak s = b(w(w(w(w(x116)))))←→_ε w(w(w(w(b(x116))))) = t can be joined as follows.
  s ↔ b(w(w(w(x116)))) ↔ w(w(b(w(w(x116))))) ↔ w(w(b(w(x116)))) ↔ t
• The critical peak s = b(w(w(w(w(x116)))))←→_ε w(w(w(w(b(x116))))) = t can be joined as follows.
  s ↔ w(w(b(w(w(w(x116)))))) ↔ w(w(b(w(w(x116))))) ↔ w(w(b(w(x116)))) ↔ t
• The critical peak s = w(w(w(w(w(x117)))))←→_ε b(b(x117)) = t can be joined as follows.
  s ↔ w(w(w(w(x117)))) ↔ t
• The critical peak s = w(w(w(w(x))))←→_ε w(w(w(x))) = t can be joined as follows.
  s ↔ t
• The critical peak s = b(w(w(w(w(x119)))))←→_ε w(w(w(b(x119)))) = t can be joined as follows.
  s ↔ b(w(w(w(x119)))) ↔ b(w(w(x119))) ↔ b(w(x119)) ↔ t
• The critical peak s = b(w(w(w(w(x119)))))←→_ε w(w(w(b(x119)))) = t can be joined as follows.
  s ↔ b(w(w(w(x119)))) ↔ b(w(w(x119))) ↔ b(w(x119)) ↔ w(w(b(x119))) ↔ t
• The critical peak s = w(b(x120))←→_ε w(b(x120)) = t can be joined as follows.
  s ↔ t
• The critical peak s = b(b(x121))←→_ε w(w(w(b(b(x121))))) = t can be joined as follows.
  s ↔ b(b(x121)) ↔ w(b(b(x121))) ↔ w(w(b(b(x121)))) ↔ t
• The critical peak s = b(b(x121))←→_ε w(w(w(b(b(x121))))) = t can be joined as follows.
  s ↔ w(w(w(w(x121)))) ↔ w(b(b(x121))) ↔ w(w(b(b(x121)))) ↔ t
• The critical peak s = b(b(x121))←→_ε w(w(w(b(b(x121))))) = t can be joined as follows.
  s ↔ w(w(w(w(x121)))) ↔ w(w(w(w(w(x121))))) ↔ w(w(b(b(x121)))) ↔ t
• The critical peak s = b(b(x121))←→_ε w(w(w(b(b(x121))))) = t can be joined as follows.
  s ↔ w(w(w(w(x121)))) ↔ w(w(w(w(w(x121))))) ↔ w(w(w(w(w(w(x121)))))) ↔ t
• The critical peak s = b(b(x122))←→_ε w(w(b(b(x122)))) = t can be joined as follows.
  s ↔ b(b(x122)) ↔ w(b(b(x122))) ↔ t
• The critical peak s = b(b(x122))←→_ε w(w(b(b(x122)))) = t can be joined as follows.
  s ↔ w(w(w(w(x122)))) ↔ w(b(b(x122))) ↔ t
• The critical peak s = b(b(x122))←→_ε w(w(b(b(x122)))) = t can be joined as follows.
  s ↔ w(w(w(w(x122)))) ↔ w(w(w(w(w(x122))))) ↔ t
• The critical peak s = b(w(w(w(b(x123)))))←→_ε w(w(w(w(w(x123))))) = t can be joined as follows.
  s ↔ b(w(w(b(x123)))) ↔ b(w(b(x123))) ↔ b(b(x123)) ↔ w(w(w(w(x123)))) ↔ t
• The critical peak s = b(w(w(w(b(x123)))))←→_ε w(w(w(w(w(x123))))) = t can be joined as follows.
  s ↔ b(w(w(b(x123)))) ↔ b(w(b(x123))) ↔ b(b(x123)) ↔ w(w(w(x123))) ↔ w(w(w(w(x123)))) ↔ t
• The critical peak s = b(w(w(w(b(x123)))))←→_ε w(w(w(w(w(x123))))) = t can be joined as follows.
  s ↔ b(w(w(b(x123)))) ↔ b(w(b(x123))) ↔ w(w(b(b(x123)))) ↔ t
• The critical peak s = b(w(w(w(b(x123)))))←→_ε w(w(w(w(w(x123))))) = t can be joined as follows.
  s ↔ b(w(w(b(x123)))) ↔ w(w(b(w(b(x123))))) ↔ w(w(b(b(x123)))) ↔ t
• The critical peak s = b(w(w(w(b(x123)))))←→_ε w(w(w(w(w(x123))))) = t can be joined as follows.
  s ↔ w(w(b(w(w(b(x123)))))) ↔ w(w(b(w(b(x123))))) ↔ w(w(b(b(x123)))) ↔ t
• The critical peak s = w(w(w(w(b(x124)))))←→_ε b(w(x124)) = t can be joined as follows.
  s ↔ w(w(w(b(x124)))) ↔ t
• The critical peak s = b(w(w(w(b(x125)))))←→_ε w(w(w(w(x125)))) = t can be joined as follows.
  s ↔ b(w(w(b(x125)))) ↔ b(w(b(x125))) ↔ b(b(x125)) ↔ t
• The critical peak s = b(w(w(w(b(x125)))))←→_ε w(w(w(w(x125)))) = t can be joined as follows.
  s ↔ b(w(w(b(x125)))) ↔ b(w(b(x125))) ↔ b(b(x125)) ↔ w(w(w(x125))) ↔ t
• The critical peak s = w(w(w(b(x))))←→_ε w(w(b(x))) = t can be joined as follows.
  s ↔ t
• The critical peak s = w(w(w(x)))←→_ε w(w(w(w(x)))) = t can be joined as follows.
  s ↔ w(w(w(x))) ↔ t
• The critical peak s = b(w(w(w(x128))))←→_ε w(w(w(w(b(x128))))) = t can be joined as follows.
  s ↔ b(w(w(x128))) ↔ b(w(x128)) ↔ w(w(w(b(x128)))) ↔ t
• The critical peak s = b(w(w(w(x128))))←→_ε w(w(w(w(b(x128))))) = t can be joined as follows.
  s ↔ b(w(w(x128))) ↔ b(w(x128)) ↔ w(w(b(x128))) ↔ w(w(w(b(x128)))) ↔ t
• The critical peak s = b(w(w(w(x128))))←→_ε w(w(w(w(b(x128))))) = t can be joined as follows.
  s ↔ b(w(w(x128))) ↔ w(w(b(w(x128)))) ↔ t
• The critical peak s = b(w(w(w(x128))))←→_ε w(w(w(w(b(x128))))) = t can be joined as follows.
  s ↔ w(w(b(w(w(x128))))) ↔ w(w(b(w(x128)))) ↔ t
• The critical peak s = w(w(w(w(x129))))←→_ε b(b(x129)) = t can be joined as follows.
  s ↔ w(w(w(w(x129)))) ↔ t
• The critical peak s = w(w(w(w(x129))))←→_ε b(b(x129)) = t can be joined as follows.
  s ↔ w(w(w(x129))) ↔ t
• The critical peak s = b(w(w(w(x130))))←→_ε w(w(w(b(x130)))) = t can be joined as follows.
  s ↔ b(w(w(x130))) ↔ b(w(x130)) ↔ t
• The critical peak s = b(w(w(w(x130))))←→_ε w(w(w(b(x130)))) = t can be joined as follows.
  s ↔ b(w(w(x130))) ↔ b(w(x130)) ↔ w(w(b(x130))) ↔ t
• The critical peak s = b(w(w(b(x131))))←→_ε w(w(w(w(w(x131))))) = t can be joined as follows.
  s ↔ b(w(b(x131))) ↔ b(b(x131)) ↔ w(w(w(w(x131)))) ↔ t
• The critical peak s = b(w(w(b(x131))))←→_ε w(w(w(w(w(x131))))) = t can be joined as follows.
  s ↔ b(w(b(x131))) ↔ b(b(x131)) ↔ w(w(w(x131))) ↔ w(w(w(w(x131)))) ↔ t
• The critical peak s = b(w(w(b(x131))))←→_ε w(w(w(w(w(x131))))) = t can be joined as follows.
  s ↔ b(w(b(x131))) ↔ w(w(b(b(x131)))) ↔ t
• The critical peak s = b(w(w(b(x131))))←→_ε w(w(w(w(w(x131))))) = t can be joined as follows.
  s ↔ w(w(b(w(b(x131))))) ↔ w(w(b(b(x131)))) ↔ t
• The critical peak s = w(w(w(b(x132))))←→_ε b(w(x132)) = t can be joined as follows.
  s ↔ w(w(w(b(x132)))) ↔ t
• The critical peak s = w(w(w(b(x132))))←→_ε b(w(x132)) = t can be joined as follows.
  s ↔ w(w(b(x132))) ↔ t
• The critical peak s = w(w(b(x)))←→_ε w(w(w(b(x)))) = t can be joined as follows.
  s ↔ w(w(b(x))) ↔ t
• The critical peak s = b(w(w(b(x134))))←→_ε w(w(w(w(x134)))) = t can be joined as follows.
  s ↔ b(w(b(x134))) ↔ b(b(x134)) ↔ t
• The critical peak s = b(w(w(b(x134))))←→_ε w(w(w(w(x134)))) = t can be joined as follows.
  s ↔ b(w(b(x134))) ↔ b(b(x134)) ↔ w(w(w(x134))) ↔ t