Certificate for #12207 ⟨a, b | aaaa=bb, abbb=b⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b

[1] aaaa=bb

Axiom: aaaa=bb.

Defines rule #2.

Referenced by [3], [4].

[2] abbb=b

Axiom: abbb=b.

Defines rule #3.

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

[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 [5], [7], [8].

[4] bbbbb=aaab

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

aaa a abbb

Critical pair: aaab=bbbbb.

Flip LHS and RHS.

Defines rule #4.

[5] ababb=ba

Overlap of [2] abbb=b with [3] bba=abb:

ab bb bba

Critical pair: ababb=ba.

Referenced by [6].

[6] bab=abb

Overlap of [5] ababb=ba with [2] abbb=b:

ab abb abbb

Critical pair: abb=bab.

Flip LHS and RHS.

Referenced by [7], [8].

[7] baabb=ba

Overlap of [6] bab=abb with [3] bba=abb:

ba b bba

Critical pair: baabb=abbba.

Reduce RHS:

[2]	(abbb)a
	⇒ ba

Referenced by [8].

[8] ba=ab

Overlap of [6] bab=abb with [6] bab=abb:

ba b bab

Critical pair: baabb=abbab.

Reduce LHS:

[7]	(baabb)
	⇒ ba

Reduce RHS:

[3]	a(bba)b
[2]	⇒ a(abbb)
	⇒ ab

Defines rule #1.