Certificate for #1669 ⟨a, b | aabaaabaa=a⟩

Back:⟨a, b | aabaaabaa=a⟩

Completion settings:

[1] aabaaabaa=a

Axiom: aabaaabaa=a.

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

[2] abaaabaa=aabaaaba

Overlap of [1] aabaaabaa=a with [1] aabaaabaa=a:

aabaaab aa aabaaabaa

Critical pair: aabaaaba=abaaabaa.

Flip LHS and RHS.

Defines rule #1.

Referenced by [3].

[3] abaaaabaaaba=abaa

Overlap of [2] abaaabaa=aabaaaba with [2] abaaabaa=aabaaaba:

abaa abaa abaaabaa

Critical pair: abaaaabaaaba=aabaaabaabaa.

Reduce RHS:

[1](aabaaabaa)baa
⇒ abaa

Referenced by [4].

[4] aaabaaaba=a

Overlap of [1] aabaaabaa=a with [3] abaaaabaaaba=abaa:

aabaa abaa abaaaabaaaba

Critical pair: aabaaabaa=aaabaaaba.

Reduce LHS:

[1](aabaaabaa)
⇒ a

Flip LHS and RHS.

Defines rule #2.