Certificate for #4812 ⟨a, b | ababaaab=aab⟩

Back:⟨a, b | ababaaab=aab⟩

Completion settings:

[1] ababaaab=aab

Axiom: ababaaab=aab.

Referenced by [3].

[2] ababaa=c

Axiom: ababaa=c.

Defines rule #4.

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

[3] aab=cab

Overlap of [1] ababaaab=aab with [2] ababaa=c:

ababaaab ababaa

Critical pair: cab=aab.

Flip LHS and RHS.

Defines rule #2.

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

[4] ababcab=cb

Overlap of [2] ababaa=c with [3] aab=cab:

abab aa aab

Critical pair: ababcab=cb.

Defines rule #6.

Referenced by [7].

[5] ababacab=cab

Overlap of [2] ababaa=c with [3] aab=cab:

ababa a aab

Critical pair: ababacab=cab.

Referenced by [8].

[6] ac=cc

Overlap of [3] aab=cab with [2] ababaa=c:

a ab ababaa

Critical pair: ac=cababaa.

Reduce RHS:

[2]c(ababaa)
⇒ cc

Defines rule #1.

Referenced by [8].

[7] ababcc=cbabaa

Overlap of [4] ababcab=cb with [2] ababaa=c:

ababc ab ababaa

Critical pair: ababcc=cbabaa.

Defines rule #3.

Referenced by [8].

[8] cbabccab=cab

Simplify [5] ababacab=cab.

Reduce LHS:

[6]abab(ac)ab
[7]⇒ (ababcc)ab
[3]⇒ cbaba(aab)
[6]⇒ cbab(ac)ab
⇒ cbabccab

Defines rule #7.

Referenced by [9].

[9] cbabccc=cc

Overlap of [8] cbabccab=cab with [2] ababaa=c:

cbabcc ab ababaa

Critical pair: cbabccc=cababaa.

Reduce RHS:

[2]c(ababaa)
⇒ cc

Defines rule #5.