Certificate for #14824 ⟨a, b | abba=a, baabb=b⟩

Back:⟨a, b | abba=a, baabb=b⟩

Completion settings:

[1] abba=a

Axiom: abba=a.

Defines rule #2.

Referenced by [3], [4].

[2] baabb=b

Axiom: baabb=b.

Referenced by [3], [5].

[3] baa=ba

Overlap of [2] baabb=b with [1] abba=a:

ba abb abba

Critical pair: baa=ba.

Referenced by [4], [5].

[4] aa=a

Overlap of [1] abba=a with [3] baa=ba:

ab ba baa

Critical pair: abba=aa.

Reduce LHS:

[1](abba)
⇒ a

Flip LHS and RHS.

Defines rule #1.

[5] babb=b

Overlap of [2] baabb=b with [3] baa=ba:

baabb baa

Critical pair: babb=b.

Defines rule #3.