Certificate for #5733 ⟨a, b | aabbaa=abaab⟩

Completion settings:

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

[1] aabbaa=abaab

Axiom: aabbaa=abaab.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

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

[3] aabbaa=cac

Simplify [1] aabbaa=abaab.

Reduce RHS:

[2]	(ab)aab
[2]	⇒ ca(ab)
	⇒ cac

Referenced by [4].

[4] acbaa=cac

Overlap of [3] aabbaa=cac with [2] ab=c:

a abbaa ab

Critical pair: acbaa=cac.

Defines rule #4.

Referenced by [5], [6], [7], [8], [11], [15], [17].

[5] acbac=cacb

Overlap of [4] acbaa=cac with [2] ab=c:

acba a ab

Critical pair: acbac=cacb.

Defines rule #2.

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

[6] caccbaa=ccacb

Overlap of [4] acbaa=cac with [4] acbaa=cac:

acba a acbaa

Critical pair: acbacac=caccbaa.

Reduce LHS:

[5]	(acbac)ac
[5]	⇒ c(acbac)
	⇒ ccacb

Flip LHS and RHS.

Defines rule #5.

Referenced by [10], [11], [12], [15].

[7] ccacbb=caccbac

Overlap of [4] acbaa=cac with [5] acbac=cacb:

acba a acbac

Critical pair: acbacacb=caccbac.

Reduce LHS:

[5]	(acbac)acb
[5]	⇒ c(acbac)b
	⇒ ccacbb

Defines rule #3.

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

[8] cacbbaa=acbcac

Overlap of [5] acbac=cacb with [4] acbaa=cac:

acb ac acbaa

Critical pair: acbcac=cacbbaa.

Flip LHS and RHS.

Defines rule #11.

Referenced by [13].

[9] cacbbac=acbcacb

Overlap of [5] acbac=cacb with [5] acbac=cacb:

acb ac acbac

Critical pair: acbcacb=cacbbac.

Flip LHS and RHS.

Defines rule #7.

[10] ccacbcbaa=cacbcacb

Overlap of [5] acbac=cacb with [6] caccbaa=ccacb:

acba c caccbaa

Critical pair: acbaccacb=cacbaccbaa.

Reduce LHS:

[5]	(acbac)cacb
	⇒ cacbcacb

Reduce RHS:

[5]	c(acbac)cbaa
	⇒ ccacbcbaa

Flip LHS and RHS.

Referenced by [11], [19].

[11] cacbcacb=caccbacac

Overlap of [6] caccbaa=ccacb with [4] acbaa=cac:

caccba a acbaa

Critical pair: caccbacac=ccacbcbaa.

Reduce RHS:

[10]	(ccacbcbaa)
	⇒ cacbcacb

Flip LHS and RHS.

Defines rule #6.

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

[12] caccbacacb=ccacbcbac

Overlap of [6] caccbaa=ccacb with [5] acbac=cacb:

caccba a acbac

Critical pair: caccbacacb=ccacbcbac.

Defines rule #10.

Referenced by [20].

[13] caccbacaa=cacbcac

Overlap of [7] ccacbb=caccbac with [8] cacbbaa=acbcac:

c cacbb cacbbaa

Critical pair: cacbcac=caccbacaa.

Flip LHS and RHS.

Defines rule #8.

Referenced by [14], [15].

[14] ccacbcbacaa=caccbaccac

Overlap of [5] acbac=cacb with [13] caccbacaa=cacbcac:

acba c caccbacaa

Critical pair: acbacacbcac=cacbaccbacaa.

Reduce LHS:

[5]	(acbac)acbcac
[5]	⇒ c(acbac)bcac
[7]	⇒ (ccacbb)cac
	⇒ caccbaccac

Reduce RHS:

[5]	c(acbac)cbacaa
	⇒ ccacbcbacaa

Flip LHS and RHS.

Defines rule #16.

[15] caccbacacac=cacbccacb

Overlap of [13] caccbacaa=cacbcac with [4] acbaa=cac:

caccbaca a acbaa

Critical pair: caccbacacac=cacbcaccbaa.

Reduce RHS:

[6]	cacb(caccbaa)
	⇒ cacbccacb

Defines rule #9.

[16] ccacbcbacac=caccbaccacb

Overlap of [5] acbac=cacb with [11] cacbcacb=caccbacac:

acba c cacbcacb

Critical pair: acbacaccbacac=cacbacbcacb.

Reduce LHS:

[5]	(acbac)accbacac
[5]	⇒ c(acbac)cbacac
	⇒ ccacbcbacac

Reduce RHS:

[5]	c(acbac)bcacb
[7]	⇒ (ccacbb)cacb
	⇒ caccbaccacb

Defines rule #13.

[17] caccbacacaa=cacbccac

Overlap of [11] cacbcacb=caccbacac with [4] acbaa=cac:

cacbc acb acbaa

Critical pair: cacbccac=caccbacacaa.

Flip LHS and RHS.

Defines rule #14.

[18] cacbcaccbacac=caccbacaccacb

Overlap of [11] cacbcacb=caccbacac with [11] cacbcacb=caccbacac:

cacb cacb cacbcacb

Critical pair: cacbcaccbacac=caccbacaccacb.

Defines rule #15.

[19] ccacbcbaa=caccbacac

Simplify [10] ccacbcbaa=cacbcacb.

Reduce RHS:

[11]	(cacbcacb)
	⇒ caccbacac

Defines rule #12.

[20] caccbacaccbacac=ccacbcbaccacb

Overlap of [12] caccbacacb=ccacbcbac with [11] cacbcacb=caccbacac:

caccba cacb cacbcacb

Critical pair: caccbacaccbacac=ccacbcbaccacb.

Defines rule #17.