Certificate for #17680 ⟨a, b | aaaa=1, babbb=ba⟩

Back:⟨a, b | aaaa=1, babbb=ba⟩

Completion settings:

[1] aaaa=1

Axiom: aaaa=1.

Defines rule #1.

Referenced by [5].

[2] babbb=ba

Axiom: babbb=ba.

Defines rule #3.

Referenced by [3], [4].

[3] baabbb=baa

Overlap of [2] babbb=ba with [2] babbb=ba:

babb b babbb

Critical pair: babbba=baabbb.

Reduce LHS:

[2](babbb)a
⇒ baa

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] baaabbb=baaa

Overlap of [2] babbb=ba with [3] baabbb=baa:

babb b baabbb

Critical pair: babbbaa=baaabbb.

Reduce LHS:

[2](babbb)aa
⇒ baaa

Flip LHS and RHS.

Defines rule #5.

[5] bbbb=b

Overlap of [3] baabbb=baa with [3] baabbb=baa:

baabb b baabbb

Critical pair: baabbbaa=baaaabbb.

Reduce LHS:

[3](baabbb)aa
[1]⇒ b(aaaa)
⇒ b

Reduce RHS:

[1]b(aaaa)bbb
⇒ bbbb

Flip LHS and RHS.

Defines rule #2.