Certificate for #2617 ⟨a, b | abbaab=aaba⟩

Completion settings:

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

[1] abbaab=aaba

Axiom: abbaab=aaba.

Referenced by [4].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

Referenced by [4], [5], [7], [12], [13], [16], [17], [20].

[3] cbcb=d

Axiom: cbcb=d.

Defines rule #2.

Referenced by [6], [8], [9], [10], [11], [12], [13], [18], [20], [22], [23], [25], [26], [28].

[4] abbaab=aca

Simplify [1] abbaab=aaba.

Reduce RHS:

[2]	a(ab)a
	⇒ aca

Referenced by [5].

[5] aca=cbac

Overlap of [4] abbaab=aca with [2] ab=c:

abbaab ab

Critical pair: cbaab=aca.

Reduce LHS:

[2]	cba(ab)
	⇒ cbac

Flip LHS and RHS.

Defines rule #5.

Referenced by [7], [8], [14], [22], [23], [26], [28].

[6] dcb=cbd

Overlap of [3] cbcb=d with [3] cbcb=d:

cb cb cbcb

Critical pair: cbd=dcb.

Flip LHS and RHS.

Defines rule #3.

[7] acc=cbacb

Overlap of [5] aca=cbac with [2] ab=c:

ac a ab

Critical pair: acc=cbacb.

Defines rule #4.

Referenced by [8], [9], [12], [15], [18], [20], [22], [23], [26], [28].

[8] cbacbbac=dacba

Overlap of [5] aca=cbac with [5] aca=cbac:

ac a aca

Critical pair: accbac=cbacca.

Reduce LHS:

[7]	(acc)bac
	⇒ cbacbbac

Reduce RHS:

[7]	cb(acc)a
[3]	⇒ (cbcb)acba
	⇒ dacba

Defines rule #8.

Referenced by [11], [12], [13], [14], [15], [16], [17], [19], [20], [24], [27], [29].

[9] cbacbbcb=acd

Overlap of [7] acc=cbacb with [3] cbcb=d:

ac c cbcb

Critical pair: acd=cbacbbcb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [10], [14], [15], [17], [21].

[10] dacbbcb=cbacd

Overlap of [3] cbcb=d with [9] cbacbbcb=acd:

cb cb cbacbbcb

Critical pair: cbacd=dacbbcb.

Flip LHS and RHS.

Defines rule #7.

[11] dacbbac=cbdacba

Overlap of [3] cbcb=d with [8] cbacbbac=dacba:

cb cb cbacbbac

Critical pair: cbdacba=dacbbac.

Flip LHS and RHS.

Defines rule #11.

Referenced by [20].

[12] acdacba=dadac

Overlap of [7] acc=cbacb with [8] cbacbbac=dacba:

ac c cbacbbac

Critical pair: acdacba=cbacbbacbbac.

Reduce RHS:

[8]	(cbacbbac)bbac
[2]	⇒ dacb(ab)bac
[3]	⇒ da(cbcb)ac
	⇒ dadac

Defines rule #16.

Referenced by [22].

[13] dacbccb=cbacbbad

Overlap of [8] cbacbbac=dacba with [3] cbcb=d:

cbacbba c cbcb

Critical pair: cbacbbad=dacbabcb.

Reduce RHS:

[2]	dacb(ab)cb
	⇒ dacbccb

Flip LHS and RHS.

Defines rule #9.

[14] dacbaa=acdac

Overlap of [8] cbacbbac=dacba with [5] aca=cbac:

cbacbb ac aca

Critical pair: cbacbbcbac=dacbaa.

Reduce LHS:

[9]	(cbacbbcb)ac
	⇒ acdac

Flip LHS and RHS.

Defines rule #12.

[15] dacbac=acdacb

Overlap of [8] cbacbbac=dacba with [7] acc=cbacb:

cbacbb ac acc

Critical pair: cbacbbcbacb=dacbac.

Reduce LHS:

[9]	(cbacbbcb)acb
	⇒ acdacb

Flip LHS and RHS.

Defines rule #10.

Referenced by [18], [19], [20], [21].

[16] dacbcacbbac=cbacbbadacba

Overlap of [8] cbacbbac=dacba with [8] cbacbbac=dacba:

cbacbba c cbacbbac

Critical pair: cbacbbadacba=dacbabacbbac.

Reduce RHS:

[2]	dacb(ab)acbbac
	⇒ dacbcacbbac

Flip LHS and RHS.

Defines rule #22.

[17] dacbcacbbcb=cbacbbaacd

