Certificate for #19490 ⟨a, b | aab=a, bbbaa=ba⟩

Back:⟨a, b | aab=a, bbbaa=ba⟩

Completion settings:

[1] aab=a

Axiom: aab=a.

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

[2] bbbaa=ba

Axiom: bbbaa=ba.

Referenced by [3], [4].

[3] bbba=bab

Overlap of [2] bbbaa=ba with [1] aab=a:

bbb aa aab

Critical pair: bbba=bab.

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

[4] baba=ba

Overlap of [2] bbbaa=ba with [1] aab=a:

bbba a aab

Critical pair: bbbaa=baab.

Reduce LHS:

[3](bbba)a
⇒ baba

Reduce RHS:

[1]b(aab)
⇒ ba

Referenced by [6].

[5] abba=a

Overlap of [1] aab=a with [3] bbba=bab:

aa b bbba

Critical pair: aabab=abba.

Reduce LHS:

[1](aab)ab
[1]⇒ (aab)
⇒ a

Flip LHS and RHS.

Referenced by [6].

[6] bab=ba

Overlap of [3] bbba=bab with [4] baba=ba:

bb ba baba

Critical pair: bbba=babba.

Reduce LHS:

[3](bbba)
⇒ bab

Reduce RHS:

[5]b(abba)
⇒ ba

Referenced by [7], [9].

[7] aa=a

Overlap of [1] aab=a with [6] bab=ba:

aa b bab

Critical pair: aaba=aab.

Reduce LHS:

[1](aab)a
⇒ aa

Reduce RHS:

[1](aab)
⇒ a

Defines rule #1.

Referenced by [8].

[8] ab=a

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

aab aa

Critical pair: ab=a.

Defines rule #2.

[9] bbba=ba

Simplify [3] bbba=bab.

Reduce RHS:

[6](bab)
⇒ ba

Defines rule #3.