Certificate for #14717 ⟨a, b | aabb=a, bbaba=a⟩

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

Completion settings:

[1] aabb=a

Axiom: aabb=a.

Defines rule #3.

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

[2] bbaba=a

Axiom: bbaba=a.

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

[3] aaba=aaa

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

aa bb bbaba

Critical pair: aaa=aaba.

Flip LHS and RHS.

Referenced by [4], [7].

[4] ababa=aaa

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

aab b bbaba

Critical pair: aaba=ababa.

Reduce LHS:

[3](aaba)
⇒ aaa

Flip LHS and RHS.

Referenced by [5], [7].

[5] bbaaa=aba

Overlap of [2] bbaba=a with [4] ababa=aaa:

bb aba ababa

Critical pair: bbaaa=aba.

Referenced by [6], [7], [8].

[6] ababb=bbaa

Overlap of [5] bbaaa=aba with [1] aabb=a:

bba aa aabb

Critical pair: bbaa=ababb.

Flip LHS and RHS.

Referenced by [9].

[7] abaa=aaa

Overlap of [5] bbaaa=aba with [3] aaba=aaa:

bba aa aaba

Critical pair: bbaaaa=ababa.

Reduce LHS:

[5](bbaaa)a
⇒ abaa

Reduce RHS:

[4](ababa)
⇒ aaa

Referenced by [8].

[8] aba=aa

Overlap of [2] bbaba=a with [7] abaa=aaa:

bb aba abaa

Critical pair: bbaaa=aa.

Reduce LHS:

[5](bbaaa)
⇒ aba

Defines rule #1.

Referenced by [9].

[9] bbaa=a

Simplify [6] ababb=bbaa.

Reduce LHS:

[8](aba)bb
[1]⇒ (aabb)
⇒ a

Flip LHS and RHS.

Referenced by [10].

[10] bba=abb

Overlap of [9] bbaa=a with [1] aabb=a:

bb aa aabb

Critical pair: bba=abb.

Defines rule #2.