Certificate for #2104 ⟨a, b | aba=b, aaaa=a⟩

Back:⟨a, b | aba=b, aaaa=a⟩

Completion settings:

[1] aba=b

Axiom: aba=b.

Referenced by [3], [4].

[2] aaaa=a

Axiom: aaaa=a.

Defines rule #1.

Referenced by [3].

[3] baaa=b

Overlap of [1] aba=b with [2] aaaa=a:

ab a aaaa

Critical pair: aba=baaa.

Reduce LHS:

[1](aba)
⇒ b

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] ab=baa

Overlap of [1] aba=b with [3] baaa=b:

a ba baaa

Critical pair: ab=baa.

Defines rule #3.