Certificate for #4155 ⟨a, b | abb=aaa, bba=b⟩

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

Completion settings:

[1] abb=aaa

Axiom: abb=aaa.

Referenced by [3], [4].

[2] bba=b

Axiom: bba=b.

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

[3] ab=aaaa

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

a bb bba

Critical pair: ab=aaaa.

Defines rule #3.

Referenced by [4], [5].

[4] aaaaaaa=aaa

Overlap of [1] abb=aaa with [3] ab=aaaa:

abb ab

Critical pair: aaaab=aaa.

Reduce LHS:

[3]aaa(ab)
⇒ aaaaaaa

Defines rule #1.

[5] bb=baaa

Overlap of [2] bba=b with [3] ab=aaaa:

bb a ab

Critical pair: bbaaaa=bb.

Reduce LHS:

[2](bba)aaa
⇒ baaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [6].

[6] baaaa=b

Overlap of [2] bba=b with [5] bb=baaa:

bba bb

Critical pair: baaaa=b.

Defines rule #2.