Certificate for #19694 ⟨a, b | aba=a, babbb=aa⟩

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

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #3.

Referenced by [3], [6].

[2] babbb=aa

Axiom: babbb=aa.

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

[3] abbb=aaa

Overlap of [1] aba=a with [2] babbb=aa:

a ba babbb

Critical pair: aaa=abbb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] abbaa=aaaaaa

Overlap of [3] abbb=aaa with [2] babbb=aa:

abb b babbb

Critical pair: abbaa=aaaabbb.

Reduce RHS:

[3]aaa(abbb)
⇒ aaaaaa

Referenced by [6].

[5] baaa=aa

Overlap of [2] babbb=aa with [3] abbb=aaa:

b abbb abbb

Critical pair: baaa=aa.

Referenced by [6], [7].

[6] aaaaaaa=aa

Overlap of [4] abbaa=aaaaaa with [5] baaa=aa:

ab baa baaa

Critical pair: abaa=aaaaaaa.

Reduce LHS:

[1](aba)a
⇒ aa

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] baa=aaaaaa

Overlap of [5] baaa=aa with [6] aaaaaaa=aa:

b aaa aaaaaaa

Critical pair: baa=aaaaaa.

Defines rule #2.