Certificate for #4184 ⟨a, b | bab=aaa, bba=a⟩

Back:⟨a, b | bab=aaa, bba=a⟩

Completion settings:

[1] bab=aaa

Axiom: bab=aaa.

Referenced by [3], [4].

[2] bba=a

Axiom: bba=a.

Defines rule #3.

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

[3] aaaba=baa

Overlap of [1] bab=aaa with [2] bba=a:

ba b bba

Critical pair: baa=aaaba.

Flip LHS and RHS.

Referenced by [5].

[4] ab=baaa

Overlap of [2] bba=a with [1] bab=aaa:

b ba bab

Critical pair: baaa=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] baaaaaaaaaa=baa

Simplify [3] aaaba=baa.

Reduce LHS:

[4]aa(ab)a
[4]⇒ a(ab)aaaa
[4]⇒ (ab)aaaaaaa
⇒ baaaaaaaaaa

Referenced by [6].

[6] aaaaaaaaaa=aa

Overlap of [2] bba=a with [5] baaaaaaaaaa=baa:

b ba baaaaaaaaaa

Critical pair: bbaa=aaaaaaaaaa.

Reduce LHS:

[2](bba)a
⇒ aa

Flip LHS and RHS.

Defines rule #1.