Certificate for #3581 ⟨a, b | aababaaaab=b⟩

Back:⟨a, b | aababaaaab=b⟩

Completion settings:

[1] aababaaaab=b

Axiom: aababaaaab=b.

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

[2] babaaaab=aababaab

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

aababaa aab aababaaaab

Critical pair: aababaab=babaaaab.

Flip LHS and RHS.

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

[3] babaab=aababb

Overlap of [2] babaaaab=aababaab with [1] aababaaaab=b:

babaa aab aababaaaab

Critical pair: babaab=aababaababaaaab.

Reduce RHS:

[1]aabab(aababaaaab)
⇒ aababb

Defines rule #1.

Referenced by [4], [5].

[4] aaaaaababb=b

Overlap of [1] aababaaaab=b with [2] babaaaab=aababaab:

aa babaaaab babaaaab

Critical pair: aaaababaab=b.

Reduce LHS:

[3]aaaa(babaab)
⇒ aaaaaababb

Defines rule #3.

[5] babaaaab=aaaababb

Simplify [2] babaaaab=aababaab.

Reduce RHS:

[3]aa(babaab)
⇒ aaaababb

Defines rule #2.