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

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

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

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

[2] aaabb=aab

Axiom: abab=ba.

Reduce LHS:

[1]a(ba)b
⇒ aaabb

Reduce RHS:

[1](ba)
⇒ aab

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

[3] aaaab=aaab

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

b a aaabb

Critical pair: baab=aabaabb.

Reduce LHS:

[1](ba)ab
[1]⇒ aa(ba)b
[2]⇒ a(aaabb)
⇒ aaab

Reduce RHS:

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

Flip LHS and RHS.

Referenced by [4].

[4] aaab=aab

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

aaab b ba

Critical pair: aaabaab=aaba.

Reduce LHS:

[1]aaa(ba)ab
[3]⇒ a(aaaab)ab
[3]⇒ (aaaab)ab
[1]⇒ aaa(ba)b
[3]⇒ a(aaaab)b
[3]⇒ (aaaab)b
[2]⇒ (aaabb)
⇒ aab

Reduce RHS:

[1]aa(ba)
[3]⇒ (aaaab)
⇒ aaab

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] aabb=aab

Overlap of [2] aaabb=aab with [4] aaab=aab:

aaabb aaab

Critical pair: aabb=aab.

Defines rule #3.