Certificate for #9176 ⟨a, b | aa=a, babb=bba⟩

Back:⟨a, b | aa=a, babb=bba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] babb=bba

Axiom: babb=bba.

Defines rule #2.

Referenced by [3], [4].

[3] bbaba=bbba

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

bab b babb

Critical pair: babbba=bbaabb.

Reduce LHS:

[2](babb)ba
⇒ bbaba

Reduce RHS:

[1]bb(aa)bb
[2]⇒ b(babb)
⇒ bbba

Defines rule #3.

Referenced by [4].

[4] bbbba=bbba

Overlap of [2] babb=bba with [3] bbaba=bbba:

bab b bbaba

Critical pair: babbbba=bbababa.

Reduce LHS:

[2](babb)bba
[2]⇒ b(babb)a
[1]⇒ bbb(aa)
⇒ bbba

Reduce RHS:

[3](bbaba)ba
[3]⇒ b(bbaba)
⇒ bbbba

Flip LHS and RHS.

Defines rule #4.