Certificate for #3779 ⟨a, b | ababbaaaab=b

Completion settings:

[1] ababbaaaab=b

Axiom: ababbaaaab=b.

Defines rule #5.

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

[2] ababbaaab=babbaaaab

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

ababbaaa ab ababbaaaab

Critical pair: ababbaaab=babbaaaab.

Defines rule #4.

Referenced by [3].

[3] ababbaab=babbaaab

Overlap of [2] ababbaaab=babbaaaab with [1] ababbaaaab=b:

ababbaa ab ababbaaaab

Critical pair: ababbaab=babbaaaababbaaaab.

Reduce RHS:

[1]babbaaa(ababbaaaab)
babbaaab

Defines rule #3.

Referenced by [4].

[4] ababbab=babbaab

Overlap of [3] ababbaab=babbaaab with [1] ababbaaaab=b:

ababba ab ababbaaaab

Critical pair: ababbab=babbaaababbaaaab.

Reduce RHS:

[1]babbaa(ababbaaaab)
babbaab

Defines rule #2.

Referenced by [5].

[5] ababbb=babbab

Overlap of [4] ababbab=babbaab with [1] ababbaaaab=b:

ababb ab ababbaaaab

Critical pair: ababbb=babbaababbaaaab.

Reduce RHS:

[1]babba(ababbaaaab)
babbab

Defines rule #1.