Certificate for #1814 ⟨a, b | abbbaaaab=b

Completion settings:

[1] abbbaaaab=b

Axiom: abbbaaaab=b.

Defines rule #5.

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

[2] abbbaaab=bbbaaaab

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

abbbaaa ab abbbaaaab

Critical pair: abbbaaab=bbbaaaab.

Defines rule #4.

Referenced by [3].

[3] abbbaab=bbbaaab

Overlap of [2] abbbaaab=bbbaaaab with [1] abbbaaaab=b:

abbbaa ab abbbaaaab

Critical pair: abbbaab=bbbaaaabbbaaaab.

Reduce RHS:

[1]bbbaaa(abbbaaaab)
bbbaaab

Defines rule #3.

Referenced by [4].

[4] abbbab=bbbaab

Overlap of [3] abbbaab=bbbaaab with [1] abbbaaaab=b:

abbba ab abbbaaaab

Critical pair: abbbab=bbbaaabbbaaaab.

Reduce RHS:

[1]bbbaa(abbbaaaab)
bbbaab

Defines rule #2.

Referenced by [5].

[5] abbbb=bbbab

Overlap of [4] abbbab=bbbaab with [1] abbbaaaab=b:

abbb ab abbbaaaab

Critical pair: abbbb=bbbaabbbaaaab.

Reduce RHS:

[1]bbba(abbbaaaab)
bbbab

Defines rule #1.