Certificate for #16230 ⟨a, b | aab=ba, abab=ab⟩

Back:⟨a, b | aab=ba, abab=ab⟩

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [2], [3].

[2] aaabb=ab

Axiom: abab=ab.

Reduce LHS:

[1]a(ba)b
⇒ aaabb

Referenced by [3], [4].

[3] aabb=aab

Overlap of [1] ba=aab with [2] aaabb=ab:

b a aaabb

Critical pair: bab=aabaabb.

Reduce LHS:

[1](ba)b
⇒ aabb

Reduce RHS:

[1]aa(ba)abb
[1]⇒ aaaa(ba)bb
[2]⇒ aaa(aaabb)b
[2]⇒ a(aaabb)
⇒ aab

Referenced by [4], [5].

[4] aaab=ab

Overlap of [2] aaabb=ab with [3] aabb=aab:

a aabb aabb

Critical pair: aaab=ab.

Defines rule #1.

Referenced by [5].

[5] abb=ab

Overlap of [4] aaab=ab with [3] aabb=aab:

a aab aabb

Critical pair: aaab=abb.

Reduce LHS:

[4](aaab)
⇒ ab

Flip LHS and RHS.

Defines rule #3.