Certificate for #14493 ⟨a, b | aaab=b, ababa=a⟩

Back:⟨a, b | aaab=b, ababa=a⟩

Completion settings:

[1] aaab=b

Axiom: aaab=b.

Defines rule #2.

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

[2] ababa=a

Axiom: ababa=a.

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

[3] baba=aaa

Overlap of [1] aaab=b with [2] ababa=a:

aa ab ababa

Critical pair: aaa=baba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[4] ababb=b

Overlap of [2] ababa=a with [1] aaab=b:

abab a aaab

Critical pair: ababb=aaab.

Reduce RHS:

[1](aaab)
⇒ b

Referenced by [5].

[5] babb=aab

Overlap of [1] aaab=b with [4] ababb=b:

aa ab ababb

Critical pair: aab=babb.

Flip LHS and RHS.

Defines rule #4.

[6] baaaa=ba

Overlap of [3] baba=aaa with [3] baba=aaa:

ba ba baba

Critical pair: baaaa=aaaba.

Reduce RHS:

[1](aaab)a
⇒ ba

Referenced by [7].

[7] aaaa=a

Overlap of [2] ababa=a with [6] baaaa=ba:

aba ba baaaa

Critical pair: ababa=aaaa.

Reduce LHS:

[2](ababa)
⇒ a

Flip LHS and RHS.

Defines rule #1.