Certificate for #13232 ⟨a, b | baa=abb, bab=aa⟩

Back:⟨a, b | baa=abb, bab=aa⟩

Completion settings:

[1] baa=abb

Axiom: baa=abb.

Referenced by [3].

[2] aa=bab

Axiom: bab=aa.

Flip LHS and RHS.

Defines rule #3.

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

[3] abb=bbab

Overlap of [1] baa=abb with [2] aa=bab:

b aa aa

Critical pair: bbab=abb.

Flip LHS and RHS.

Defines rule #2.

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

[4] abab=baba

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

a a aa

Critical pair: abab=baba.

Defines rule #5.

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

[5] bbbaba=bbbbbab

Overlap of [2] aa=bab with [3] abb=bbab:

a a abb

Critical pair: abbab=babbb.

Reduce LHS:

[3](abb)ab
[4]⇒ bb(abab)
⇒ bbbaba

Reduce RHS:

[3]b(abb)b
[3]⇒ bbb(abb)
⇒ bbbbbab

Referenced by [6], [7].

[6] bbaba=bbbbbbbab

Overlap of [4] abab=baba with [3] abb=bbab:

ab ab abb

Critical pair: abbbab=babab.

Reduce LHS:

[3](abb)bab
[3]⇒ bb(abb)ab
[4]⇒ bbbb(abab)
[5]⇒ bb(bbbaba)
⇒ bbbbbbbab

Reduce RHS:

[4]b(abab)
⇒ bbaba

Flip LHS and RHS.

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

[7] bbbbbbbbab=bbbbbab

Simplify [5] bbbaba=bbbbbab.

Reduce LHS:

[6]b(bbaba)
⇒ bbbbbbbbab

Referenced by [8].

[8] bbbbbbab=bbbbbab

Overlap of [3] abb=bbab with [6] bbaba=bbbbbbbab:

a bb bbaba

Critical pair: abbbbbbbab=bbababa.

Reduce LHS:

[3](abb)bbbbbab
[3]⇒ bb(abb)bbbbab
[3]⇒ bbbb(abb)bbbab
[3]⇒ bbbbbb(abb)bbab
[7]⇒ (bbbbbbbbab)bbab
[3]⇒ bbbbb(abb)bab
[3]⇒ bbbbbbb(abb)ab
[7]⇒ b(bbbbbbbbab)ab
[4]⇒ bbbbbb(abab)
[6]⇒ bbbbb(bbaba)
[7]⇒ bbbb(bbbbbbbbab)
[7]⇒ b(bbbbbbbbab)
⇒ bbbbbbab

Reduce RHS:

[4]bb(abab)a
[2]⇒ bbbab(aa)
[3]⇒ bbb(abb)ab
[4]⇒ bbbbb(abab)
[6]⇒ bbbb(bbaba)
[7]⇒ bbb(bbbbbbbbab)
[7]⇒ (bbbbbbbbab)
⇒ bbbbbab

Defines rule #1.

Referenced by [9].

[9] bbaba=bbbbbab

Simplify [6] bbaba=bbbbbbbab.

Reduce RHS:

[8]b(bbbbbbab)
[8]⇒ (bbbbbbab)
⇒ bbbbbab

Defines rule #4.