Certificate for #2496 ⟨a, b | aababa=aaab⟩

Back:⟨a, b | aababa=aaab⟩

Completion settings:

[1] aababa=aaab

Axiom: aababa=aaab.

Defines rule #1.

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

[2] aaabaab=aaaabba

Overlap of [1] aababa=aaab with [1] aababa=aaab:

aabab a aababa

Critical pair: aababaaab=aaabababa.

Reduce LHS:

[1](aababa)aab
⇒ aaabaab

Reduce RHS:

[1]a(aababa)ba
⇒ aaaabba

Defines rule #2.

Referenced by [3], [4].

[3] aaabaaabba=aaaabbaaab

Overlap of [1] aababa=aaab with [2] aaabaab=aaaabba:

aabab a aaabaab

Critical pair: aababaaaabba=aaabaabaab.

Reduce LHS:

[1](aababa)aaabba
⇒ aaabaaabba

Reduce RHS:

[2](aaabaab)aab
⇒ aaaabbaaab

Defines rule #4.

[4] aaaabbaaba=aaabaaab

Overlap of [2] aaabaab=aaaabba with [1] aababa=aaab:

aaab aab aababa

Critical pair: aaabaaab=aaaabbaaba.

Flip LHS and RHS.

Defines rule #3.