Certificate for #27679 ⟨a, b | aa=1, abbbab=bab⟩

Back:⟨a, b | aa=1, abbbab=bab⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [3].

[2] abbbab=bab

Axiom: abbbab=bab.

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

[3] bbbab=abab

Overlap of [1] aa=1 with [2] abbbab=bab:

a a abbbab

Critical pair: abab=bbbab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] babab=abbab

Overlap of [3] bbbab=abab with [2] abbbab=bab:

bbb ab abbbab

Critical pair: bbbbab=ababbbab.

Reduce LHS:

[3]b(bbbab)
⇒ babab

Reduce RHS:

[2]ab(abbbab)
⇒ abbab

Defines rule #2.

Referenced by [5].

[5] babbab=bab

Overlap of [4] babab=abbab with [2] abbbab=bab:

bab ab abbbab

Critical pair: babbab=abbabbbab.

Reduce RHS:

[2]abb(abbbab)
[2]⇒ (abbbab)
⇒ bab

Defines rule #4.