Certificate for #588 ⟨a, b | aab=a, bab=a⟩

Back:⟨a, b | aab=a, bab=a⟩

Completion settings:

[1] aab=a

Axiom: aab=a.

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

[2] bab=a

Axiom: bab=a.

Referenced by [3], [4].

[3] aaa=a

Overlap of [1] aab=a with [2] bab=a:

aa b bab

Critical pair: aaa=aab.

Reduce RHS:

[1](aab)
⇒ a

Defines rule #3.

Referenced by [5].

[4] baa=a

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

ba b bab

Critical pair: baa=aab.

Reduce RHS:

[1](aab)
⇒ a

Referenced by [6].

[5] ab=aa

Overlap of [3] aaa=a with [1] aab=a:

a aa aab

Critical pair: aa=ab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [6].

[6] ba=aa

Overlap of [4] baa=a with [1] aab=a:

b aa aab

Critical pair: ba=ab.

Reduce RHS:

[5](ab)
⇒ aa

Defines rule #2.