Certificate for #7308 ⟨a, b, c | ab=1, aabc=bb⟩

Completion settings:

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

Axiom: ab=1.

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

Axiom: aabc=bb.

Reduce LHS:

[1]	a(ab)c
	⇒ ac

Flip LHS and RHS.

Referenced by [3], [4].

Overlap of [1] ab=1 with [2] bb=ac:

a b bb

Critical pair: aac=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

b b bb

Critical pair: bac=acb.

Reduce LHS:

[3]	(b)ac
	⇒ aacac

Reduce RHS:

[3]	ac(b)
	⇒ acaac

Flip LHS and RHS.

Defines rule #2.

a b b

Critical pair: aaac=1.

Defines rule #1.