Certificate for #6818 ⟨a, b | aab=b, abb=aaa⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

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

[2] abb=aaa

Axiom: abb=aaa.

Referenced by [3], [6].

[3] bb=aaaa

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

a ab abb

Critical pair: aaaa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] aaaaaa=aaaa

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

aa b bb

Critical pair: aaaaaa=bb.

Reduce RHS:

[3](bb)
⇒ aaaa

Referenced by [6].

[5] baaaa=b

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

b b bb

Critical pair: baaaa=aaaab.

Reduce RHS:

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

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

[6] aaaaa=aaa

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

ab b baaaa

Critical pair: abb=aaaaaaa.

Reduce LHS:

[2](abb)
⇒ 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.