Certificate for #12983 ⟨a, b | abb=aaa, baab=b⟩

Completion settings:

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

[1] aaa=abb

Axiom: abb=aaa.

Flip LHS and RHS.

Defines rule #5.

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

[2] baab=b

Axiom: baab=b.

Defines rule #4.

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

[3] abba=aabb

Overlap of [1] aaa=abb with [1] aaa=abb:

a aa aaa

Critical pair: aabb=abba.

Flip LHS and RHS.

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

[4] bba=babbbb

Overlap of [2] baab=b with [3] abba=aabb:

ba ab abba

Critical pair: baaabb=bba.

Reduce LHS:

[1]	b(aaa)bb
	⇒ babbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[5] abbbbb=abb

Overlap of [3] abba=aabb with [2] baab=b:

ab ba baab

Critical pair: abb=aabbab.

Reduce RHS:

[3]	a(abba)b
[1]	⇒ (aaa)bbb
	⇒ abbbbb

Flip LHS and RHS.

Referenced by [6].

[6] bbbbb=bb

Overlap of [2] baab=b with [5] abbbbb=abb:

ba ab abbbbb

Critical pair: baabb=bbbbb.

Reduce LHS:

[2]	(baab)b
	⇒ bb

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[7] ababbbb=aabb

Overlap of [3] abba=aabb with [4] bba=babbbb:

a bba bba

Critical pair: ababbbb=aabb.

Referenced by [8].

[8] ababb=aabbb

Overlap of [7] ababbbb=aabb with [6] bbbbb=bb:

aba bbbb bbbbb

Critical pair: ababb=aabbb.

Defines rule #3.