Certificate for #12514 ⟨a, b | abab=aa, bbba=a⟩

Back:⟨a, b | abab=aa, bbba=a⟩

Completion settings:

[1] abab=aa

Axiom: abab=aa.

Defines rule #2.

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

[2] bbba=a

Axiom: bbba=a.

Defines rule #3.

Referenced by [4].

[3] abaa=aaab

Overlap of [1] abab=aa with [1] abab=aa:

ab ab abab

Critical pair: abaa=aaab.

Defines rule #1.

Referenced by [4], [5].

[4] aabba=aaab

Overlap of [1] abab=aa with [2] bbba=a:

aba b bbba

Critical pair: abaa=aabba.

Reduce LHS:

[3](abaa)
⇒ aaab

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] aaaabb=aaaba

Overlap of [3] abaa=aaab with [1] abab=aa:

aba a abab

Critical pair: abaaa=aaabbab.

Reduce LHS:

[3](abaa)a
⇒ aaaba

Reduce RHS:

[4]a(aabba)b
⇒ aaaabb

Flip LHS and RHS.

Defines rule #5.