Certificate for #20234 ⟨a, b | aba=a, babb=aaa⟩

Back:⟨a, b | aba=a, babb=aaa⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #3.

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

[2] babb=aaa

Axiom: babb=aaa.

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

[3] abb=aaaa

Overlap of [1] aba=a with [2] babb=aaa:

a ba babb

Critical pair: aaaa=abb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] baaa=aaaaaaa

Overlap of [2] babb=aaa with [2] babb=aaa:

bab b babb

Critical pair: babaaa=aaaabb.

Reduce LHS:

[1]b(aba)aa
⇒ baaa

Reduce RHS:

[3]aaa(abb)
⇒ aaaaaaa

Defines rule #2.

[5] aaaaaaaa=aaa

Overlap of [3] abb=aaaa with [2] babb=aaa:

ab b babb

Critical pair: abaaa=aaaaabb.

Reduce LHS:

[1](aba)aa
⇒ aaa

Reduce RHS:

[3]aaaa(abb)
⇒ aaaaaaaa

Flip LHS and RHS.

Defines rule #1.