Certificate for #20117 ⟨a, b | aab=b, baaa=bab⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

Referenced by [3], [4].

[2] bab=baaa

Axiom: baaa=bab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[3] bb=baaaaaa

Overlap of [2] bab=baaa with [2] bab=baaa:

ba b bab

Critical pair: babaaa=baaaab.

Reduce LHS:

[2](bab)aaa
⇒ baaaaaa

Reduce RHS:

[1]baa(aab)
[1]⇒ b(aab)
⇒ bb

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] baaaaaaaaa=baaa

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

ba b bb

Critical pair: babaaaaaa=baaab.

Reduce LHS:

[2](bab)aaaaaa
⇒ baaaaaaaaa

Reduce RHS:

[1]ba(aab)
[2]⇒ (bab)
⇒ baaa

Defines rule #1.