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

Back:⟨a, b | aababaaaab=a⟩

Completion settings:

[1] aababaaaab=a

Axiom: aababaaaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] aabaaaab=aababaaa

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

aababaa aab aababaaaab

Critical pair: aababaaa=aabaaaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaaaab=aabaaa

Overlap of [1] aababaaaab=a with [2] aabaaaab=aababaaa:

aababaa aab aabaaaab

Critical pair: aababaaaababaaa=aaaaab.

Reduce LHS:

[1](aababaaaab)abaaa
⇒ aabaaa

Flip LHS and RHS.

Defines rule #1.