Certificate for #8614 ⟨a, b | aa=a, abbbab=a⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [7], [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], [11].

[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], [10].

[6] ababbb=a

Simplify [4] abbabb=a.

Reduce LHS:

[5](abba)bb
⇒ ababbb

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

[7] ababb=abbb

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

abbb ab ababbb

Critical pair: abbba=aabbb.

Reduce LHS:

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

Reduce RHS:

[1](aa)bbb
⇒ abbb

Referenced by [8].

[8] abbbb=a

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

ab abbb abbba

Critical pair: ababbab=aa.

Reduce LHS:

[7](ababb)ab
[3]⇒ (abbba)b
[5]⇒ (abba)bb
[7]⇒ (ababb)b
⇒ abbbb

Reduce RHS:

[1](aa)
⇒ a

Defines rule #5.

Referenced by [9].

[9] aba=ab

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

ab abbb abbbb

Critical pair: aba=ab.

Defines rule #2.

Referenced by [10].

[10] abba=abb

Simplify [5] abba=abab.

Reduce RHS:

[9](aba)b
⇒ abb

Defines rule #3.

Referenced by [11].

[11] abbba=abbb

Simplify [3] abbba=abbab.

Reduce RHS:

[10](abba)b
⇒ abbb

Defines rule #4.