Certificate for #15523 ⟨a, b | aaa=bb, ababa=a⟩

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

Completion settings:

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [6], [7], [8].

[2] ababa=a

Axiom: ababa=a.

Defines rule #5.

Referenced by [4], [8].

[3] aaab=baaa

Overlap of [1] bb=aaa with [1] bb=aaa:

b b bb

Critical pair: baaa=aaab.

Flip LHS and RHS.

Defines rule #3.

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

[4] babaaaa=aaa

Overlap of [3] aaab=baaa with [2] ababa=a:

aa ab ababa

Critical pair: aaa=baaaaba.

Reduce RHS:

[3]ba(aaab)a
⇒ babaaaa

Flip LHS and RHS.

Referenced by [5], [6].

[5] babaabaaa=abaaa

Overlap of [4] babaaaa=aaa with [3] aaab=baaa:

babaa aa aaab

Critical pair: babaabaaa=aaaab.

Reduce RHS:

[3]a(aaab)
⇒ abaaa

Referenced by [7].

[6] aabaaa=baaaaaaaaaa

Overlap of [4] babaaaa=aaa with [3] aaab=baaa:

babaaa a aaab

Critical pair: babaaabaaa=aaaaab.

Reduce LHS:

[3]bab(aaab)aaa
[1]⇒ ba(bb)aaaaaa
⇒ baaaaaaaaaa

Reduce RHS:

[3]aa(aaab)
⇒ aabaaa

Flip LHS and RHS.

Referenced by [7].

[7] abaaa=baaaaaaaaaaaaaa

Simplify [5] babaabaaa=abaaa.

Reduce LHS:

[6]bab(aabaaa)
[1]⇒ ba(bb)aaaaaaaaaa
⇒ baaaaaaaaaaaaaa

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[8] aaaaaaaaaaaaaaaaaa=aaa

Overlap of [2] ababa=a with [7] abaaa=baaaaaaaaaaaaaa:

ab aba abaaa

Critical pair: abbaaaaaaaaaaaaaa=aaa.

Reduce LHS:

[1]a(bb)aaaaaaaaaaaaaa
⇒ aaaaaaaaaaaaaaaaaa

Defines rule #1.