Certificate for #9785 ⟨a, b | aa=1, babbbab=b⟩

Completion settings:

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

[1] aa=1

Axiom: aa=1.

Defines rule #3.

[2] babbbab=b

Axiom: babbbab=b.

Referenced by [4].

[3] bb=c

Axiom: bb=c.

Defines rule #1.

Referenced by [4], [5], [7], [8], [14], [15], [16].

[4] bacbab=b

Overlap of [2] babbbab=b with [3] bb=c:

ba bbbab bb

Critical pair: bacbab=b.

Referenced by [6].

[5] cb=bc

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

b b bb

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #2.

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

[6] babcab=b

Simplify [4] bacbab=b.

Reduce LHS:

[5]	ba(cb)ab
	⇒ babcab

Referenced by [7], [8], [9], [12].

[7] cabcab=c

Overlap of [3] bb=c with [6] babcab=b:

b b babcab

Critical pair: bb=cabcab.

Reduce LHS:

[3]	(bb)
	⇒ c

Flip LHS and RHS.

Referenced by [9], [10], [11].

[8] babcac=c

Overlap of [6] babcab=b with [3] bb=c:

babca b bb

Critical pair: babcac=bb.

Reduce RHS:

[3]	(bb)
	⇒ c

Referenced by [11], [13].

[9] babc=bcab

Overlap of [6] babcab=b with [7] cabcab=c:

bab cab cabcab

Critical pair: babc=bcab.

Defines rule #4.

Referenced by [11], [12], [13], [14], [19].

[10] cabc=ccab

Overlap of [7] cabcab=c with [7] cabcab=c:

cab cab cabcab

Critical pair: cabc=ccab.

Defines rule #6.

Referenced by [11], [20].

[11] ccabab=bcabac

Overlap of [8] babcac=c with [7] cabcab=c:

babca c cabcab

Critical pair: babcac=cabcab.

Reduce LHS:

[9]	(babc)ac
	⇒ bcabac

Reduce RHS:

[10]	(cabc)ab
	⇒ ccabab

Flip LHS and RHS.

Referenced by [15], [17].

[12] bcabab=b

Overlap of [6] babcab=b with [9] babc=bcab:

babcab babc

Critical pair: bcabab=b.

Referenced by [15], [20].

[13] bcabac=c

Overlap of [8] babcac=c with [9] babc=bcab:

babcac babc

Critical pair: bcabac=c.

Referenced by [17], [19].

[14] bacc=bcac

Overlap of [9] babc=bcab with [5] cb=bc:

bab c cb

Critical pair: babbc=bcabb.

Reduce LHS:

[3]	ba(bb)c
	⇒ bacc

Reduce RHS:

[3]	bca(bb)
	⇒ bcac

Defines rule #5.

Referenced by [16], [18].

[15] ccabac=bc

Overlap of [5] cb=bc with [12] bcabab=b:

c b bcabab

Critical pair: cb=bccabab.

Reduce LHS:

[5]	(cb)
	⇒ bc

Reduce RHS:

[11]	b(ccabab)
[3]	⇒ (bb)cabac
	⇒ ccabac

Flip LHS and RHS.

Referenced by [20].

[16] cacc=ccac

Overlap of [3] bb=c with [14] bacc=bcac:

b b bacc

Critical pair: bbcac=cacc.

Reduce LHS:

[3]	(bb)cac
	⇒ ccac

Flip LHS and RHS.

Defines rule #7.

[17] ccabab=c

Simplify [11] ccabab=bcabac.

Reduce RHS:

[13]	(bcabac)
	⇒ c

Referenced by [18].

[18] bcacabab=bac

Overlap of [14] bacc=bcac with [17] ccabab=c:

ba cc ccabab

Critical pair: bac=bcacabab.

Flip LHS and RHS.

Referenced by [19], [20].

[19] cabab=babac

Overlap of [9] babc=bcab with [18] bcacabab=bac:

ba bc bcacabab

Critical pair: babac=bcabacabab.

Reduce RHS:

[13]	(bcabac)abab
	⇒ cabab

Flip LHS and RHS.

Defines rule #8.

[20] cabac=b

Overlap of [10] cabc=ccab with [18] bcacabab=bac:

ca bc bcacabab

Critical pair: cabac=ccabacabab.

Reduce RHS:

[15]	(ccabac)abab
[12]	⇒ (bcabab)
	⇒ b

Defines rule #9.