Certificate for #4136 ⟨a, b | aba=aaa, bab=a⟩

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

Completion settings:

[1] aba=aaa

Axiom: aba=aaa.

Defines rule #2.

Referenced by [4], [5].

[2] bab=a

Axiom: bab=a.

Defines rule #4.

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

[3] baa=aab

Overlap of [2] bab=a with [2] bab=a:

ba b bab

Critical pair: baa=aab.

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

[4] aaaa=aa

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

b ab aba

Critical pair: baaa=aa.

Reduce LHS:

[3](baa)a
[1]⇒ a(aba)
⇒ aaaa

Defines rule #5.

Referenced by [5].

[5] aab=aaa

Overlap of [2] bab=a with [3] baa=aab:

ba b baa

Critical pair: baaab=aaa.

Reduce LHS:

[3](baa)ab
[1]⇒ a(aba)b
[4]⇒ (aaaa)b
⇒ aab

Defines rule #1.

Referenced by [6].

[6] baa=aaa

Simplify [3] baa=aab.

Reduce RHS:

[5](aab)
⇒ aaa

Defines rule #3.