Certificate for #6732 ⟨a, b | aba=a, aaab=bb⟩

Back:⟨a, b | aba=a, aaab=bb⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #3.

Referenced by [4], [5].

[2] bb=aaab

Axiom: aaab=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3].

[3] baaab=aaaaaab

Overlap of [2] bb=aaab with [2] bb=aaab:

b b bb

Critical pair: baaab=aaabb.

Reduce RHS:

[2]aaa(bb)
⇒ aaaaaab

Referenced by [4].

[4] baaa=aaaaaa

Overlap of [3] baaab=aaaaaab with [1] aba=a:

baa ab aba

Critical pair: baaa=aaaaaaba.

Reduce RHS:

[1]aaaaa(aba)
⇒ aaaaaa

Defines rule #2.

Referenced by [5].

[5] aaaaaaa=aaa

Overlap of [1] aba=a with [4] baaa=aaaaaa:

a ba baaa

Critical pair: aaaaaaa=aaa.

Defines rule #1.