Certificate for #12206 ⟨a, b | aaaa=bb, abbb=a⟩

Completion settings:

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

[1] aaaa=bb

Axiom: aaaa=bb.

Defines rule #2.

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

[2] abbb=a

Axiom: abbb=a.

Defines rule #3.

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

[3] bba=abb

Overlap of [1] aaaa=bb with [1] aaaa=bb:

a aaa aaaa

Critical pair: abb=bba.

Flip LHS and RHS.

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

[4] bbbbb=bb

Overlap of [1] aaaa=bb with [2] abbb=a:

aaa a abbb

Critical pair: aaaa=bbbbb.

Reduce LHS:

[1]	(aaaa)
	⇒ bb

Flip LHS and RHS.

Defines rule #4.

[5] aba=aab

Overlap of [2] abbb=a with [3] bba=abb:

abb b bba

Critical pair: abbabb=aba.

Reduce LHS:

[3]	a(bba)bb
[2]	⇒ a(abbb)b
	⇒ aab

Flip LHS and RHS.

Referenced by [6].

[6] babb=a

Overlap of [1] aaaa=bb with [5] aba=aab:

aaa a aba

Critical pair: aaaaab=bbba.

Reduce LHS:

[1]	(aaaa)ab
[3]	⇒ (bba)b
[2]	⇒ (abbb)
	⇒ a

Reduce RHS:

[3]	b(bba)
	⇒ babb

Flip LHS and RHS.

Referenced by [7].

[7] ba=ab

Overlap of [3] bba=abb with [6] babb=a:

b ba babb

Critical pair: ba=abbbb.

Reduce RHS:

[2]	(abbb)b
	⇒ ab

Defines rule #1.