Certificate for #16308 ⟨a, b | aab=bb, baaa=bb⟩

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

Completion settings:

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Referenced by [2], [3].

[2] aab=baaa

Axiom: baaa=bb.

Reduce RHS:

[1](bb)
⇒ aab

Flip LHS and RHS.

Defines rule #2.

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

[3] bb=baaa

Simplify [1] bb=aab.

Reduce RHS:

[2](aab)
⇒ baaa

Defines rule #3.

Referenced by [4], [5].

[4] babaaa=baaaaaa

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

b b bb

Critical pair: bbaaa=baaab.

Reduce LHS:

[3](bb)aaa
⇒ baaaaaa

Reduce RHS:

[2]ba(aab)
⇒ babaaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] baaaaaaaaaaaa=baaaaaaaaa

Overlap of [3] bb=baaa with [4] babaaa=baaaaaa:

b b babaaa

Critical pair: bbaaaaaa=baaaabaaa.

Reduce LHS:

[3](bb)aaaaaa
⇒ baaaaaaaaa

Reduce RHS:

[2]baa(aab)aaa
[2]⇒ b(aab)aaaaaa
[3]⇒ (bb)aaaaaaaaa
⇒ baaaaaaaaaaaa

Flip LHS and RHS.

Defines rule #1.