Certificate for #16177 ⟨a, b | aab=ab, baaa=aa⟩

Back:⟨a, b | aab=ab, baaa=aa⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Defines rule #2.

Referenced by [3].

[2] baaa=aa

Axiom: baaa=aa.

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

[3] bab=ab

Overlap of [2] baaa=aa with [1] aab=ab:

ba aa aab

Critical pair: baab=aab.

Reduce LHS:

[1]b(aab)
⇒ bab

Reduce RHS:

[1](aab)
⇒ ab

Defines rule #4.

Referenced by [4].

[4] aaa=aa

Overlap of [3] bab=ab with [2] baaa=aa:

ba b baaa

Critical pair: baaa=abaaa.

Reduce LHS:

[2](baaa)
⇒ aa

Reduce RHS:

[2]a(baaa)
⇒ aaa

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] baa=aa

Overlap of [2] baaa=aa with [4] aaa=aa:

b aaa aaa

Critical pair: baa=aa.

Defines rule #3.