Certificate for #6828 ⟨a, b | aba=a, baa=aab⟩

Completion settings:

Auxiliary generators:
1. c = aabbb
Reduction order:
- Left-to-right shortlex with a < c < b

[1] aba=a

Axiom: aba=a.

Defines rule #6.

Referenced by [4], [5], [6], [8], [9], [13].

[2] baa=aab

Axiom: baa=aab.

Referenced by [4], [5], [7], [8], [9], [17], [19].

[3] aabbb=c

Axiom: aabbb=c.

Referenced by [6], [7], [8], [9], [10], [12], [14].

[4] aaab=aa

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

a ba baa

Critical pair: aaab=aa.

Referenced by [10], [18], [20].

[5] aabba=aab

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

ba a aba

Critical pair: baa=aabba.

Reduce LHS:

[2]	(baa)
	⇒ aab

Flip LHS and RHS.

Referenced by [9].

[6] abc=c

Overlap of [1] aba=a with [3] aabbb=c:

ab a aabbb

Critical pair: abc=aabbb.

Reduce RHS:

[3]	(aabbb)
	⇒ c

Referenced by [11].

[7] bc=cb

Overlap of [2] baa=aab with [3] aabbb=c:

b aa aabbb

Critical pair: bc=aabbbb.

Reduce RHS:

[3]	(aabbb)b
	⇒ cb

Referenced by [11], [15], [16].

[8] bac=c

Overlap of [2] baa=aab with [3] aabbb=c:

ba a aabbb

Critical pair: bac=aababbb.

Reduce RHS:

[1]	a(aba)bbb
[3]	⇒ (aabbb)
	⇒ c

Defines rule #8.

Referenced by [12], [17].

[9] caa=aab

Overlap of [3] aabbb=c with [2] baa=aab:

aabb b baa

Critical pair: aabbaab=caa.

Reduce LHS:

[5]	(aabba)ab
[1]	⇒ a(aba)b
	⇒ aab

Flip LHS and RHS.

Referenced by [13], [14], [15].

[10] aabb=ac

Overlap of [4] aaab=aa with [3] aabbb=c:

a aab aabbb

Critical pair: ac=aabb.

Flip LHS and RHS.

Referenced by [12], [13], [14], [17], [18].

[11] acb=c

Simplify [6] abc=c.

Reduce LHS:

[7]	a(bc)
	⇒ acb

Referenced by [14], [15].

[12] cac=acc

Overlap of [3] aabbb=c with [8] bac=c:

aabb b bac

Critical pair: aabbc=cac.

Reduce LHS:

[10]	(aabb)c
	⇒ acc

Flip LHS and RHS.

Referenced by [15].

[13] aca=aab

Overlap of [9] caa=aab with [1] aba=a:

ca a aba

Critical pair: caa=aabba.

Reduce LHS:

[9]	(caa)
	⇒ aab

Reduce RHS:

[10]	(aabb)a
	⇒ aca

Flip LHS and RHS.

Referenced by [17].

[14] cb=cc

Overlap of [9] caa=aab with [3] aabbb=c:

c aa aabbb

Critical pair: cc=aabbbb.

Reduce RHS:

[10]	(aabb)bb
[11]	⇒ (acb)b
	⇒ cb

Flip LHS and RHS.

Defines rule #2.

Referenced by [16].

[15] acc=c

Overlap of [9] caa=aab with [11] acb=c:

ca a acb

Critical pair: cac=aabcb.

Reduce LHS:

[12]	(cac)
	⇒ acc

Reduce RHS:

[7]	aa(bc)b
[11]	⇒ a(acb)b
[11]	⇒ (acb)
	⇒ c

Defines rule #5.

[16] bc=cc

Simplify [7] bc=cb.

Reduce RHS:

[14]	(cb)
	⇒ cc

Defines rule #3.

[17] ca=ac

Overlap of [8] bac=c with [13] aca=aab:

b ac aca

Critical pair: baab=ca.

Reduce LHS:

[2]	(baa)b
[10]	⇒ (aabb)
	⇒ ac

Flip LHS and RHS.

Defines rule #1.

[18] aab=aac

Overlap of [4] aaab=aa with [10] aabb=ac:

a aab aabb

Critical pair: aac=aab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [19], [20].

[19] baa=aac

Simplify [2] baa=aab.

Reduce RHS:

[18]	(aab)
	⇒ aac

Defines rule #7.

[20] aaac=aa

Overlap of [4] aaab=aa with [18] aab=aac:

a aab aab

Critical pair: aaac=aa.

Defines rule #9.