Certificate for #1664 ⟨a, b | aabaaaaab=b⟩

Back:⟨a, b | aabaaaaab=b⟩

Completion settings:

[1] aabaaaaab=b

Axiom: aabaaaaab=b.

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

[2] baaaaab=aabaaab

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

aabaaa aab aabaaaaab

Critical pair: aabaaab=baaaaab.

Flip LHS and RHS.

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

[3] baaab=aabab

Overlap of [2] baaaaab=aabaaab with [1] aabaaaaab=b:

baaa aab aabaaaaab

Critical pair: baaab=aabaaabaaaaab.

Reduce RHS:

[1]aaba(aabaaaaab)
⇒ aabab

Defines rule #1.

Referenced by [4], [5].

[4] aaaaaabab=b

Overlap of [1] aabaaaaab=b with [2] baaaaab=aabaaab:

aa baaaaab baaaaab

Critical pair: aaaabaaab=b.

Reduce LHS:

[3]aaaa(baaab)
⇒ aaaaaabab

Defines rule #3.

[5] baaaaab=aaaabab

Simplify [2] baaaaab=aabaaab.

Reduce RHS:

[3]aa(baaab)
⇒ aaaabab

Defines rule #2.