Certificate for #2292 ⟨a, b | abaaaab=aab⟩

Back:⟨a, b | abaaaab=aab⟩

Completion settings:

[1] abaaaab=aab

Axiom: abaaaab=aab.

Referenced by [3].

[2] aaaab=c

Axiom: aaaab=c.

Referenced by [3], [4].

[3] aab=abc

Overlap of [1] abaaaab=aab with [2] aaaab=c:

ab aaaab aaaab

Critical pair: abc=aab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] abccc=c

Overlap of [2] aaaab=c with [3] aab=abc:

aa aab aab

Critical pair: aaabc=c.

Reduce LHS:

[3]a(aab)c
[3]⇒ (aab)cc
⇒ abccc

Defines rule #3.

Referenced by [5].

[5] ac=cc

Overlap of [3] aab=abc with [4] abccc=c:

a ab abccc

Critical pair: ac=abcccc.

Reduce RHS:

[4](abccc)c
⇒ cc

Defines rule #1.