Certificate for #20112 ⟨a, b | aab=b, baaa=aaa⟩

Back:⟨a, b | aab=b, baaa=aaa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

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

[2] baaa=aaa

Axiom: baaa=aaa.

Defines rule #4.

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

[3] aaaaa=aaa

Overlap of [1] aab=b with [2] baaa=aaa:

aa b baaa

Critical pair: aaaaa=baaa.

Reduce RHS:

[2](baaa)
⇒ aaa

Defines rule #5.

[4] bab=ab

Overlap of [2] baaa=aaa with [1] aab=b:

ba aa aab

Critical pair: bab=aaab.

Reduce RHS:

[1]a(aab)
⇒ ab

Defines rule #3.

[5] bb=b

Overlap of [2] baaa=aaa with [1] aab=b:

baa a aab

Critical pair: baab=aaaab.

Reduce LHS:

[1]b(aab)
⇒ bb

Reduce RHS:

[1]aa(aab)
[1]⇒ (aab)
⇒ b

Defines rule #1.