Certificate for #3824 ⟨a, b | abbbaaaaab=b

Completion settings:

[1] abbbaaaaab=b

Axiom: abbbaaaaab=b.

Defines rule #6.

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

[2] abbbaaaab=bbbaaaaab

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

abbbaaaa ab abbbaaaaab

Critical pair: abbbaaaab=bbbaaaaab.

Defines rule #5.

Referenced by [3].

[3] abbbaaab=bbbaaaab

Overlap of [2] abbbaaaab=bbbaaaaab with [1] abbbaaaaab=b:

abbbaaa ab abbbaaaaab

Critical pair: abbbaaab=bbbaaaaabbbaaaaab.

Reduce RHS:

[1]bbbaaaa(abbbaaaaab)
bbbaaaab

Defines rule #4.

Referenced by [4].

[4] abbbaab=bbbaaab

Overlap of [3] abbbaaab=bbbaaaab with [1] abbbaaaaab=b:

abbbaa ab abbbaaaaab

Critical pair: abbbaab=bbbaaaabbbaaaaab.

Reduce RHS:

[1]bbbaaa(abbbaaaaab)
bbbaaab

Defines rule #3.

Referenced by [5].

[5] abbbab=bbbaab

Overlap of [4] abbbaab=bbbaaab with [1] abbbaaaaab=b:

abbba ab abbbaaaaab

Critical pair: abbbab=bbbaaabbbaaaaab.

Reduce RHS:

[1]bbbaa(abbbaaaaab)
bbbaab

Defines rule #2.

Referenced by [6].

[6] abbbb=bbbab

Overlap of [5] abbbab=bbbaab with [1] abbbaaaaab=b:

abbb ab abbbaaaaab

Critical pair: abbbb=bbbaabbbaaaaab.

Reduce RHS:

[1]bbba(abbbaaaaab)
bbbab

Defines rule #1.