Certificate for #13151 ⟨a, b | aba=aaa, baa=bb⟩

Back:⟨a, b | aba=aaa, baa=bb⟩

Completion settings:

[1] aba=aaa

Axiom: aba=aaa.

Defines rule #3.

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

[2] bb=baa

Axiom: baa=bb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [3].

[3] baab=baaaa

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

b b bb

Critical pair: bbaa=baab.

Reduce LHS:

[2](bb)aa
⇒ baaaa

Flip LHS and RHS.

Defines rule #6.

Referenced by [4], [5].

[4] aaaab=aaaaaa

Overlap of [1] aba=aaa with [3] baab=baaaa:

a ba baab

Critical pair: abaaaa=aaaab.

Reduce LHS:

[1](aba)aaa
⇒ aaaaaa

Flip LHS and RHS.

Defines rule #4.

[5] baaaaa=baaaa

Overlap of [3] baab=baaaa with [1] aba=aaa:

ba ab aba

Critical pair: baaaa=baaaaa.

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] aaaaaaa=aaaaaa

Overlap of [1] aba=aaa with [5] baaaaa=baaaa:

a ba baaaaa

Critical pair: abaaaa=aaaaaaa.

Reduce LHS:

[1](aba)aaa
⇒ aaaaaa

Flip LHS and RHS.

Defines rule #1.