Certificate for #20168 ⟨a, b | aab=b, bbbb=aaa⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

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

[2] bbbb=aaa

Axiom: bbbb=aaa.

Defines rule #3.

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

[3] aaaaa=aaa

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

aa b bbbb

Critical pair: aaaaa=bbbb.

Reduce RHS:

[2](bbbb)
⇒ aaa

Defines rule #4.

[4] baaa=ab

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

b bbb bbbb

Critical pair: baaa=aaab.

Reduce RHS:

[1]a(aab)
⇒ ab

Referenced by [5], [6].

[5] bab=abb

Overlap of [4] baaa=ab with [1] aab=b:

ba aa aab

Critical pair: bab=abb.

Referenced by [6].

[6] aba=b

Overlap of [5] bab=abb with [2] bbbb=aaa:

ba b bbbb

Critical pair: baaaa=abbbbb.

Reduce LHS:

[4](baaa)a
⇒ aba

Reduce RHS:

[2]a(bbbb)b
[1]⇒ aa(aab)
[1]⇒ (aab)
⇒ b

Referenced by [7].

[7] ba=ab

Overlap of [1] aab=b with [6] aba=b:

a ab aba

Critical pair: ab=ba.

Flip LHS and RHS.

Defines rule #1.