Certificate for #16275 ⟨a, b | aab=bb, aaaa=ba⟩

Back:⟨a, b | aab=bb, aaaa=ba⟩

Completion settings:

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[2] ba=aaaa

Axiom: aaaa=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] aaaaab=aaaab

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

b b bb

Critical pair: baab=aabb.

Reduce LHS:

[2](ba)ab
⇒ aaaaab

Reduce RHS:

[1]aa(bb)
⇒ aaaab

Defines rule #3.

[4] aaaaaaa=aaaaaa

Overlap of [1] bb=aab with [2] ba=aaaa:

b b ba

Critical pair: baaaa=aaba.

Reduce LHS:

[2](ba)aaa
⇒ aaaaaaa

Reduce RHS:

[2]aa(ba)
⇒ aaaaaa

Defines rule #1.