Certificate for #864 ⟨a, b | abbbaaab=a⟩

Back:⟨a, b | abbbaaab=a⟩

Completion settings:

[1] abbbaaab=a

Axiom: abbbaaab=a.

Defines rule #4.

Referenced by [2], [3], [4].

[2] abbaaab=abbbaaa

Overlap of [1] abbbaaab=a with [1] abbbaaab=a:

abbbaa ab abbbaaab

Critical pair: abbbaaa=abbaaab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] abaaab=abbaaa

Overlap of [1] abbbaaab=a with [2] abbaaab=abbbaaa:

abbbaa ab abbaaab

Critical pair: abbbaaabbbaaa=abaaab.

Reduce LHS:

[1](abbbaaab)bbaaa
⇒ abbaaa

Flip LHS and RHS.

Defines rule #2.

[4] aaaab=abaaa

Overlap of [2] abbaaab=abbbaaa with [2] abbaaab=abbbaaa:

abbaa ab abbaaab

Critical pair: abbaaabbbaaa=abbbaaabaaab.

Reduce LHS:

[2](abbaaab)bbaaa
[1]⇒ (abbbaaab)baaa
⇒ abaaa

Reduce RHS:

[1](abbbaaab)aaab
⇒ aaaab

Flip LHS and RHS.

Defines rule #1.