Certificate for #3706 ⟨a, b | abaaaabaab=b⟩

Back:⟨a, b | abaaaabaab=b⟩

Completion settings:

[1] abaaaabaab=b

Axiom: abaaaabaab=b.

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

[2] baaaabaab=abaaaabab

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

abaaaaba ab abaaaabaab

Critical pair: abaaaabab=baaaabaab.

Flip LHS and RHS.

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

[3] baaaabab=abaaaabb

Overlap of [2] baaaabaab=abaaaabab with [1] abaaaabaab=b:

baaaaba ab abaaaabaab

Critical pair: baaaabab=abaaaababaaaabaab.

Reduce RHS:

[1]abaaaab(abaaaabaab)
⇒ abaaaabb

Defines rule #1.

Referenced by [4], [5].

[4] aaabaaaabb=b

Overlap of [1] abaaaabaab=b with [2] baaaabaab=abaaaabab:

a baaaabaab baaaabaab

Critical pair: aabaaaabab=b.

Reduce LHS:

[3]aa(baaaabab)
⇒ aaabaaaabb

Defines rule #3.

[5] baaaabaab=aabaaaabb

Simplify [2] baaaabaab=abaaaabab.

Reduce RHS:

[3]a(baaaabab)
⇒ aabaaaabb

Defines rule #2.