Certificate for #12259 ⟨a, b | aaab=ab, baba=b⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b

[1] aaab=ab

Axiom: aaab=ab.

Defines rule #4.

Referenced by [4], [5].

[2] baba=b

Axiom: baba=b.

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

[3] bba=bab

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

ba ba baba

Critical pair: bab=bba.

Flip LHS and RHS.

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

[4] baab=bb

Overlap of [2] baba=b with [1] aaab=ab:

bab a aaab

Critical pair: babab=baab.

Reduce LHS:

[2]	(baba)b
	⇒ bb

Flip LHS and RHS.

Referenced by [6], [7].

[5] babb=bab

Overlap of [3] bba=bab with [1] aaab=ab:

bb a aaab

Critical pair: bbab=babaab.

Reduce LHS:

[3]	(bba)b
	⇒ babb

Reduce RHS:

[2]	(baba)ab
	⇒ bab

Referenced by [6].

[6] bb=b

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

baa b baba

Critical pair: baab=bbaba.

Reduce LHS:

[4]	(baab)
	⇒ bb

Reduce RHS:

[3]	(bba)ba
[5]	⇒ (babb)a
[2]	⇒ (baba)
	⇒ b

Defines rule #1.

Referenced by [7], [8].

[7] bab=ba

Overlap of [4] baab=bb with [3] bba=bab:

baa b bba

Critical pair: baabab=bbba.

Reduce LHS:

[4]	(baab)ab
[6]	⇒ (bb)ab
	⇒ bab

Reduce RHS:

[6]	(bb)ba
[6]	⇒ (bb)a
	⇒ ba

Defines rule #3.

Referenced by [8].

[8] baa=b

Overlap of [6] bb=b with [2] baba=b:

b b baba

Critical pair: bb=baba.

Reduce LHS:

[6]	(bb)
	⇒ b

Reduce RHS:

[7]	(bab)a
	⇒ baa

Flip LHS and RHS.

Defines rule #2.