Certificate for #18711 ⟨a, b | aaa=a, aabbaa=b⟩

Back:⟨a, b | aaa=a, aabbaa=b⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #2.

Referenced by [3], [4].

[2] aabbaa=b

Axiom: aabbaa=b.

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

[3] aab=b

Overlap of [1] aaa=a with [2] aabbaa=b:

aa a aabbaa

Critical pair: aab=aabbaa.

Reduce RHS:

[2](aabbaa)
⇒ b

Defines rule #3.

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

[4] bba=ba

Overlap of [2] aabbaa=b with [1] aaa=a:

aabb aa aaa

Critical pair: aabba=ba.

Reduce LHS:

[3](aab)ba
⇒ bba

Referenced by [5], [6].

[5] bbb=baa

Overlap of [2] aabbaa=b with [2] aabbaa=b:

aabb aa aabbaa

Critical pair: aabbb=bbbaa.

Reduce LHS:

[3](aab)bb
⇒ bbb

Reduce RHS:

[4]b(bba)a
[4]⇒ (bba)a
⇒ baa

Referenced by [7].

[6] baa=b

Overlap of [2] aabbaa=b with [3] aab=b:

aabbaa aab

Critical pair: bbaa=b.

Reduce LHS:

[4](bba)a
⇒ baa

Defines rule #4.

Referenced by [7].

[7] bb=b

Overlap of [2] aabbaa=b with [3] aab=b:

aabb aa aab

Critical pair: aabbb=bb.

Reduce LHS:

[3](aab)bb
[5]⇒ (bbb)
[6]⇒ (baa)
⇒ b

Flip LHS and RHS.

Defines rule #1.