Certificate for #16339 ⟨a, b | aba=aa, aaaa=bb⟩

Back:⟨a, b | aba=aa, aaaa=bb⟩

Completion settings:

[1] aba=aa

Axiom: aba=aa.

Defines rule #3.

Referenced by [4], [5].

[2] bb=aaaa

Axiom: aaaa=bb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [3], [4].

[3] aaaab=baaaa

Overlap of [2] bb=aaaa with [2] bb=aaaa:

b b bb

Critical pair: baaaa=aaaab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] aaaaaaaaa=aaaaa

Overlap of [1] aba=aa with [3] aaaab=baaaa:

ab a aaaab

Critical pair: abbaaaa=aaaaab.

Reduce LHS:

[2]a(bb)aaaa
⇒ aaaaaaaaa

Reduce RHS:

[3]a(aaaab)
[1]⇒ (aba)aaa
⇒ aaaaa

Defines rule #1.

[5] baaaaa=aaaaa

Overlap of [3] aaaab=baaaa with [1] aba=aa:

aaa ab aba

Critical pair: aaaaa=baaaaa.

Flip LHS and RHS.

Defines rule #2.