Certificate for #12197 ⟨a, b | aaaa=bb, aaab=b⟩

Back:⟨a, b | aaaa=bb, aaab=b⟩

Completion settings:

[1] aaaa=bb

Axiom: aaaa=bb.

Defines rule #4.

Referenced by [3], [4].

[2] aaab=b

Axiom: aaab=b.

Referenced by [4], [6].

[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].

[4] ab=bbb

Overlap of [1] aaaa=bb with [2] aaab=b:

a aaa aaab

Critical pair: ab=bbb.

Defines rule #2.

Referenced by [5], [6].

[5] bba=bbbb

Simplify [3] bba=abb.

Reduce RHS:

[4](ab)b
⇒ bbbb

Referenced by [7].

[6] bbbbbbb=b

Overlap of [2] aaab=b with [4] ab=bbb:

aa ab ab

Critical pair: aabbb=b.

Reduce LHS:

[4]a(ab)bb
[4]⇒ (ab)bbbb
⇒ bbbbbbb

Defines rule #1.

Referenced by [7].

[7] ba=bbb

Overlap of [6] bbbbbbb=b with [5] bba=bbbb:

bbbbb bb bba

Critical pair: bbbbbbbbb=ba.

Reduce LHS:

[6](bbbbbbb)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #3.