Certificate for #12954 ⟨a, b | aba=aab, babb=a⟩

Back:⟨a, b | aba=aab, babb=a⟩

Completion settings:

[1] aba=aab

Axiom: aba=aab.

Defines rule #1.

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

[2] babb=a

Axiom: babb=a.

Defines rule #3.

Referenced by [3], [5].

[3] baab=aabb

Overlap of [2] babb=a with [2] babb=a:

bab b babb

Critical pair: baba=aabb.

Reduce LHS:

[1]b(aba)
⇒ baab

Referenced by [6].

[4] aabba=aaabb

Overlap of [1] aba=aab with [1] aba=aab:

ab a aba

Critical pair: abaab=aabba.

Reduce LHS:

[1](aba)ab
[1]⇒ a(aba)b
⇒ aaabb

Flip LHS and RHS.

Defines rule #4.

[5] aabbb=aa

Overlap of [1] aba=aab with [2] babb=a:

a ba babb

Critical pair: aa=aabbb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [6].

[6] baa=aab

Overlap of [3] baab=aabb with [5] aabbb=aa:

b aab aabbb

Critical pair: baa=aabbbb.

Reduce RHS:

[5](aabbb)b
⇒ aab

Defines rule #2.