Certificate for #19041 ⟨a, b | aab=b, babaaa=b⟩

Completion settings:

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

[1] aab=b

Axiom: aab=b.

Defines rule #2.

Referenced by [3], [4].

[2] babaaa=b

Axiom: babaaa=b.

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

[3] babab=bb

Overlap of [2] babaaa=b with [1] aab=b:

baba aa aab

Critical pair: babab=bb.

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

[4] babb=bab

Overlap of [2] babaaa=b with [1] aab=b:

babaa a aab

Critical pair: babaab=bab.

Reduce LHS:

[1]	bab(aab)
	⇒ babb

Referenced by [5], [6].

[5] bbaaa=bab

Overlap of [4] babb=bab with [2] babaaa=b:

bab b babaaa

Critical pair: babb=bababaaa.

Reduce LHS:

[4]	(babb)
	⇒ bab

Reduce RHS:

[3]	(babab)aaa
	⇒ bbaaa

Flip LHS and RHS.

Referenced by [8].

[6] bbab=bab

Overlap of [3] babab=bb with [3] babab=bb:

ba bab babab

Critical pair: babb=bbab.

Reduce LHS:

[4]	(babb)
	⇒ bab

Flip LHS and RHS.

Referenced by [7].

[7] bb=b

Overlap of [6] bbab=bab with [2] babaaa=b:

b bab babaaa

Critical pair: bb=babaaa.

Reduce RHS:

[2]	(babaaa)
	⇒ b

Defines rule #1.

Referenced by [8], [9].

[8] baaa=bab

Simplify [5] bbaaa=bab.

Reduce LHS:

[7]	(bb)aaa
	⇒ baaa

Defines rule #3.

[9] babab=b

Simplify [3] babab=bb.

Reduce RHS:

[7]	(bb)
	⇒ b

Defines rule #4.