Certificate for #4112 ⟨a, b | aababaaba=aa⟩

Back:⟨a, b | aababaaba=aa⟩

Completion settings:

[1] aababaaba=aa

Axiom: aababaaba=aa.

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

[2] aababaa=aabaaba

Overlap of [1] aababaaba=aa with [1] aababaaba=aa:

aabab aaba aababaaba

Critical pair: aababaa=aabaaba.

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

[3] aabaababa=aa

Overlap of [1] aababaaba=aa with [2] aababaa=aabaaba:

aababaaba aababaa

Critical pair: aabaababa=aa.

Referenced by [4], [5].

[4] aabaa=aaaba

Overlap of [1] aababaaba=aa with [2] aababaa=aabaaba:

aabab aaba aababaa

Critical pair: aababaabaaba=aabaa.

Reduce LHS:

[2](aababaa)baaba
[3]⇒ (aabaababa)aba
⇒ aaaba

Flip LHS and RHS.

Defines rule #1.

Referenced by [5], [6].

[5] aaabababa=aa

Simplify [3] aabaababa=aa.

Reduce LHS:

[4](aabaa)baba
⇒ aaabababa

Defines rule #3.

[6] aababaa=aaababa

Simplify [2] aababaa=aabaaba.

Reduce RHS:

[4](aabaa)ba
⇒ aaababa

Defines rule #2.