Certificate for #7764 ⟨a, b, c | ab=1, bbb=acc⟩

Completion settings:

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

[1] ab=1

Axiom: ab=1.

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

[2] bbb=acc

Axiom: bbb=acc.

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

[3] bb=aacc

Overlap of [1] ab=1 with [2] bbb=acc:

a b bbb

Critical pair: aacc=bb.

Flip LHS and RHS.

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

[4] accb=bacc

Overlap of [2] bbb=acc with [2] bbb=acc:

b bb bbb

Critical pair: bacc=accb.

Flip LHS and RHS.

Referenced by [6], [7], [8].

[5] b=aaacc

Overlap of [1] ab=1 with [3] bb=aacc:

a b bb

Critical pair: aaacc=b.

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7], [8], [10].

[6] aaccaacc=aaaccacc

Overlap of [2] bbb=acc with [3] bb=aacc:

bb b bb

Critical pair: bbaacc=accb.

Reduce LHS:

[5]	(b)baacc
[4]	⇒ aa(accb)aacc
[1]	⇒ a(ab)accaacc
	⇒ aaccaacc

Reduce RHS:

[4]	(accb)
[5]	⇒ (b)acc
	⇒ aaaccacc

Referenced by [7].

[7] aaaaccacc=acc

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

b b bb

Critical pair: baacc=aaccb.

Reduce LHS:

[5]	(b)aacc
[6]	⇒ a(aaccaacc)
	⇒ aaaaccacc

Reduce RHS:

[4]	a(accb)
[1]	⇒ (ab)acc
	⇒ acc

Referenced by [9].

[8] accaaacc=aaaccacc

Simplify [4] accb=bacc.

Reduce LHS:

[5]	acc(b)
	⇒ accaaacc

Reduce RHS:

[5]	(b)acc
	⇒ aaaccacc

Defines rule #3.

Referenced by [9].

[9] accaacc=aaccacc

Overlap of [8] accaaacc=aaaccacc with [8] accaaacc=aaaccacc:

accaa acc accaaacc

Critical pair: accaaaaaccacc=aaaccaccaaacc.

Reduce LHS:

[7]	acca(aaaaccacc)
	⇒ accaacc

Reduce RHS:

[8]	aaacc(accaaacc)
[8]	⇒ aa(accaaacc)acc
[7]	⇒ a(aaaaccacc)acc
	⇒ aaccacc

Defines rule #2.

[10] aaaacc=1

Overlap of [1] ab=1 with [5] b=aaacc:

a b b

Critical pair: aaaacc=1.

Defines rule #1.