Vervollständigung (basic)

...ist Algorithmus mit dieser Spezifikation

• Eingabe: Gleichungssystem E
• Ausgabe: Ersetzungssystem R mit Eigenschaften:
  • R ist konvergent (: = terminierend und konfluent)
  • $\approx_{R}^{}$  =  $\approx_{E}^{}$

Implementierung: zusätzliche Eingabe: eine wfmA A

• ordne Paare aus E bzgl. > _A, Resultat R₀
• wiederhole bis R_i+1 = R_i:

  R_i+1 : = R_i∪ die folgenden Paare: ∀(s, t)∈CP(R_i):

  • wähle s'∈Nf_Ri(s), t'∈Nf_Ri(t)
  • falls s'≠t', ordne (s', t') bzgl. > _A.

Korrektheit? Termination? beachte: 3 Fehlermöglichkeiten