Certificate for #12377 ⟨a, b | aaba=ab, bbbb=b⟩

Back:⟨a, b | aaba=ab, bbbb=b⟩

Completion settings:

[1] aaba=ab

Axiom: aaba=ab.

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

[2] bbbb=b

Axiom: bbbb=b.

Defines rule #4.

Referenced by [6], [7].

[3] ababa=abb

Overlap of [1] aaba=ab with [1] aaba=ab:

aab a aaba

Critical pair: aabab=ababa.

Reduce LHS:

[1](aaba)b
⇒ abb

Flip LHS and RHS.

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

[4] abba=aabb

Overlap of [1] aaba=ab with [3] ababa=abb:

a aba ababa

Critical pair: aabb=abba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [7].

[5] abbba=ababb

Overlap of [3] ababa=abb with [3] ababa=abb:

ab aba ababa

Critical pair: ababb=abbba.

Flip LHS and RHS.

Referenced by [8].

[6] aba=aab

Overlap of [3] ababa=abb with [4] abba=aabb:

abab a abba

Critical pair: ababaabb=abbbba.

Reduce LHS:

[3](ababa)abb
[4]⇒ (abba)bb
[2]⇒ aa(bbbb)
⇒ aab

Reduce RHS:

[2]a(bbbb)a
⇒ aba

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[7] aaab=ab

Overlap of [4] abba=aabb with [4] abba=aabb:

abb a abba

Critical pair: abbaabb=aabbbba.

Reduce LHS:

[4](abba)abb
[4]⇒ a(abba)bb
[2]⇒ aaa(bbbb)
⇒ aaab

Reduce RHS:

[2]aa(bbbb)a
[1]⇒ (aaba)
⇒ ab

Defines rule #2.

[8] abbba=aabbb

Simplify [5] abbba=ababb.

Reduce RHS:

[6](aba)bb
⇒ aabbb

Defines rule #5.