Certificate for #5491 ⟨a, b | aaaaba=babba⟩

Completion settings:

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

[1] babba=aaaaba

Axiom: aaaaba=babba.

Flip LHS and RHS.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #3.

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

[3] babba=aaaac

Simplify [1] babba=aaaaba.

Reduce RHS:

[2]	aaaa(ba)
	⇒ aaaac

Referenced by [4].

[4] cbc=aaaac

Overlap of [3] babba=aaaac with [2] ba=c:

babba ba

Critical pair: cbba=aaaac.

Reduce LHS:

[2]	cb(ba)
	⇒ cbc

Defines rule #5.

Referenced by [5], [7].

[5] aaaaaaaac=ccaaac

Overlap of [4] cbc=aaaac with [4] cbc=aaaac:

cb c cbc

Critical pair: cbaaaac=aaaacbc.

Reduce LHS:

[2]	c(ba)aaac
	⇒ ccaaac

Reduce RHS:

[4]	aaaa(cbc)
	⇒ aaaaaaaac

Flip LHS and RHS.

Defines rule #1.

Referenced by [6], [7].

[6] bccaaac=caaaaaaac

Overlap of [2] ba=c with [5] aaaaaaaac=ccaaac:

b a aaaaaaaac

Critical pair: bccaaac=caaaaaaac.

Defines rule #4.

[7] ccaaaaaaac=aaaaccaaac

Overlap of [5] aaaaaaaac=ccaaac with [4] cbc=aaaac:

aaaaaaaa c cbc

Critical pair: aaaaaaaaaaaac=ccaaacbc.

Reduce LHS:

[5]	aaaa(aaaaaaaac)
	⇒ aaaaccaaac

Reduce RHS:

[4]	ccaaa(cbc)
	⇒ ccaaaaaaac

Flip LHS and RHS.

Defines rule #2.