Certificate for #20160 ⟨a, b | aab=b, bbba=aaa⟩

Back:⟨a, b | aab=b, bbba=aaa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3], [4].

[2] bbba=aaa

Axiom: bbba=aaa.

Defines rule #3.

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

[3] aaaaa=aaa

Overlap of [1] aab=b with [2] bbba=aaa:

aa b bbba

Critical pair: aaaaa=bbba.

Reduce RHS:

[2](bbba)
⇒ aaa

Defines rule #5.

[4] bbbb=b

Overlap of [2] bbba=aaa with [1] aab=b:

bbb a aab

Critical pair: bbbb=aaaab.

Reduce RHS:

[1]aa(aab)
[1]⇒ (aab)
⇒ b

Defines rule #4.

Referenced by [5].

[5] baaa=ba

Overlap of [4] bbbb=b with [2] bbba=aaa:

b bbb bbba

Critical pair: baaa=ba.

Defines rule #2.