Certificate for #815 ⟨a, b | aabbaaba=b⟩

Completion settings:

• Reduction order:
  • Right-to-left shortlex with a < b

Axiom: aabbaaba=b.

Defines rule #1.

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

Overlap of [1] aabbaaba=b with [1] aabbaaba=b:

Critical pair: aabbaabb=babbaaba.

Defines rule #2.

Referenced by [3], [4].

Overlap of [2] aabbaabb=babbaaba with [1] aabbaaba=b:

Critical pair: aabbb=babbaabaaaba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6].

Overlap of [2] aabbaabb=babbaaba with [2] aabbaabb=babbaaba:

Critical pair: aabbbabbaaba=babbaabaaabb.

Flip LHS and RHS.

Defines rule #5.

Overlap of [1] aabbaaba=b with [3] babbaabaaaba=aabbb:

Critical pair: aabbaaaabbb=bbbaabaaaba.

Defines rule #3.

Overlap of [3] babbaabaaaba=aabbb with [3] babbaabaaaba=aabbb:

Critical pair: babbaabaaaaabbb=aabbbbbaabaaaba.

Defines rule #6.