Certificate for #12984 ⟨a, b | abb=aaa, baba=a⟩

Back:⟨a, b | abb=aaa, baba=a⟩

Completion settings:

[1] abb=aaa

Axiom: abb=aaa.

Defines rule #4.

Referenced by [4].

[2] baba=a

Axiom: baba=a.

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

[3] aba=baa

Overlap of [2] baba=a with [2] baba=a:

ba ba baba

Critical pair: baa=aba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] aaaaa=aa

Overlap of [3] aba=baa with [3] aba=baa:

ab a aba

Critical pair: abbaa=baaba.

Reduce LHS:

[1](abb)aa
⇒ aaaaa

Reduce RHS:

[3]ba(aba)
[2]⇒ (baba)a
⇒ aa

Referenced by [6].

[5] bbaa=a

Overlap of [2] baba=a with [3] aba=baa:

b aba aba

Critical pair: bbaa=a.

Referenced by [6], [7].

[6] aaaa=a

Overlap of [5] bbaa=a with [4] aaaaa=aa:

bb aa aaaaa

Critical pair: bbaa=aaaa.

Reduce LHS:

[5](bbaa)
⇒ a

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] bba=aaa

Overlap of [5] bbaa=a with [6] aaaa=a:

bb aa aaaa

Critical pair: bba=aaa.

Defines rule #3.