Certificate for #4153 ⟨a, b | abb=aaa, bab=b⟩

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

Completion settings:

[1] abb=aaa

Axiom: abb=aaa.

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

[2] bab=b

Axiom: bab=b.

Defines rule #5.

Referenced by [3], [4].

[3] aaaab=aaa

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

ab b bab

Critical pair: abb=aaaab.

Reduce LHS:

[1](abb)
⇒ aaa

Flip LHS and RHS.

Referenced by [6].

[4] bb=baaa

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

b ab abb

Critical pair: baaa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [7].

[5] aaab=aaaaaa

Overlap of [1] abb=aaa with [4] bb=baaa:

ab b bb

Critical pair: abbaaa=aaab.

Reduce LHS:

[1](abb)aaa
⇒ aaaaaa

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] aaaaaaa=aaa

Simplify [3] aaaab=aaa.

Reduce LHS:

[5]a(aaab)
⇒ aaaaaaa

Defines rule #1.

[7] abaaa=aaa

Overlap of [1] abb=aaa with [4] bb=baaa:

a bb bb

Critical pair: abaaa=aaa.

Defines rule #2.