Certificate for #3624 ⟨a, b | aabbaaaaab=b⟩

Back:⟨a, b | aabbaaaaab=b⟩

Completion settings:

[1] aabbaaaaab=b

Axiom: aabbaaaaab=b.

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

[2] bbaaaaab=aabbaaab

Overlap of [1] aabbaaaaab=b with [1] aabbaaaaab=b:

aabbaaa aab aabbaaaaab

Critical pair: aabbaaab=bbaaaaab.

Flip LHS and RHS.

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

[3] bbaaab=aabbab

Overlap of [2] bbaaaaab=aabbaaab with [1] aabbaaaaab=b:

bbaaa aab aabbaaaaab

Critical pair: bbaaab=aabbaaabbaaaaab.

Reduce RHS:

[1]aabba(aabbaaaaab)
⇒ aabbab

Defines rule #1.

Referenced by [4], [5].

[4] aaaaaabbab=b

Overlap of [1] aabbaaaaab=b with [2] bbaaaaab=aabbaaab:

aa bbaaaaab bbaaaaab

Critical pair: aaaabbaaab=b.

Reduce LHS:

[3]aaaa(bbaaab)
⇒ aaaaaabbab

Defines rule #3.

[5] bbaaaaab=aaaabbab

Simplify [2] bbaaaaab=aabbaaab.

Reduce RHS:

[3]aa(bbaaab)
⇒ aaaabbab

Defines rule #2.