Certificate for #27160 ⟨a, b | aa=1, abbbbab=bb⟩

Completion settings:

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

[1] aa=1

Axiom: aa=1.

Defines rule #3.

Referenced by [3], [5].

[2] abbbbab=bb

Axiom: abbbbab=bb.

Referenced by [3], [4].

[3] abb=bbbbab

Overlap of [1] aa=1 with [2] abbbbab=bb:

a a abbbbab

Critical pair: abb=bbbbab.

Defines rule #2.

Referenced by [4], [5].

[4] bbbbbbbbbbbbbbbbbbbbab=bbbbbab

Overlap of [2] abbbbab=bb with [2] abbbbab=bb:

abbbb ab abbbbab

Critical pair: abbbbbb=bbbbbab.

Reduce LHS:

[3]	(abb)bbbb
[3]	⇒ bbbb(abb)bbb
[3]	⇒ bbbbbbbb(abb)bb
[3]	⇒ bbbbbbbbbbbb(abb)b
[3]	⇒ bbbbbbbbbbbbbbbb(abb)
	⇒ bbbbbbbbbbbbbbbbbbbbab

Referenced by [6].

[5] bbbbbbbbbbbbabab=bb

Overlap of [1] aa=1 with [3] abb=bbbbab:

a a abb

Critical pair: abbbbab=bb.

Reduce LHS:

[3]	(abb)bbab
[3]	⇒ bbbb(abb)bab
[3]	⇒ bbbbbbbb(abb)ab
	⇒ bbbbbbbbbbbbabab

Referenced by [6], [7].

[6] bbbbbabab=bbbbbbbbbb

Overlap of [4] bbbbbbbbbbbbbbbbbbbbab=bbbbbab with [5] bbbbbbbbbbbbabab=bb:

bbbbbbbb bbbbbbbbbbbbab bbbbbbbbbbbbabab

Critical pair: bbbbbbbbbb=bbbbbabab.

Flip LHS and RHS.

Referenced by [7], [8].

[7] bbbbbbbbbbbbbbbbb=bb

Overlap of [5] bbbbbbbbbbbbabab=bb with [6] bbbbbabab=bbbbbbbbbb:

bbbbbbb bbbbbabab bbbbbabab

Critical pair: bbbbbbbbbbbbbbbbb=bb.

Defines rule #1.

Referenced by [8].

[8] bbabab=bbbbbbb

Overlap of [7] bbbbbbbbbbbbbbbbb=bb with [6] bbbbbabab=bbbbbbbbbb:

bbbbbbbbbbbb bbbbb bbbbbabab

Critical pair: bbbbbbbbbbbbbbbbbbbbbb=bbabab.

Reduce LHS:

[7]	(bbbbbbbbbbbbbbbbb)bbbbb
	⇒ bbbbbbb

Flip LHS and RHS.

Defines rule #4.