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

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

Completion settings:

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Referenced by [3].

[2] ab=baaa

Axiom: baaa=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] bb=baaaaaa

Simplify [1] bb=aab.

Reduce RHS:

[2]a(ab)
[2]⇒ (ab)aaa
⇒ baaaaaa

Defines rule #3.

Referenced by [4].

[4] baaaaaaaaaaaaaaa=baaaaaaaaa

Overlap of [2] ab=baaa with [3] bb=baaaaaa:

a b bb

Critical pair: abaaaaaa=baaab.

Reduce LHS:

[2](ab)aaaaaa
⇒ baaaaaaaaa

Reduce RHS:

[2]baa(ab)
[2]⇒ ba(ab)aaa
[2]⇒ b(ab)aaaaaa
[3]⇒ (bb)aaaaaaaaa
⇒ baaaaaaaaaaaaaaa

Flip LHS and RHS.

Defines rule #1.