Certificate for #5340 ⟨a, b | ababaab=aaab⟩

Completion settings:

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

[1] ababaab=aaab

Axiom: ababaab=aaab.

Referenced by [3].

[2] aaab=c

Axiom: aaab=c.

Defines rule #1.

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

[3] ababaab=c

Simplify [1] ababaab=aaab.

Reduce RHS:

[2]	(aaab)
	⇒ c

Defines rule #5.

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

[4] cabaab=ababac

Overlap of [3] ababaab=c with [3] ababaab=c:

ababa ab ababaab

Critical pair: ababac=cabaab.

Flip LHS and RHS.

Referenced by [5], [8].

[5] ababac=aac

Overlap of [2] aaab=c with [3] ababaab=c:

aa ab ababaab

Critical pair: aac=cabaab.

Reduce RHS:

[4]	(cabaab)
	⇒ ababac

Flip LHS and RHS.

Defines rule #2.

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

[6] ababaaac=cabac

Overlap of [3] ababaab=c with [5] ababac=aac:

ababa ab ababac

Critical pair: ababaaac=cabac.

Defines rule #7.

[7] aaaac=cabac

Overlap of [2] aaab=c with [5] ababac=aac:

aa ab ababac

Critical pair: aaaac=cabac.

Defines rule #4.

[8] cabaab=aac

Simplify [4] cabaab=ababac.

Reduce RHS:

[5]	(ababac)
	⇒ aac

Defines rule #3.

Referenced by [9].

[9] cabaaac=aacabac

Overlap of [8] cabaab=aac with [5] ababac=aac:

caba ab ababac

Critical pair: cabaaac=aacabac.

Defines rule #6.