Certificate for #19687 ⟨a, b | aba=a, baabb=aa⟩

Back:⟨a, b | aba=a, baabb=aa⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #3.

Referenced by [3], [4].

[2] baabb=aa

Axiom: baabb=aa.

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

[3] aabb=aaa

Overlap of [1] aba=a with [2] baabb=aa:

a ba baabb

Critical pair: aaa=aabb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] baaa=aaaaa

Overlap of [2] baabb=aa with [2] baabb=aa:

baab b baabb

Critical pair: baabaa=aaaabb.

Reduce LHS:

[1]ba(aba)a
⇒ baaa

Reduce RHS:

[3]aa(aabb)
⇒ aaaaa

Referenced by [5], [6].

[5] aaaaa=aa

Overlap of [2] baabb=aa with [3] aabb=aaa:

b aabb aabb

Critical pair: baaa=aa.

Reduce LHS:

[4](baaa)
⇒ aaaaa

Defines rule #1.

Referenced by [6], [7].

[6] baaa=aa

Simplify [4] baaa=aaaaa.

Reduce RHS:

[5](aaaaa)
⇒ aa

Referenced by [7].

[7] baa=aaaa

Overlap of [6] baaa=aa with [5] aaaaa=aa:

b aaa aaaaa

Critical pair: baa=aaaa.

Defines rule #2.