Certificate for #10807 ⟨a, b | aaba=aab, bbbb=1⟩

Back:⟨a, b | aaba=aab, bbbb=1⟩

Completion settings:

[1] aaba=aab

Axiom: aaba=aab.

Defines rule #2.

Referenced by [3], [4].

[2] bbbb=1

Axiom: bbbb=1.

Defines rule #3.

Referenced by [5].

[3] aabba=aabb

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

aab a aaba

Critical pair: aabaab=aababa.

Reduce LHS:

[1](aaba)ab
[1]⇒ (aaba)b
⇒ aabb

Reduce RHS:

[1](aaba)ba
⇒ aabba

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] aabbba=aabbb

Overlap of [1] aaba=aab with [3] aabba=aabb:

aab a aabba

Critical pair: aabaabb=aababba.

Reduce LHS:

[1](aaba)abb
[1]⇒ (aaba)bb
⇒ aabbb

Reduce RHS:

[1](aaba)bba
⇒ aabbba

Flip LHS and RHS.

Defines rule #5.

[5] aaa=aa

Overlap of [3] aabba=aabb with [3] aabba=aabb:

aabb a aabba

Critical pair: aabbaabb=aabbabba.

Reduce LHS:

[3](aabba)abb
[3]⇒ (aabba)bb
[2]⇒ aa(bbbb)
⇒ aa

Reduce RHS:

[3](aabba)bba
[2]⇒ aa(bbbb)a
⇒ aaa

Flip LHS and RHS.

Defines rule #1.