Certificate for #20104 ⟨a, b | aab=b, abbb=aaa⟩

Back:⟨a, b | aab=b, abbb=aaa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

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

[2] abbb=aaa

Axiom: abbb=aaa.

Referenced by [3], [6].

[3] bbb=aaaa

Overlap of [1] aab=b with [2] abbb=aaa:

a ab abbb

Critical pair: aaaa=bbb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] aaaaaa=aaaa

Overlap of [1] aab=b with [3] bbb=aaaa:

aa b bbb

Critical pair: aaaaaa=bbb.

Reduce RHS:

[3](bbb)
⇒ aaaa

Referenced by [6].

[5] baaaa=b

Overlap of [3] bbb=aaaa with [3] bbb=aaaa:

b bb bbb

Critical pair: baaaa=aaaab.

Reduce RHS:

[1]aa(aab)
[1]⇒ (aab)
⇒ b

Referenced by [6], [7], [8].

[6] aaaaa=aaa

Overlap of [2] abbb=aaa with [5] baaaa=b:

abb b baaaa

Critical pair: abbb=aaaaaaa.

Reduce LHS:

[2](abbb)
⇒ aaa

Reduce RHS:

[4](aaaaaa)a
⇒ aaaaa

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] baaa=ba

Overlap of [5] baaaa=b with [6] aaaaa=aaa:

b aaaa aaaaa

Critical pair: baaa=ba.

Referenced by [8].

[8] baa=b

Overlap of [5] baaaa=b with [7] baaa=ba:

baaaa baaa

Critical pair: baa=b.

Defines rule #2.