Certificate for #13100 ⟨a, b | bab=aba, aaaa=a⟩

Back:⟨a, b | bab=aba, aaaa=a⟩

Completion settings:

[1] bab=aba

Axiom: bab=aba.

Defines rule #1.

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

[2] aaaa=a

Axiom: aaaa=a.

Defines rule #2.

Referenced by [5], [6], [8].

[3] baaba=abaab

Overlap of [1] bab=aba with [1] bab=aba:

ba b bab

Critical pair: baaba=abaab.

Defines rule #3.

Referenced by [4], [6], [9].

[4] baaaba=abaabb

Overlap of [3] baaba=abaab with [1] bab=aba:

baa ba bab

Critical pair: baaaba=abaabb.

Defines rule #4.

Referenced by [5], [6].

[5] abaabbb=abaa

Overlap of [4] baaaba=abaabb with [1] bab=aba:

baaa ba bab

Critical pair: baaaaba=abaabbb.

Reduce LHS:

[2]b(aaaa)ba
[1]⇒ (bab)a
⇒ abaa

Flip LHS and RHS.

Defines rule #5.

Referenced by [7].

[6] aabaabbaa=abaaab

Overlap of [4] baaaba=abaabb with [3] baaba=abaab:

baaa ba baaba

Critical pair: baaaabaab=abaabbaba.

Reduce LHS:

[2]b(aaaa)baab
[1]⇒ (bab)aab
⇒ abaaab

Reduce RHS:

[1]abaab(bab)a
[3]⇒ a(baaba)baa
⇒ aabaabbaa

Flip LHS and RHS.

Referenced by [8], [9].

[7] abaaabbb=abaaa

Overlap of [1] bab=aba with [5] abaabbb=abaa:

b ab abaabbb

Critical pair: babaa=abaaabbb.

Reduce LHS:

[1](bab)aa
⇒ abaaa

Flip LHS and RHS.

Defines rule #7.

[8] abaabbaa=aaabaaab

Overlap of [2] aaaa=a with [6] aabaabbaa=abaaab:

aa aa aabaabbaa

Critical pair: aaabaaab=abaabbaa.

Flip LHS and RHS.

Defines rule #8.

[9] abaaabba=aabaaabb

Overlap of [6] aabaabbaa=abaaab with [3] baaba=abaab:

aabaab baa baaba

Critical pair: aabaababaab=abaaabba.

Reduce LHS:

[3]aa(baaba)baab
[6]⇒ a(aabaabbaa)b
⇒ aabaaabb

Flip LHS and RHS.

Defines rule #6.