Certificate for #12197 ⟨a, b | aaaa=bb, aaab=b⟩

Back:⟨a, b | aaaa=bb, aaab=b⟩

Completion settings:

[1] aaaa=bb

Axiom: aaaa=bb.

Defines rule #3.

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

[2] aaab=b

Axiom: aaab=b.

Defines rule #4.

Referenced by [4], [7].

[3] bba=abb

Overlap of [1] aaaa=bb with [1] aaaa=bb:

a aaa aaaa

Critical pair: abb=bba.

Flip LHS and RHS.

Referenced by [6].

[4] bbb=ab

Overlap of [1] aaaa=bb with [2] aaab=b:

a aaa aaab

Critical pair: ab=bbb.

Flip LHS and RHS.

Defines rule #2.

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

[5] bab=abb

Overlap of [4] bbb=ab with [4] bbb=ab:

b bb bbb

Critical pair: bab=abb.

Referenced by [6].

[6] aba=aab

Overlap of [4] bbb=ab with [3] bba=abb:

b bb bba

Critical pair: babb=aba.

Reduce LHS:

[5](bab)b
[4]⇒ a(bbb)
⇒ aab

Flip LHS and RHS.

Referenced by [7].

[7] ba=ab

Overlap of [2] aaab=b with [6] aba=aab:

aa ab aba

Critical pair: aaaab=ba.

Reduce LHS:

[1](aaaa)b
[4]⇒ (bbb)
⇒ ab

Flip LHS and RHS.

Defines rule #1.