Certificate for #6536 ⟨a, b | aaa=a, aaba=bb⟩

Back:⟨a, b | aaa=a, aaba=bb⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

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

[2] bb=aaba

Axiom: aaba=bb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [6].

[3] baaba=aabab

Overlap of [2] bb=aaba with [2] bb=aaba:

b b bb

Critical pair: baaba=aabab.

Defines rule #3.

Referenced by [4], [6].

[4] aababaa=aabab

Overlap of [3] baaba=aabab with [1] aaa=a:

baab a aaa

Critical pair: baaba=aababaa.

Reduce LHS:

[3](baaba)
⇒ aabab

Flip LHS and RHS.

Referenced by [5].

[5] ababaa=abab

Overlap of [1] aaa=a with [4] aababaa=aabab:

a aa aababaa

Critical pair: aaabab=ababaa.

Reduce LHS:

[1](aaa)bab
⇒ abab

Flip LHS and RHS.

Defines rule #4.

Referenced by [6].

[6] ababab=abab

Overlap of [5] ababaa=abab with [3] baaba=aabab:

aba baa baaba

Critical pair: abaaabab=ababba.

Reduce LHS:

[1]ab(aaa)bab
⇒ ababab

Reduce RHS:

[2]aba(bb)a
[1]⇒ ab(aaa)baa
[5]⇒ (ababaa)
⇒ abab

Defines rule #5.