Certificate for #20231 ⟨a, b | aba=a, baab=abb⟩

Back:⟨a, b | aba=a, baab=abb⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #2.

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

[2] abb=baab

Axiom: baab=abb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[3] baaab=baab

Overlap of [1] aba=a with [2] abb=baab:

ab a abb

Critical pair: abbaab=abb.

Reduce LHS:

[2](abb)aab
[1]⇒ ba(aba)ab
⇒ baaab

Reduce RHS:

[2](abb)
⇒ baab

Referenced by [4].

[4] baaa=baa

Overlap of [3] baaab=baab with [1] aba=a:

baa ab aba

Critical pair: baaa=baaba.

Reduce RHS:

[1]ba(aba)
⇒ baa

Referenced by [5].

[5] aaa=aa

Overlap of [1] aba=a with [4] baaa=baa:

a ba baaa

Critical pair: abaa=aaa.

Reduce LHS:

[1](aba)a
⇒ aa

Flip LHS and RHS.

Defines rule #1.