Certificate for #20140 ⟨a, b | aab=b, babb=baa⟩

Back:⟨a, b | aab=b, babb=baa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3].

[2] babb=baa

Axiom: babb=baa.

Defines rule #2.

Referenced by [3].

[3] baaaa=baa

Overlap of [2] babb=baa with [2] babb=baa:

bab b babb

Critical pair: babbaa=baaabb.

Reduce LHS:

[2](babb)aa
⇒ baaaa

Reduce RHS:

[1]ba(aab)b
[2]⇒ (babb)
⇒ baa

Defines rule #3.