Certificate for #20202 ⟨a, b | aba=a, aabb=baa⟩

Completion settings:

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

[1] aba=a

Axiom: aba=a.

Defines rule #2.

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

[2] aabb=baa

Axiom: aabb=baa.

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

[3] abbaa=baa

Overlap of [1] aba=a with [2] aabb=baa:

ab a aabb

Critical pair: abbaa=aabb.

Reduce RHS:

[2]	(aabb)
	⇒ baa

Referenced by [4].

[4] baaaa=aa

Overlap of [2] aabb=baa with [3] abbaa=baa:

a abb abbaa

Critical pair: abaa=baaaa.

Reduce LHS:

[1]	(aba)a
	⇒ aa

Flip LHS and RHS.

Referenced by [5], [6].

[5] baaa=baa

Overlap of [4] baaaa=aa with [2] aabb=baa:

baa aa aabb

Critical pair: baabaa=aabb.

Reduce LHS:

[1]	ba(aba)a
	⇒ baaa

Reduce RHS:

[2]	(aabb)
	⇒ baa

Referenced by [6].

[6] baa=aa

Overlap of [4] baaaa=aa with [2] aabb=baa:

baaa a aabb

Critical pair: baaabaa=aaabb.

Reduce LHS:

[5]	(baaa)baa
[1]	⇒ ba(aba)a
[5]	⇒ (baaa)
	⇒ baa

Reduce RHS:

[2]	a(aabb)
[1]	⇒ (aba)a
	⇒ aa

Defines rule #3.

Referenced by [7], [8].

[7] aaa=aa

Overlap of [1] aba=a with [6] baa=aa:

a ba baa

Critical pair: aaa=aa.

Defines rule #1.

[8] aabb=aa

Simplify [2] aabb=baa.

Reduce RHS:

[6]	(baa)
	⇒ aa

Defines rule #4.