Certificate for #1800 ⟨a, b | abbaaaaab=b

Completion settings:

[1] abbaaaaab=b

Axiom: abbaaaaab=b.

Defines rule #6.

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

[2] abbaaaab=bbaaaaab

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

abbaaaa ab abbaaaaab

Critical pair: abbaaaab=bbaaaaab.

Defines rule #5.

Referenced by [3].

[3] abbaaab=bbaaaab

Overlap of [2] abbaaaab=bbaaaaab with [1] abbaaaaab=b:

abbaaa ab abbaaaaab

Critical pair: abbaaab=bbaaaaabbaaaaab.

Reduce RHS:

[1]bbaaaa(abbaaaaab)
bbaaaab

Defines rule #4.

Referenced by [4].

[4] abbaab=bbaaab

Overlap of [3] abbaaab=bbaaaab with [1] abbaaaaab=b:

abbaa ab abbaaaaab

Critical pair: abbaab=bbaaaabbaaaaab.

Reduce RHS:

[1]bbaaa(abbaaaaab)
bbaaab

Defines rule #3.

Referenced by [5].

[5] abbab=bbaab

Overlap of [4] abbaab=bbaaab with [1] abbaaaaab=b:

abba ab abbaaaaab

Critical pair: abbab=bbaaabbaaaaab.

Reduce RHS:

[1]bbaa(abbaaaaab)
bbaab

Defines rule #2.

Referenced by [6].

[6] abbb=bbab

Overlap of [5] abbab=bbaab with [1] abbaaaaab=b:

abb ab abbaaaaab

Critical pair: abbb=bbaabbaaaaab.

Reduce RHS:

[1]bba(abbaaaaab)
bbab

Defines rule #1.