Certificate for #24679 ⟨a, b | aa=a, abbbab=ba⟩

Back:⟨a, b | aa=a, abbbab=ba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [5].

[2] abbbab=ba

Axiom: abbbab=ba.

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

[3] aba=ba

Overlap of [1] aa=a with [2] abbbab=ba:

a a abbbab

Critical pair: aba=abbbab.

Reduce RHS:

[2](abbbab)
⇒ ba

Defines rule #2.

Referenced by [5], [6], [7], [10].

[4] babbab=abbbba

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

abbb ab abbbab

Critical pair: abbbba=babbab.

Flip LHS and RHS.

Referenced by [10].

[5] abbbba=ba

Overlap of [2] abbbab=ba with [3] aba=ba:

abbb ab aba

Critical pair: abbbba=baa.

Reduce RHS:

[1]b(aa)
⇒ ba

Referenced by [8].

[6] abba=bba

Overlap of [3] aba=ba with [2] abbbab=ba:

ab a abbbab

Critical pair: abba=babbbab.

Reduce RHS:

[2]b(abbbab)
⇒ bba

Referenced by [7], [8], [10].

[7] abbba=bbba

Overlap of [3] aba=ba with [6] abba=bba:

ab a abba

Critical pair: abbba=babba.

Reduce RHS:

[6]b(abba)
⇒ bbba

Referenced by [9].

[8] bbbba=ba

Overlap of [6] abba=bba with [6] abba=bba:

abb a abba

Critical pair: abbbba=bbabba.

Reduce LHS:

[5](abbbba)
⇒ ba

Reduce RHS:

[6]bb(abba)
⇒ bbbba

Flip LHS and RHS.

Referenced by [9], [10].

[9] bba=bab

Overlap of [8] bbbba=ba with [2] abbbab=ba:

bbbb a abbbab

Critical pair: bbbbba=babbbab.

Reduce LHS:

[8]b(bbbba)
⇒ bba

Reduce RHS:

[7]b(abbba)b
[8]⇒ (bbbba)b
⇒ bab

Defines rule #3.

Referenced by [10].

[10] babbb=ba

Simplify [4] babbab=abbbba.

Reduce LHS:

[6]b(abba)b
[9]⇒ b(bba)b
[9]⇒ (bba)bb
⇒ babbb

Reduce RHS:

[8]a(bbbba)
[3]⇒ (aba)
⇒ ba

Defines rule #4.