Certificate for #18734 ⟨a, b | aaa=a, abbbab=a⟩

Back:⟨a, b | aaa=a, abbbab=a⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [8].

[2] abbbab=a

Axiom: abbbab=a.

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

[3] abbba=abbab

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

abbb ab abbbab

Critical pair: abbba=abbab.

Referenced by [4], [5], [7], [8], [12].

[4] abbabb=a

Overlap of [2] abbbab=a with [3] abbba=abbab:

abbbab abbba

Critical pair: abbabb=a.

Referenced by [5], [6].

[5] abba=abab

Overlap of [2] abbbab=a with [3] abbba=abbab:

abbb ab abbba

Critical pair: abbbabbab=abba.

Reduce LHS:

[3](abbba)bbab
[4]⇒ (abbabb)bab
⇒ abab

Flip LHS and RHS.

Referenced by [6], [7], [8], [11].

[6] ababbb=a

Simplify [4] abbabb=a.

Reduce LHS:

[5](abba)bb
⇒ ababbb

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

[7] ababb=aabbb

Overlap of [2] abbbab=a with [6] ababbb=a:

abbb ab ababbb

Critical pair: abbba=aabbb.

Reduce LHS:

[3](abbba)
[5]⇒ (abba)b
⇒ ababb

Referenced by [8].

[8] abbbb=aa

Overlap of [6] ababbb=a with [3] abbba=abbab:

ab abbb abbba

Critical pair: ababbab=aa.

Reduce LHS:

[7](ababb)ab
[3]⇒ a(abbba)b
[5]⇒ a(abba)bb
[7]⇒ a(ababb)b
[1]⇒ (aaa)bbbb
⇒ abbbb

Defines rule #5.

Referenced by [9], [10].

[9] abaa=ab

Overlap of [6] ababbb=a with [8] abbbb=aa:

ab abbb abbbb

Critical pair: abaa=ab.

Referenced by [10].

[10] aba=aab

Overlap of [9] abaa=ab with [8] abbbb=aa:

aba a abbbb

Critical pair: abaaa=abbbbb.

Reduce LHS:

[9](abaa)a
⇒ aba

Reduce RHS:

[8](abbbb)b
⇒ aab

Defines rule #2.

Referenced by [11].

[11] abba=aabb

Simplify [5] abba=abab.

Reduce RHS:

[10](aba)b
⇒ aabb

Defines rule #3.

Referenced by [12].

[12] abbba=aabbb

Simplify [3] abbba=abbab.

Reduce RHS:

[11](abba)b
⇒ aabbb

Defines rule #4.