Certificate for #16313 ⟨a, b | aab=bb, baba=aa⟩

Back:⟨a, b | aab=bb, baba=aa⟩

Completion settings:

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3].

[2] baba=aa

Axiom: baba=aa.

Defines rule #5.

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

[3] baa=aaaa

Overlap of [1] bb=aab with [2] baba=aa:

b b baba

Critical pair: baa=aababa.

Reduce RHS:

[2]aa(baba)
⇒ aaaa

Defines rule #2.

Referenced by [4], [5].

[4] aaba=aaaaa

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

ba ba baba

Critical pair: baaa=aaba.

Reduce LHS:

[3](baa)a
⇒ aaaaa

Flip LHS and RHS.

Defines rule #3.

[5] aaaaaaa=aaa

Overlap of [2] baba=aa with [3] baa=aaaa:

ba ba baa

Critical pair: baaaaa=aaa.

Reduce LHS:

[3](baa)aaa
⇒ aaaaaaa

Defines rule #1.