Certificate for #20038 ⟨a, b | aab=a, bbba=bba⟩

Back:⟨a, b | aab=a, bbba=bba⟩

Completion settings:

[1] aab=a

Axiom: aab=a.

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

[2] bbba=bba

Axiom: bbba=bba.

Defines rule #3.

Referenced by [3].

[3] abba=aba

Overlap of [1] aab=a with [2] bbba=bba:

aa b bbba

Critical pair: aabba=abba.

Reduce LHS:

[1](aab)ba
⇒ aba

Flip LHS and RHS.

Referenced by [4].

[4] aba=aa

Overlap of [1] aab=a with [3] abba=aba:

a ab abba

Critical pair: aaba=aba.

Reduce LHS:

[1](aab)a
⇒ aa

Flip LHS and RHS.

Referenced by [5], [6].

[5] aaa=aa

Overlap of [1] aab=a with [4] aba=aa:

a ab aba

Critical pair: aaa=aa.

Referenced by [6].

[6] aa=a

Overlap of [4] aba=aa with [1] aab=a:

ab a aab

Critical pair: aba=aaab.

Reduce LHS:

[4](aba)
⇒ aa

Reduce RHS:

[5](aaa)b
[1]⇒ (aab)
⇒ a

Defines rule #1.

Referenced by [7].

[7] ab=a

Overlap of [1] aab=a with [6] aa=a:

aab aa

Critical pair: ab=a.

Defines rule #2.