Certificate for #5404 ⟨a, b | aab=bb, aba=aa⟩

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

Completion settings:

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [3].

[2] aba=aa

Axiom: aba=aa.

Defines rule #3.

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

[3] baab=aaaab

Overlap of [1] bb=aab with [1] bb=aab:

b b bb

Critical pair: baab=aabb.

Reduce RHS:

[1]aa(bb)
⇒ aaaab

Defines rule #6.

Referenced by [4], [5].

[4] aaaaab=aaab

Overlap of [2] aba=aa with [3] baab=aaaab:

a ba baab

Critical pair: aaaaab=aaab.

Defines rule #4.

[5] baaa=aaaaa

Overlap of [3] baab=aaaab with [2] aba=aa:

ba ab aba

Critical pair: baaa=aaaaba.

Reduce RHS:

[2]aaa(aba)
⇒ aaaaa

Defines rule #2.

Referenced by [6].

[6] aaaaaa=aaaa

Overlap of [2] aba=aa with [5] baaa=aaaaa:

a ba baaa

Critical pair: aaaaaa=aaaa.

Defines rule #1.