Certificate for #4095 ⟨a, b | baa=abb, abab=1⟩

Completion settings:

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

[1] baa=abb

Axiom: baa=abb.

Defines rule #1.

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

[2] abab=1

Axiom: abab=1.

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

[3] abbbab=ba

Overlap of [1] baa=abb with [2] abab=1:

ba a abab

Critical pair: ba=abbbab.

Flip LHS and RHS.

Referenced by [5].

[4] aabbbb=aa

Overlap of [2] abab=1 with [1] baa=abb:

aba b baa

Critical pair: abaabb=aa.

Reduce LHS:

[1]	a(baa)bb
	⇒ aabbbb

Referenced by [5], [7].

[5] aaaa=1

Overlap of [4] aabbbb=aa with [1] baa=abb:

aabbb b baa

Critical pair: aabbbabb=aaaa.

Reduce LHS:

[3]	a(abbbab)b
[2]	⇒ (abab)
	⇒ 1

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[6] bab=aaa

Overlap of [5] aaaa=1 with [2] abab=1:

aaa a abab

Critical pair: aaa=bab.

Flip LHS and RHS.

Defines rule #2.

[7] bbbb=1

Overlap of [5] aaaa=1 with [4] aabbbb=aa:

aa aa aabbbb

Critical pair: aaaa=bbbb.

Reduce LHS:

[5]	(aaaa)
	⇒ 1

Flip LHS and RHS.

Referenced by [8].

[8] bbb=aba

Overlap of [2] abab=1 with [7] bbbb=1:

aba b bbbb

Critical pair: aba=bbb.

Flip LHS and RHS.

Defines rule #3.