Certificate for #24683 ⟨a, b | aa=a, abbbba=bb⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] abbbba=bb

Axiom: abbbba=bb.

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

[3] abb=bb

Overlap of [1] aa=a with [2] abbbba=bb:

a a abbbba

Critical pair: abb=abbbba.

Reduce RHS:

[2]	(abbbba)
	⇒ bb

Defines rule #2.

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

[4] bbbba=bba

Overlap of [2] abbbba=bb with [1] aa=a:

abbbb a aa

Critical pair: abbbba=bba.

Reduce LHS:

[3]	(abb)bba
	⇒ bbbba

Referenced by [5], [6].

[5] bbbbbb=bba

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

abbbb a abbbba

Critical pair: abbbbbb=bbbbbba.

Reduce LHS:

[3]	(abb)bbbb
	⇒ bbbbbb

Reduce RHS:

[4]	bb(bbbba)
[4]	⇒ (bbbba)
	⇒ bba

Referenced by [7].

[6] bba=bb

Overlap of [2] abbbba=bb with [3] abb=bb:

abbbba abb

Critical pair: bbbba=bb.

Reduce LHS:

[4]	(bbbba)
	⇒ bba

Defines rule #3.

Referenced by [7].

[7] bbbb=bb

Overlap of [2] abbbba=bb with [3] abb=bb:

abbbb a abb

Critical pair: abbbbbb=bbbb.

Reduce LHS:

[3]	(abb)bbbb
[5]	⇒ (bbbbbb)
[6]	⇒ (bba)
	⇒ bb

Flip LHS and RHS.

Defines rule #4.