Certificate for #12196 ⟨a, b | aaaa=bb, aaab=a⟩

Back:⟨a, b | aaaa=bb, aaab=a⟩

Completion settings:

[1] aaaa=bb

Axiom: aaaa=bb.

Defines rule #3.

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

[2] aaab=a

Axiom: aaab=a.

Defines rule #4.

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

[3] bba=abb

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

a aaa aaaa

Critical pair: abb=bba.

Flip LHS and RHS.

Referenced by [7], [8].

[4] bbb=aa

Overlap of [1] aaaa=bb with [2] aaab=a:

a aaa aaab

Critical pair: aa=bbb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [7].

[5] baa=aab

Overlap of [4] bbb=aa with [4] bbb=aa:

b bb bbb

Critical pair: baa=aab.

Referenced by [6], [8].

[6] aabab=ba

Overlap of [5] baa=aab with [2] aaab=a:

b aa aaab

Critical pair: ba=aabab.

Flip LHS and RHS.

Referenced by [8].

[7] aba=aab

Overlap of [2] aaab=a with [3] bba=abb:

aaa b bba

Critical pair: aaaabb=aba.

Reduce LHS:

[1](aaaa)bb
[4]⇒ (bbb)b
⇒ aab

Flip LHS and RHS.

Referenced by [8].

[8] ba=ab

Overlap of [5] baa=aab with [7] aba=aab:

ba a aba

Critical pair: baaab=aabba.

Reduce LHS:

[5](baa)ab
[6]⇒ (aabab)
⇒ ba

Reduce RHS:

[3]aa(bba)
[2]⇒ (aaab)b
⇒ ab

Defines rule #1.