Certificate for #19564 ⟨a, b | aab=b, abbbb=aa⟩

Back:⟨a, b | aab=b, abbbb=aa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Referenced by [3].

[2] aa=abbbb

Axiom: abbbb=aa.

Flip LHS and RHS.

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

[3] abbbbb=b

Overlap of [1] aab=b with [2] aa=abbbb:

aab aa

Critical pair: abbbbb=b.

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

[4] abbbba=bbbb

Overlap of [2] aa=abbbb with [2] aa=abbbb:

a a aa

Critical pair: aabbbb=abbbba.

Reduce LHS:

[2](aa)bbbb
[3]⇒ (abbbbb)bbb
⇒ bbbb

Flip LHS and RHS.

Referenced by [7].

[5] ab=bbbbb

Overlap of [2] aa=abbbb with [3] abbbbb=b:

a a abbbbb

Critical pair: ab=abbbbbbbbb.

Reduce RHS:

[3](abbbbb)bbbb
⇒ bbbbb

Defines rule #2.

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

[6] bbbbbbbbb=b

Overlap of [3] abbbbb=b with [5] ab=bbbbb:

abbbbb ab

Critical pair: bbbbbbbbb=b.

Defines rule #1.

Referenced by [8].

[7] bbbbbbbba=bbbb

Simplify [4] abbbba=bbbb.

Reduce LHS:

[5](ab)bbba
⇒ bbbbbbbba

Referenced by [8].

[8] ba=bbbbb

Overlap of [6] bbbbbbbbb=b with [7] bbbbbbbba=bbbb:

b bbbbbbbb bbbbbbbba

Critical pair: bbbbb=ba.

Flip LHS and RHS.

Defines rule #3.

[9] aa=bbbbbbbb

Simplify [2] aa=abbbb.

Reduce RHS:

[5](ab)bbb
⇒ bbbbbbbb

Defines rule #4.