Certificate for #19818 ⟨a, b | aaa=a, abba=bab⟩

Completion settings:

Auxiliary generators:
1. c = ab
Reduction order:
- Left-to-right recursive path with deg(a) = 0; deg(c) = deg(b) = 1, c < b

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [6], [9].

[2] abba=bab

Axiom: abba=bab.

Referenced by [4].

[3] ab=c

Axiom: ab=c.

Defines rule #3.

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

[4] abba=bc

Simplify [2] abba=bab.

Reduce RHS:

[3]	b(ab)
	⇒ bc

Referenced by [5].

[5] bc=cba

Overlap of [4] abba=bc with [3] ab=c:

abba ab

Critical pair: cba=bc.

Flip LHS and RHS.

Referenced by [7], [10], [11], [12], [13], [20], [21].

[6] aac=c

Overlap of [1] aaa=a with [3] ab=c:

aa a ab

Critical pair: aac=ab.

Reduce RHS:

[3]	(ab)
	⇒ c

Defines rule #2.

Referenced by [8], [11], [13].

[7] acba=cc

Overlap of [3] ab=c with [5] bc=cba:

a b bc

Critical pair: acba=cc.

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

[8] cba=acc

Overlap of [6] aac=c with [7] acba=cc:

a ac acba

Critical pair: acc=cba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [10], [11], [12], [13], [15], [17], [20], [21].

[9] ccaa=cc

Overlap of [7] acba=cc with [1] aaa=a:

acb a aaa

Critical pair: acba=ccaa.

Reduce LHS:

[7]	(acba)
	⇒ cc

Flip LHS and RHS.

Defines rule #4.

Referenced by [18].

[10] ccb=acacc

Overlap of [7] acba=cc with [3] ab=c:

acb a ab

Critical pair: acbc=ccb.

Reduce LHS:

[5]	ac(bc)
[8]	⇒ ac(cba)
	⇒ acacc

Flip LHS and RHS.

Referenced by [14].

[11] acacc=ccac

Overlap of [7] acba=cc with [6] aac=c:

acb a aac

Critical pair: acbc=ccac.

Reduce LHS:

[5]	ac(bc)
[8]	⇒ ac(cba)
	⇒ acacc

Referenced by [12], [14].

[12] bacc=ccac

Overlap of [5] bc=cba with [8] cba=acc:

b c cba

Critical pair: bacc=cbaba.

Reduce RHS:

[8]	(cba)ba
[8]	⇒ ac(cba)
[11]	⇒ (acacc)
	⇒ ccac

Defines rule #11.

Referenced by [16], [17], [18], [19].

[13] accac=cacc

Overlap of [8] cba=acc with [6] aac=c:

cb a aac

Critical pair: cbc=accac.

Reduce LHS:

[5]	c(bc)
[8]	⇒ c(cba)
	⇒ cacc

Flip LHS and RHS.

Referenced by [20], [22].

[14] ccb=ccac

Simplify [10] ccb=acacc.

Reduce RHS:

[11]	(acacc)
	⇒ ccac

Defines rule #10.

Referenced by [15], [19].

[15] cacc=ccaca

Overlap of [14] ccb=ccac with [8] cba=acc:

c cb cba

Critical pair: cacc=ccaca.

Defines rule #8.

Referenced by [20], [22].

[16] acccac=cccc

Overlap of [7] acba=cc with [12] bacc=ccac:

ac ba bacc

Critical pair: acccac=cccc.

Defines rule #14.

Referenced by [20].

[17] acccc=cccac

Overlap of [8] cba=acc with [12] bacc=ccac:

c ba bacc

Critical pair: cccac=acccc.

Flip LHS and RHS.

Defines rule #13.

[18] ccacaa=ccac

Overlap of [12] bacc=ccac with [9] ccaa=cc:

ba cc ccaa

Critical pair: bacc=ccacaa.

Reduce LHS:

[12]	(bacc)
	⇒ ccac

Flip LHS and RHS.

Defines rule #7.

[19] ccacb=ccacac

Overlap of [12] bacc=ccac with [14] ccb=ccac:

ba cc ccb

Critical pair: baccac=ccacb.

Reduce LHS:

[12]	(bacc)ac
	⇒ ccacac

Flip LHS and RHS.

Referenced by [23].

[20] ccacac=cccca

Overlap of [5] bc=cba with [15] cacc=ccaca:

b c cacc

Critical pair: bccaca=cbaacc.

Reduce LHS:

[5]	(bc)caca
[8]	⇒ (cba)caca
[16]	⇒ (acccac)a
	⇒ cccca

Reduce RHS:

[8]	(cba)acc
[13]	⇒ (accac)c
[15]	⇒ (cacc)c
	⇒ ccacac

Flip LHS and RHS.

Defines rule #12.

Referenced by [23].

[21] bc=acc

Simplify [5] bc=cba.

Reduce RHS:

[8]	(cba)
	⇒ acc

Defines rule #6.

[22] accac=ccaca

Simplify [13] accac=cacc.

Reduce RHS:

[15]	(cacc)
	⇒ ccaca

Defines rule #9.

[23] ccacb=cccca

Simplify [19] ccacb=ccacac.

Reduce RHS:

[20]	(ccacac)
	⇒ cccca

Defines rule #15.