Certificate for #19795 ⟨a, b | aaa=a, aaba=bab⟩

Back:⟨a, b | aaa=a, aaba=bab⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [3], [4].

[2] bab=aaba

Axiom: aaba=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aabaab=aabaa

Overlap of [2] bab=aaba with [2] bab=aaba:

ba b bab

Critical pair: baaaba=aabaab.

Reduce LHS:

[1]b(aaa)ba
[2]⇒ (bab)a
⇒ aabaa

Flip LHS and RHS.

Referenced by [4].

[4] abaab=abaa

Overlap of [1] aaa=a with [3] aabaab=aabaa:

a aa aabaab

Critical pair: aaabaa=abaab.

Reduce LHS:

[1](aaa)baa
⇒ abaa

Flip LHS and RHS.

Defines rule #3.