Certificate for #5327 ⟨a, b | aaa=ab, bab=aa⟩

Back:⟨a, b | aaa=ab, bab=aa⟩

Completion settings:

[1] ab=aaa

Axiom: aaa=ab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [2], [3].

[2] baaa=aa

Axiom: bab=aa.

Reduce LHS:

[1]b(ab)
⇒ baaa

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

[3] aaaaaa=aaa

Overlap of [1] ab=aaa with [2] baaa=aa:

a b baaa

Critical pair: aaa=aaaaaa.

Flip LHS and RHS.

Referenced by [4].

[4] aaaaa=aa

Overlap of [2] baaa=aa with [3] aaaaaa=aaa:

b aaa aaaaaa

Critical pair: baaa=aaaaa.

Reduce LHS:

[2](baaa)
⇒ aa

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] baa=aaaa

Overlap of [2] baaa=aa with [4] aaaaa=aa:

b aaa aaaaa

Critical pair: baa=aaaa.

Defines rule #2.