Certificate for #790 ⟨a, b | aabaaaab=b⟩

Back:⟨a, b | aabaaaab=b⟩

Completion settings:

[1] aabaaaab=b

Axiom: aabaaaab=b.

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

[2] baaaab=aabaab

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

aabaa aab aabaaaab

Critical pair: aabaab=baaaab.

Flip LHS and RHS.

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

[3] baab=aabb

Overlap of [2] baaaab=aabaab with [1] aabaaaab=b:

baa aab aabaaaab

Critical pair: baab=aabaabaaaab.

Reduce RHS:

[1]aab(aabaaaab)
⇒ aabb

Defines rule #1.

Referenced by [4], [5].

[4] aaaaaabb=b

Overlap of [1] aabaaaab=b with [2] baaaab=aabaab:

aa baaaab baaaab

Critical pair: aaaabaab=b.

Reduce LHS:

[3]aaaa(baab)
⇒ aaaaaabb

Defines rule #3.

[5] baaaab=aaaabb

Simplify [2] baaaab=aabaab.

Reduce RHS:

[3]aa(baab)
⇒ aaaabb

Defines rule #2.