Certificate for #14729 ⟨a, b | abab=a, aaaaa=a⟩

Back:⟨a, b | abab=a, aaaaa=a⟩

Completion settings:

[1] abab=a

Axiom: abab=a.

Referenced by [3], [4].

[2] aaaaa=a

Axiom: aaaaa=a.

Defines rule #1.

Referenced by [4], [5].

[3] aba=aab

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

ab ab abab

Critical pair: aba=aab.

Defines rule #2.

Referenced by [4].

[4] aabb=a

Overlap of [2] aaaaa=a with [1] abab=a:

aaaa a abab

Critical pair: aaaaa=abab.

Reduce LHS:

[2](aaaaa)
⇒ a

Reduce RHS:

[3](aba)b
⇒ aabb

Flip LHS and RHS.

Referenced by [5].

[5] abb=aaaa

Overlap of [2] aaaaa=a with [4] aabb=a:

aaa aa aabb

Critical pair: aaaa=abb.

Flip LHS and RHS.

Defines rule #3.