Certificate for #19560 ⟨a, b | aab=b, abbba=aa⟩

Back:⟨a, b | aab=b, abbba=aa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

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

[2] abbba=aa

Axiom: abbba=aa.

Referenced by [3], [5].

[3] bbba=aaa

Overlap of [1] aab=b with [2] abbba=aa:

a ab abbba

Critical pair: aaa=bbba.

Flip LHS and RHS.

Defines rule #4.

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

[4] bbbb=b

Overlap of [3] bbba=aaa with [1] aab=b:

bbb a aab

Critical pair: bbbb=aaaab.

Reduce RHS:

[1]aa(aab)
[1]⇒ (aab)
⇒ b

Defines rule #5.

Referenced by [6].

[5] aaaa=aa

Overlap of [3] bbba=aaa with [2] abbba=aa:

bbb a abbba

Critical pair: bbbaa=aaabbba.

Reduce LHS:

[3](bbba)a
⇒ aaaa

Reduce RHS:

[1]a(aab)bba
[2]⇒ (abbba)
⇒ aa

Defines rule #2.

[6] baaa=ba

Overlap of [4] bbbb=b with [3] bbba=aaa:

b bbb bbba

Critical pair: baaa=ba.

Defines rule #3.