Certificate for #3758 ⟨a, b | ababaaabab=b⟩

Back:⟨a, b | ababaaabab=b⟩

Completion settings:

[1] ababaaabab=b

Axiom: ababaaabab=b.

Referenced by [2], [3], [4], [6], [7], [8].

[2] baaabab=ababaab

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

ababaa abab ababaaabab

Critical pair: ababaab=baaabab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4], [6], [8].

[3] ababaaabb=baababaab

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

ababaaab ab ababaaabab

Critical pair: ababaaabb=babaaabab.

Reduce RHS:

[2]ba(baaabab)
⇒ baababaab

Referenced by [5].

[4] baaabb=ababab

Overlap of [2] baaabab=ababaab with [1] ababaaabab=b:

baaab ab ababaaabab

Critical pair: baaabb=ababaababaaabab.

Reduce RHS:

[1]ababa(ababaaabab)
⇒ ababab

Defines rule #1.

Referenced by [5].

[5] abaababab=baababaab

Simplify [3] ababaaabb=baababaab.

Reduce LHS:

[4]aba(baaabb)
⇒ abaababab

Defines rule #5.

Referenced by [6], [7].

[6] abaabb=babaab

Overlap of [5] abaababab=baababaab with [1] ababaaabab=b:

abaab abab ababaaabab

Critical pair: abaabb=baababaabaaabab.

Reduce RHS:

[2]baababaa(baaabab)
[1]⇒ ba(ababaaabab)aab
⇒ babaab

Defines rule #2.

[7] abaababb=baababab

Overlap of [5] abaababab=baababaab with [1] ababaaabab=b:

abaabab ab ababaaabab

Critical pair: abaababb=baababaababaaabab.

Reduce RHS:

[1]baababa(ababaaabab)
⇒ baababab

Defines rule #4.

[8] abaababaab=b

Overlap of [1] ababaaabab=b with [2] baaabab=ababaab:

aba baaabab baaabab

Critical pair: abaababaab=b.

Defines rule #6.