Certificate for #3823 ⟨a, b | abbbaaaaab=a⟩

Back:⟨a, b | abbbaaaaab=a⟩

Completion settings:

[1] abbbaaaaab=a

Axiom: abbbaaaaab=a.

Defines rule #4.

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

[2] abbaaaaab=abbbaaaaa

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

abbbaaaa ab abbbaaaaab

Critical pair: abbbaaaaa=abbaaaaab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] abaaaaab=abbaaaaa

Overlap of [1] abbbaaaaab=a with [2] abbaaaaab=abbbaaaaa:

abbbaaaa ab abbaaaaab

Critical pair: abbbaaaaabbbaaaaa=abaaaaab.

Reduce LHS:

[1](abbbaaaaab)bbaaaaa
⇒ abbaaaaa

Flip LHS and RHS.

Defines rule #2.

[4] aaaaaab=abaaaaa

Overlap of [2] abbaaaaab=abbbaaaaa with [2] abbaaaaab=abbbaaaaa:

abbaaaa ab abbaaaaab

Critical pair: abbaaaaabbbaaaaa=abbbaaaaabaaaaab.

Reduce LHS:

[2](abbaaaaab)bbaaaaa
[1]⇒ (abbbaaaaab)baaaaa
⇒ abaaaaa

Reduce RHS:

[1](abbbaaaaab)aaaaab
⇒ aaaaaab

Flip LHS and RHS.

Defines rule #1.