Certificate for #7761 ⟨a, b, c | ab=1, bbb=aac⟩

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=aac

Axiom: bbb=aac.

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

[3] bb=aaac

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

a b bbb

Critical pair: aaac=bb.

Flip LHS and RHS.

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

[4] aacb=baac

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

b bb bbb

Critical pair: baac=aacb.

Flip LHS and RHS.

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

[5] b=aaaac

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

a b bb

Critical pair: aaaac=b.

Flip LHS and RHS.

Defines rule #4.

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

[6] aaacaaac=aaaacaac

Overlap of [2] bbb=aac with [3] bb=aaac:

bb b bb

Critical pair: bbaaac=aacb.

Reduce LHS:

[5]	(b)baaac
[4]	⇒ aa(aacb)aaac
[1]	⇒ a(ab)aacaaac
	⇒ aaacaaac

Reduce RHS:

[4]	(aacb)
[5]	⇒ (b)aac
	⇒ aaaacaac

Referenced by [7].

[7] aaaaacaac=aac

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

b b bb

Critical pair: baaac=aaacb.

Reduce LHS:

[5]	(b)aaac
[6]	⇒ a(aaacaaac)
	⇒ aaaaacaac

Reduce RHS:

[4]	a(aacb)
[1]	⇒ (ab)aac
	⇒ aac

Referenced by [9].

[8] aacaaaac=aaaacaac

Simplify [4] aacb=baac.

Reduce LHS:

[5]	aac(b)
	⇒ aacaaaac

Reduce RHS:

[5]	(b)aac
	⇒ aaaacaac

Defines rule #3.

Referenced by [9].

[9] aacaaac=aaacaac

Overlap of [8] aacaaaac=aaaacaac with [8] aacaaaac=aaaacaac:

aacaa aac aacaaaac

Critical pair: aacaaaaaacaac=aaaacaacaaaac.

Reduce LHS:

[7]	aaca(aaaaacaac)
	⇒ aacaaac

Reduce RHS:

[8]	aaaac(aacaaaac)
[8]	⇒ aa(aacaaaac)aac
[7]	⇒ a(aaaaacaac)aac
	⇒ aaacaac

Defines rule #2.

[10] aaaaac=1

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

a b b

Critical pair: aaaaac=1.

Defines rule #1.