Certificate for #16292 ⟨a, b | aab=bb, abaa=bb⟩

Back:⟨a, b | aab=bb, abaa=bb⟩

Completion settings:

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Referenced by [2], [3].

[2] aab=abaa

Axiom: abaa=bb.

Reduce RHS:

[1](bb)
⇒ aab

Flip LHS and RHS.

Defines rule #2.

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

[3] bb=abaa

Simplify [1] bb=aab.

Reduce RHS:

[2](aab)
⇒ abaa

Defines rule #3.

Referenced by [4], [5].

[4] ababaa=babaa

Overlap of [3] bb=abaa with [3] bb=abaa:

b b bb

Critical pair: babaa=abaab.

Reduce RHS:

[2]ab(aab)
⇒ ababaa

Flip LHS and RHS.

Referenced by [5], [6].

[5] babaa=abaaaaaa

Overlap of [2] aab=abaa with [3] bb=abaa:

aa b bb

Critical pair: aaabaa=abaab.

Reduce LHS:

[2]a(aab)aa
[2]⇒ (aab)aaaa
⇒ abaaaaaa

Reduce RHS:

[2]ab(aab)
[4]⇒ (ababaa)
⇒ babaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [6].

[6] abaaaaaaaa=abaaaaaa

Simplify [4] ababaa=babaa.

Reduce LHS:

[5]a(babaa)
[2]⇒ (aab)aaaaaa
⇒ abaaaaaaaa

Reduce RHS:

[5](babaa)
⇒ abaaaaaa

Defines rule #1.