Certificate for #995 ⟨a, b | ab=a, aaa=bb⟩

Back:⟨a, b | ab=a, aaa=bb⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #3.

Referenced by [3], [4].

[2] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[3] aaaa=a

Overlap of [1] ab=a with [2] bb=aaa:

a b bb

Critical pair: aaaa=ab.

Reduce RHS:

[1](ab)
⇒ a

Defines rule #1.

Referenced by [5].

[4] baaa=aaa

Overlap of [2] bb=aaa with [2] bb=aaa:

b b bb

Critical pair: baaa=aaab.

Reduce RHS:

[1]aa(ab)
⇒ aaa

Referenced by [5].

[5] ba=a

Overlap of [4] baaa=aaa with [3] aaaa=a:

b aaa aaaa

Critical pair: ba=aaaa.

Reduce RHS:

[3](aaaa)
⇒ a

Defines rule #2.