Certificate for #22785 ⟨a, b | aaa=1, abaab=bab⟩

Completion settings:

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

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [6], [8].

[2] abaab=bab

Axiom: abaab=bab.

Referenced by [4].

[3] ab=c

Axiom: ab=c.

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

[4] abaab=bc

Simplify [2] abaab=bab.

Reduce RHS:

[3]	b(ab)
	⇒ bc

Referenced by [5].

[5] bc=cac

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

abaab ab

Critical pair: caab=bc.

Reduce LHS:

[3]	ca(ab)
	⇒ cac

Flip LHS and RHS.

Referenced by [7].

[6] b=aac

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

aa a ab

Critical pair: aac=b.

Flip LHS and RHS.

Defines rule #5.

Referenced by [7].

[7] aacc=cac

Simplify [5] bc=cac.

Reduce LHS:

[6]	(b)c
	⇒ aacc

Defines rule #2.

Referenced by [8].

[8] acac=cc

Overlap of [1] aaa=1 with [7] aacc=cac:

a aa aacc

Critical pair: acac=cc.

Defines rule #3.

Referenced by [9].

[9] ccac=accc

Overlap of [8] acac=cc with [8] acac=cc:

ac ac acac

Critical pair: accc=ccac.

Flip LHS and RHS.

Defines rule #4.