Certificate for #16532 ⟨a, b | aba=aa, bbb=aaa⟩

Back:⟨a, b | aba=aa, bbb=aaa⟩

Completion settings:

[1] aba=aa

Axiom: aba=aa.

Defines rule #1.

Referenced by [4], [5].

[2] bbb=aaa

Axiom: bbb=aaa.

Defines rule #2.

Referenced by [3], [6].

[3] baaa=aaab

Overlap of [2] bbb=aaa with [2] bbb=aaa:

b bb bbb

Critical pair: baaa=aaab.

Defines rule #3.

Referenced by [4], [5].

[4] aaaab=aaaa

Overlap of [1] aba=aa with [3] baaa=aaab:

a ba baaa

Critical pair: aaaab=aaaa.

Defines rule #4.

Referenced by [6].

[5] aaabba=aaaa

Overlap of [3] baaa=aaab with [1] aba=aa:

baa a aba

Critical pair: baaaa=aaabba.

Reduce LHS:

[3](baaa)a
[1]⇒ aa(aba)
⇒ aaaa

Flip LHS and RHS.

Defines rule #5.

[6] aaaaaaa=aaaa

Overlap of [4] aaaab=aaaa with [2] bbb=aaa:

aaaa b bbb

Critical pair: aaaaaaa=aaaabb.

Reduce RHS:

[4](aaaab)b
[4]⇒ (aaaab)
⇒ aaaa

Defines rule #6.