Certificate for #25652 ⟨a, b | ab=a, bbbbb=aaa⟩

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

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3], [4].

[2] bbbbb=aaa

Axiom: bbbbb=aaa.

Defines rule #4.

Referenced by [3], [4].

[3] aaaa=a

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

a b bbbbb

Critical pair: aaaa=abbbb.

Reduce RHS:

[1](ab)bbb
[1]⇒ (ab)bb
[1]⇒ (ab)b
[1]⇒ (ab)
⇒ a

Defines rule #3.

Referenced by [5].

[4] baaa=aaa

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

b bbbb bbbbb

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.