Certificate for #28270 ⟨a, b | aa=1, babbb=baba⟩

Back:⟨a, b | aa=1, babbb=baba⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [3], [4].

[2] babbb=baba

Axiom: babbb=baba.

Defines rule #2.

Referenced by [3], [4].

[3] babab=babba

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

babb b babbb

Critical pair: babbbaba=babaabbb.

Reduce LHS:

[2](babbb)aba
[1]⇒ bab(aa)ba
⇒ babba

Reduce RHS:

[1]bab(aa)bbb
[2]⇒ (babbb)b
⇒ babab

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] babbab=bab

Overlap of [2] babbb=baba with [3] babab=babba:

babb b babab

Critical pair: babbbabba=babaabab.

Reduce LHS:

[2](babbb)abba
[1]⇒ bab(aa)bba
[2]⇒ (babbb)a
[1]⇒ bab(aa)
⇒ bab

Reduce RHS:

[1]bab(aa)bab
⇒ babbab

Flip LHS and RHS.

Defines rule #4.