Overlap of [8] cbacbbac=dacba with [9] cbacbbcb=acd:

cbacbba c cbacbbcb

Critical pair: cbacbbaacd=dacbabacbbcb.

Reduce RHS:

[2]	dacb(ab)acbbcb
	⇒ dacbcacbbcb

Flip LHS and RHS.

Defines rule #18.

[18] acdacbc=dadacb

Overlap of [15] dacbac=acdacb with [7] acc=cbacb:

dacb ac acc

Critical pair: dacbcbacb=acdacbc.

Reduce LHS:

[3]	da(cbcb)acb
	⇒ dadacb

Flip LHS and RHS.

Defines rule #14.

Referenced by [23], [24], [25].

[19] acdacbbbac=dadacba

Overlap of [15] dacbac=acdacb with [8] cbacbbac=dacba:

da cbac cbacbbac

Critical pair: dadacba=acdacbbbac.

Flip LHS and RHS.

Defines rule #17.

Referenced by [28], [29].

[20] dacbadacba=cbacbbdadac

Overlap of [15] dacbac=acdacb with [8] cbacbbac=dacba:

dacba c cbacbbac

Critical pair: dacbadacba=acdacbbacbbac.

Reduce RHS:

[11]	ac(dacbbac)bbac
[7]	⇒ (acc)bdacbabbac
[2]	⇒ cbacbbdacb(ab)bac
[3]	⇒ cbacbbda(cbcb)ac
	⇒ cbacbbdadac

Defines rule #25.

[21] acdacbbbcb=daacd

Overlap of [15] dacbac=acdacb with [9] cbacbbcb=acd:

da cbac cbacbbcb

Critical pair: daacd=acdacbbbcb.

Flip LHS and RHS.

Defines rule #15.

Referenced by [26], [27].

[22] dacbdacba=acdadac

Overlap of [5] aca=cbac with [12] acdacba=dadac:

ac a acdacba

Critical pair: acdadac=cbaccdacba.

Reduce RHS:

[7]	cb(acc)dacba
[3]	⇒ (cbcb)acbdacba
	⇒ dacbdacba

Flip LHS and RHS.

Defines rule #21.

[23] dacbdacbc=acdadacb

Overlap of [5] aca=cbac with [18] acdacbc=dadacb:

ac a acdacbc

Critical pair: acdadacb=cbaccdacbc.

Reduce RHS:

[7]	cb(acc)dacbc
[3]	⇒ (cbcb)acbdacbc
	⇒ dacbdacbc

Flip LHS and RHS.

Defines rule #19.

[24] dacbadacbc=cbacbbdadacb

Overlap of [8] cbacbbac=dacba with [18] acdacbc=dadacb:

cbacbb ac acdacbc

Critical pair: cbacbbdadacb=dacbadacbc.

Flip LHS and RHS.

Defines rule #23.

[25] dadacbb=acdad

Overlap of [18] acdacbc=dadacb with [3] cbcb=d:

acda cbc cbcb

Critical pair: acdad=dadacbb.

Flip LHS and RHS.

Defines rule #13.

[26] dacbdacbbbcb=acdaacd

Overlap of [5] aca=cbac with [21] acdacbbbcb=daacd:

ac a acdacbbbcb

Critical pair: acdaacd=cbaccdacbbbcb.

Reduce RHS:

[7]	cb(acc)dacbbbcb
[3]	⇒ (cbcb)acbdacbbbcb
	⇒ dacbdacbbbcb

Flip LHS and RHS.

Defines rule #20.

[27] dacbadacbbbcb=cbacbbdaacd

Overlap of [8] cbacbbac=dacba with [21] acdacbbbcb=daacd:

cbacbb ac acdacbbbcb

Critical pair: cbacbbdaacd=dacbadacbbbcb.

Flip LHS and RHS.

Defines rule #24.

[28] dacbdacbbbac=acdadacba

Overlap of [5] aca=cbac with [19] acdacbbbac=dadacba:

ac a acdacbbbac

Critical pair: acdadacba=cbaccdacbbbac.

Reduce RHS:

[7]	cb(acc)dacbbbac
[3]	⇒ (cbcb)acbdacbbbac
	⇒ dacbdacbbbac

Flip LHS and RHS.

Defines rule #26.

[29] dacbadacbbbac=cbacbbdadacba

Overlap of [8] cbacbbac=dacba with [19] acdacbbbac=dadacba:

cbacbb ac acdacbbbac

Critical pair: cbacbbdadacba=dacbadacbbbac.

Flip LHS and RHS.

Defines rule #27.