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

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

Completion settings:

[1] aba=aa

Axiom: aba=aa.

Defines rule #3.

Referenced by [4], [5], [6].

[2] bb=aaab

Axiom: aaab=bb.

Flip LHS and RHS.

Defines rule #5.

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

Defines rule #6.

Referenced by [4], [5].

[4] aaaaaaab=aaaab

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

a ba baaab

Critical pair: aaaaaaab=aaaab.

Defines rule #4.

[5] baaaa=aaaaaaa

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

baa ab aba

Critical pair: baaaa=aaaaaaba.

Reduce RHS:

[1]aaaaa(aba)
⇒ aaaaaaa

Defines rule #2.

Referenced by [6].

[6] aaaaaaaa=aaaaa

Overlap of [1] aba=aa with [5] baaaa=aaaaaaa:

a ba baaaa

Critical pair: aaaaaaaa=aaaaa.

Defines rule #1.