Certificate for #14351 ⟨a, b | aaaa=a, abbab=a⟩

Back:⟨a, b | aaaa=a, abbab=a⟩

Completion settings:

[1] aaaa=a

Axiom: aaaa=a.

Defines rule #2.

Referenced by [7].

[2] abbab=a

Axiom: abbab=a.

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

[3] abba=abab

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

abb ab abbab

Critical pair: abba=abab.

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

[4] ababb=a

Overlap of [2] abbab=a with [3] abba=abab:

abbab abba

Critical pair: ababb=a.

Referenced by [5], [6].

[5] aba=aab

Overlap of [2] abbab=a with [3] abba=abab:

abb ab abba

Critical pair: abbabab=aba.

Reduce LHS:

[3](abba)bab
[4]⇒ (ababb)ab
⇒ aab

Flip LHS and RHS.

Defines rule #1.

Referenced by [6], [8].

[6] aabbb=a

Simplify [4] ababb=a.

Reduce LHS:

[5](aba)bb
⇒ aabbb

Referenced by [7].

[7] abbb=aaa

Overlap of [1] aaaa=a with [6] aabbb=a:

aa aa aabbb

Critical pair: aaa=abbb.

Flip LHS and RHS.

Defines rule #4.

[8] abba=aabb

Simplify [3] abba=abab.

Reduce RHS:

[5](aba)b
⇒ aabb

Defines rule #3.