Certificate for #3788 ⟨a, b | ababbbaaab=b

Completion settings:

[1] ababbbaaab=b

Axiom: ababbbaaab=b.

Defines rule #4.

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

[2] ababbbaab=babbbaaab

Overlap of [1] ababbbaaab=b with [1] ababbbaaab=b:

ababbbaa ab ababbbaaab

Critical pair: ababbbaab=babbbaaab.

Defines rule #3.

Referenced by [3].

[3] ababbbab=babbbaab

Overlap of [2] ababbbaab=babbbaaab with [1] ababbbaaab=b:

ababbba ab ababbbaaab

Critical pair: ababbbab=babbbaaababbbaaab.

Reduce RHS:

[1]babbbaa(ababbbaaab)
babbbaab

Defines rule #2.

Referenced by [4].

[4] ababbbb=babbbab

Overlap of [3] ababbbab=babbbaab with [1] ababbbaaab=b:

ababbb ab ababbbaaab

Critical pair: ababbbb=babbbaababbbaaab.

Reduce RHS:

[1]babbba(ababbbaaab)
babbbab

Defines rule #1.