Certificate for #15603 ⟨a, b | aab=aa, bbbab=a⟩

Back:⟨a, b | aab=aa, bbbab=a⟩

Completion settings:

[1] aab=aa

Axiom: aab=aa.

Defines rule #1.

Referenced by [4], [5].

[2] bbbab=a

Axiom: bbbab=a.

Defines rule #5.

Referenced by [3], [6], [7], [8], [9].

[3] bbbaa=abbab

Overlap of [2] bbbab=a with [2] bbbab=a:

bbba b bbbab

Critical pair: bbbaa=abbab.

Defines rule #4.

Referenced by [4], [5].

[4] abbabb=abbab

Overlap of [3] bbbaa=abbab with [1] aab=aa:

bbb aa aab

Critical pair: bbbaa=abbabb.

Reduce LHS:

[3](bbbaa)
⇒ abbab

Flip LHS and RHS.

Defines rule #7.

Referenced by [6], [7].

[5] abbabab=abbaba

Overlap of [3] bbbaa=abbab with [1] aab=aa:

bbba a aab

Critical pair: bbbaaa=abbabab.

Reduce LHS:

[3](bbbaa)a
⇒ abbaba

Flip LHS and RHS.

Referenced by [7].

[6] ababb=abab

Overlap of [2] bbbab=a with [4] abbabb=abbab:

bbb ab abbabb

Critical pair: bbbabbab=ababb.

Reduce LHS:

[2](bbbab)bab
⇒ abab

Flip LHS and RHS.

Defines rule #3.

Referenced by [8], [9].

[7] abbaba=abbaa

Overlap of [4] abbabb=abbab with [2] bbbab=a:

abba bb bbbab

Critical pair: abbaa=abbabbab.

Reduce RHS:

[4](abbabb)ab
[5]⇒ (abbabab)
⇒ abbaba

Flip LHS and RHS.

Defines rule #6.

[8] ababab=abaa

Overlap of [6] ababb=abab with [2] bbbab=a:

aba bb bbbab

Critical pair: abaa=ababbab.

Reduce RHS:

[6](ababb)ab
⇒ ababab

Flip LHS and RHS.

Referenced by [9].

[9] ababa=abaa

Overlap of [6] ababb=abab with [2] bbbab=a:

abab b bbbab

Critical pair: ababa=ababbbab.

Reduce RHS:

[6](ababb)bab
[6]⇒ (ababb)ab
[8]⇒ (ababab)
⇒ abaa

Defines rule #2.