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

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

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #1.

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

[2] bbabb=aa

Axiom: bbabb=aa.

Defines rule #4.

Referenced by [3], [4].

[3] bbaa=aabb

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

bbab b bbabb

Critical pair: bbabaa=aababb.

Reduce LHS:

[1]bb(aba)a
⇒ bbaa

Reduce RHS:

[1]a(aba)bb
⇒ aabb

Defines rule #2.

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

[4] aabbbb=aaa

Overlap of [2] bbabb=aa with [3] bbaa=aabb:

bbab b bbaa

Critical pair: bbabaabb=aabaa.

Reduce LHS:

[1]bb(aba)abb
[3]⇒ (bbaa)bb
⇒ aabbbb

Reduce RHS:

[1]a(aba)a
⇒ aaa

Defines rule #6.

Referenced by [6].

[5] aabbba=aabb

Overlap of [3] bbaa=aabb with [1] aba=a:

bba a aba

Critical pair: bbaa=aabbba.

Reduce LHS:

[3](bbaa)
⇒ aabb

Flip LHS and RHS.

Defines rule #5.

[6] aabba=aaabb

Overlap of [3] bbaa=aabb with [4] aabbbb=aaa:

bb aa aabbbb

Critical pair: bbaaa=aabbbbbb.

Reduce LHS:

[3](bbaa)a
⇒ aabba

Reduce RHS:

[4](aabbbb)bb
⇒ aaabb

Defines rule #3.