Certificate for #14869 ⟨a, b | abba=b, bbabb=a⟩

Completion settings:

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

[1] abba=b

Axiom: abba=b.

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

[2] bbabb=a

Axiom: bbabb=a.

Referenced by [4], [7].

[3] bbba=abbb

Overlap of [1] abba=b with [1] abba=b:

abb a abba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Referenced by [6].

[4] aa=bbb

Overlap of [1] abba=b with [2] bbabb=a:

a bba bbabb

Critical pair: aa=bbb.

Defines rule #4.

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

[5] ba=abbbbb

Overlap of [1] abba=b with [4] aa=bbb:

abb a aa

Critical pair: abbbbb=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [8].

[6] bbbbbbbbbbbbbb=bb

Overlap of [5] ba=abbbbb with [1] abba=b:

b a abba

Critical pair: bb=abbbbbbba.

Reduce RHS:

[3]	abbbb(bbba)
[3]	⇒ ab(bbba)bbb
[5]	⇒ a(ba)bbbbbb
[4]	⇒ (aa)bbbbbbbbbbb
	⇒ bbbbbbbbbbbbbb

Flip LHS and RHS.

Referenced by [7].

[7] abbbbbbbbbbbb=a

Overlap of [2] bbabb=a with [6] bbbbbbbbbbbbbb=bb:

bba bb bbbbbbbbbbbbbb

Critical pair: bbabb=abbbbbbbbbbbb.

Reduce LHS:

[2]	(bbabb)
	⇒ a

Flip LHS and RHS.

Defines rule #2.

[8] bbbbbbbbbbbbb=b

Overlap of [1] abba=b with [5] ba=abbbbb:

ab ba ba

Critical pair: ababbbbb=b.

Reduce LHS:

[5]	a(ba)bbbbb
[4]	⇒ (aa)bbbbbbbbbb
	⇒ bbbbbbbbbbbbb

Defines rule #1.