Certificate for #14510 ⟨a, b | aaab=b, baaba=b⟩

Back:⟨a, b | aaab=b, baaba=b⟩

Completion settings:

[1] aaab=b

Axiom: aaab=b.

Defines rule #3.

Referenced by [3].

[2] baaba=b

Axiom: baaba=b.

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

[3] baabb=baab

Overlap of [2] baaba=b with [1] aaab=b:

baab a aaab

Critical pair: baabb=baab.

Referenced by [6].

[4] baba=baab

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

baa ba baaba

Critical pair: baab=baba.

Flip LHS and RHS.

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

[5] bba=bab

Overlap of [2] baaba=b with [4] baba=baab:

baa ba baba

Critical pair: baabaab=bba.

Reduce LHS:

[2](baaba)ab
⇒ bab

Flip LHS and RHS.

Referenced by [7].

[6] bb=b

Overlap of [4] baba=baab with [4] baba=baab:

ba ba baba

Critical pair: babaab=baabba.

Reduce LHS:

[4](baba)ab
[2]⇒ (baaba)b
⇒ bb

Reduce RHS:

[3](baabb)a
[2]⇒ (baaba)
⇒ b

Defines rule #1.

Referenced by [7].

[7] bab=ba

Simplify [5] bba=bab.

Reduce LHS:

[6](bb)a
⇒ ba

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[8] baab=baa

Overlap of [4] baba=baab with [7] bab=ba:

baba bab

Critical pair: baa=baab.

Flip LHS and RHS.

Defines rule #5.

Referenced by [9].

[9] baaa=b

Overlap of [2] baaba=b with [8] baab=baa:

baaba baab

Critical pair: baaa=b.

Defines rule #4.