Certificate for #5390 ⟨a, b | aab=ba, aba=aa

Completion settings:

[1] aab=ba

Axiom: aab=ba.

Referenced by [3], [5], [6], [7].

[2] aba=aa

Axiom: aba=aa.

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

[3] baa=aaa

Overlap of [1] aab=ba with [2] aba=aa:

a ab aba

Critical pair: aaa=baa.

Flip LHS and RHS.

Referenced by [4], [5].

[4] aaaa=aaa

Overlap of [2] aba=aa with [3] baa=aaa:

a ba baa

Critical pair: aaaa=aaa.

Referenced by [5].

[5] aaa=aa

Overlap of [3] baa=aaa with [1] aab=ba:

ba a aab

Critical pair: baba=aaaab.

Reduce LHS:

[2]b(aba)
[3](baa)
aaa

Reduce RHS:

[4](aaaa)b
[1]a(aab)
[2](aba)
aa

Defines rule #2.

Referenced by [6].

[6] ba=aa

Overlap of [5] aaa=aa with [1] aab=ba:

a aa aab

Critical pair: aba=aab.

Reduce LHS:

[2](aba)
aa

Reduce RHS:

[1](aab)
ba

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] aab=aa

Simplify [1] aab=ba.

Reduce RHS:

[6](ba)
aa

Defines rule #3.