Certificate for #14673 ⟨a, b | aabb=a, aabaa=a⟩

Back:⟨a, b | aabb=a, aabaa=a⟩

Completion settings:

[1] aabb=a

Axiom: aabb=a.

Referenced by [3].

[2] aabaa=a

Axiom: aabaa=a.

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

[3] abb=aaba

Overlap of [2] aabaa=a with [1] aabb=a:

aab aa aabb

Critical pair: aaba=abb.

Flip LHS and RHS.

Referenced by [5].

[4] aaba=abaa

Overlap of [2] aabaa=a with [2] aabaa=a:

aab aa aabaa

Critical pair: aaba=abaa.

Defines rule #2.

Referenced by [5], [6].

[5] abb=abaa

Simplify [3] abb=aaba.

Reduce RHS:

[4](aaba)
⇒ abaa

Defines rule #3.

[6] abaaa=a

Overlap of [2] aabaa=a with [4] aaba=abaa:

aabaa aaba

Critical pair: abaaa=a.

Defines rule #1.