Certificate for #3534 ⟨a, b | aabaaaaaab=b⟩

Back:⟨a, b | aabaaaaaab=b⟩

Completion settings:

[1] aabaaaaaab=b

Axiom: aabaaaaaab=b.

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

[2] baaaaaab=aabaaaab

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

aabaaaa aab aabaaaaaab

Critical pair: aabaaaab=baaaaaab.

Flip LHS and RHS.

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

[3] baaaab=aabaab

Overlap of [2] baaaaaab=aabaaaab with [1] aabaaaaaab=b:

baaaa aab aabaaaaaab

Critical pair: baaaab=aabaaaabaaaaaab.

Reduce RHS:

[1]aabaa(aabaaaaaab)
⇒ aabaab

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

[4] baab=aabb

Overlap of [3] baaaab=aabaab with [1] aabaaaaaab=b:

baa aab aabaaaaaab

Critical pair: baab=aabaabaaaaaab.

Reduce RHS:

[1]aab(aabaaaaaab)
⇒ aabb

Defines rule #1.

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

[5] aaaaaaaabb=b

Overlap of [1] aabaaaaaab=b with [2] baaaaaab=aabaaaab:

aa baaaaaab baaaaaab

Critical pair: aaaabaaaab=b.

Reduce LHS:

[3]aaaa(baaaab)
[4]⇒ aaaaaa(baab)
⇒ aaaaaaaabb

Defines rule #4.

[6] baaaaaab=aaaaaabb

Simplify [2] baaaaaab=aabaaaab.

Reduce RHS:

[3]aa(baaaab)
[4]⇒ aaaa(baab)
⇒ aaaaaabb

Defines rule #3.

[7] baaaab=aaaabb

Simplify [3] baaaab=aabaab.

Reduce RHS:

[4]aa(baab)
⇒ aaaabb

Defines rule #2.