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

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

Completion settings:

[1] aab=a

Axiom: aab=a.

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

[2] bbbaa=a

Axiom: bbbaa=a.

Referenced by [3], [4].

[3] bbba=ab

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

bbb aa aab

Critical pair: bbba=ab.

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

[4] aba=a

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

bbba a aab

Critical pair: bbbaa=aab.

Reduce LHS:

[3](bbba)a
⇒ aba

Reduce RHS:

[1](aab)
⇒ a

Referenced by [6].

[5] abba=aa

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

aa b bbba

Critical pair: aaab=abba.

Reduce LHS:

[1]a(aab)
⇒ aa

Flip LHS and RHS.

Referenced by [6].

[6] ab=aa

Overlap of [3] bbba=ab with [4] aba=a:

bbb a aba

Critical pair: bbba=abba.

Reduce LHS:

[3](bbba)
⇒ ab

Reduce RHS:

[5](abba)
⇒ aa

Defines rule #1.

Referenced by [7], [8].

[7] aaa=a

Overlap of [3] bbba=ab with [6] ab=aa:

bbb a ab

Critical pair: bbbaa=abb.

Reduce LHS:

[3](bbba)a
[6]⇒ (ab)a
⇒ aaa

Reduce RHS:

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

Defines rule #2.

[8] bbba=aa

Simplify [3] bbba=ab.

Reduce RHS:

[6](ab)
⇒ aa

Defines rule #3.