Certificate for #13123 ⟨a, b | aab=aaa, aba=bb⟩

Back:⟨a, b | aab=aaa, aba=bb⟩

Completion settings:

[1] aab=aaa

Axiom: aab=aaa.

Defines rule #2.

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

[2] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Defines rule #4.

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

[3] baba=abab

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

b b bb

Critical pair: baba=abab.

Defines rule #5.

Referenced by [5].

[4] aaaaa=aaaa

Overlap of [1] aab=aaa with [2] bb=aba:

aa b bb

Critical pair: aaaba=aaab.

Reduce LHS:

[1]a(aab)a
⇒ aaaaa

Reduce RHS:

[1]a(aab)
⇒ aaaa

Defines rule #1.

Referenced by [5], [6].

[5] abaaaa=baaaa

Overlap of [3] baba=abab with [3] baba=abab:

ba ba baba

Critical pair: baabab=ababba.

Reduce LHS:

[1]b(aab)ab
[1]⇒ baa(aab)
[4]⇒ b(aaaaa)
⇒ baaaa

Reduce RHS:

[2]aba(bb)a
[1]⇒ ab(aab)aa
[4]⇒ ab(aaaaa)
⇒ abaaaa

Flip LHS and RHS.

Referenced by [6].

[6] baaaa=aaaa

Overlap of [1] aab=aaa with [5] abaaaa=baaaa:

a ab abaaaa

Critical pair: abaaaa=aaaaaaa.

Reduce LHS:

[5](abaaaa)
⇒ baaaa

Reduce RHS:

[4](aaaaa)aa
[4]⇒ (aaaaa)a
[4]⇒ (aaaaa)
⇒ aaaa

Defines rule #3.