Certificate for #25250 ⟨a, b | aa=a, bbabb=aba⟩

Back:⟨a, b | aa=a, bbabb=aba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

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

[2] bbabb=aba

Axiom: bbabb=aba.

Defines rule #3.

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

[3] bbaba=ababb

Overlap of [2] bbabb=aba with [2] bbabb=aba:

bba bb bbabb

Critical pair: bbaaba=abaabb.

Reduce LHS:

[1]bb(aa)ba
⇒ bbaba

Reduce RHS:

[1]ab(aa)bb
⇒ ababb

Defines rule #2.

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

[4] ababbba=abababb

Overlap of [2] bbabb=aba with [2] bbabb=aba:

bbab b bbabb

Critical pair: bbababa=abababb.

Reduce LHS:

[3](bbaba)ba
⇒ ababbba

Defines rule #5.

[5] ababbbb=ababa

Overlap of [2] bbabb=aba with [3] bbaba=ababb:

bba bb bbaba

Critical pair: bbaababb=abaaba.

Reduce LHS:

[1]bb(aa)babb
[3]⇒ (bbaba)bb
⇒ ababbbb

Reduce RHS:

[1]ab(aa)ba
⇒ ababa

Defines rule #6.

[6] ababba=ababb

Overlap of [3] bbaba=ababb with [1] aa=a:

bbab a aa

Critical pair: bbaba=ababba.

Reduce LHS:

[3](bbaba)
⇒ ababb

Flip LHS and RHS.

Defines rule #4.