Certificate for #16212 ⟨a, b | aab=ba, aaaa=bb⟩

Back:⟨a, b | aab=ba, aaaa=bb⟩

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[2] bb=aaaa

Axiom: aaaa=bb.

Flip LHS and RHS.

Defines rule #4.

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

[3] aaaaaaaa=aaaaa

Overlap of [2] bb=aaaa with [1] ba=aab:

b b ba

Critical pair: baab=aaaaa.

Reduce LHS:

[1](ba)ab
[1]⇒ aa(ba)b
[2]⇒ aaaa(bb)
⇒ aaaaaaaa

Referenced by [4], [5].

[4] aaaaab=aaaab

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

b b bb

Critical pair: baaaa=aaaab.

Reduce LHS:

[1](ba)aaa
[1]⇒ aa(ba)aa
[1]⇒ aaaa(ba)a
[1]⇒ aaaaaa(ba)
[3]⇒ (aaaaaaaa)b
⇒ aaaaab

Defines rule #2.

Referenced by [5].

[5] aaaaaa=aaaaa

Overlap of [4] aaaaab=aaaab with [2] bb=aaaa:

aaaaa b bb

Critical pair: aaaaaaaaa=aaaabb.

Reduce LHS:

[3](aaaaaaaa)a
⇒ aaaaaa

Reduce RHS:

[2]aaaa(bb)
[3]⇒ (aaaaaaaa)
⇒ aaaaa

Defines rule #1.