Certificate for #5399 ⟨a, b | aab=ba, bab=ab⟩

Completion settings:

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

[1] aab=ba

Axiom: aab=ba.

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

[2] bab=ab

Axiom: bab=ab.

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

[3] bba=aba

Overlap of [1] aab=ba with [2] bab=ab:

aa b bab

Critical pair: aaab=baab.

Reduce LHS:

[1]	a(aab)
	⇒ aba

Reduce RHS:

[1]	b(aab)
	⇒ bba

Flip LHS and RHS.

Referenced by [4], [6].

[4] aba=ba

Overlap of [2] bab=ab with [2] bab=ab:

ba b bab

Critical pair: baab=abab.

Reduce LHS:

[1]	b(aab)
[3]	⇒ (bba)
	⇒ aba

Reduce RHS:

[2]	a(bab)
[1]	⇒ (aab)
	⇒ ba

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

[5] baa=ba

Overlap of [1] aab=ba with [4] aba=ba:

a ab aba

Critical pair: aba=baa.

Reduce LHS:

[4]	(aba)
	⇒ ba

Flip LHS and RHS.

Referenced by [6].

[6] ba=ab

Overlap of [4] aba=ba with [1] aab=ba:

ab a aab

Critical pair: abba=baab.

Reduce LHS:

[3]	a(bba)
[1]	⇒ (aab)a
[5]	⇒ (baa)
	⇒ ba

Reduce RHS:

[5]	(baa)b
[2]	⇒ (bab)
	⇒ ab

Defines rule #1.

Referenced by [7], [8].

[7] abb=ab

Overlap of [4] aba=ba with [2] bab=ab:

a ba bab

Critical pair: aab=bab.

Reduce LHS:

[1]	(aab)
[6]	⇒ (ba)
	⇒ ab

Reduce RHS:

[6]	(ba)b
	⇒ abb

Flip LHS and RHS.

Defines rule #3.

[8] aab=ab

Simplify [1] aab=ba.

Reduce RHS:

[6]	(ba)
	⇒ ab

Defines rule #2.