Certificate for #4152 ⟨a, b | aabbaaaab=ab⟩

Back:⟨a, b | aabbaaaab=ab⟩

Completion settings:

[1] aabbaaaab=ab

Axiom: aabbaaaab=ab.

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

[2] abbaaaab=aabbaaab

Overlap of [1] aabbaaaab=ab with [1] aabbaaaab=ab:

aabbaa aab aabbaaaab

Critical pair: aabbaaab=abbaaaab.

Flip LHS and RHS.

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

[3] abbaaab=aabbaab

Overlap of [2] abbaaaab=aabbaaab with [1] aabbaaaab=ab:

abbaa aab aabbaaaab

Critical pair: abbaaab=aabbaaabbaaaab.

Reduce RHS:

[1]aabba(aabbaaaab)
⇒ aabbaab

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

[4] abbaab=aabbab

Overlap of [3] abbaaab=aabbaab with [1] aabbaaaab=ab:

abba aab aabbaaaab

Critical pair: abbaab=aabbaabbaaaab.

Reduce RHS:

[1]aabb(aabbaaaab)
⇒ aabbab

Defines rule #1.

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

[5] aaaaabbab=ab

Overlap of [1] aabbaaaab=ab with [2] abbaaaab=aabbaaab:

a abbaaaab abbaaaab

Critical pair: aaabbaaab=ab.

Reduce LHS:

[3]aa(abbaaab)
[4]⇒ aaa(abbaab)
⇒ aaaaabbab

Defines rule #4.

[6] abbaaaab=aaaabbab

Simplify [2] abbaaaab=aabbaaab.

Reduce RHS:

[3]a(abbaaab)
[4]⇒ aa(abbaab)
⇒ aaaabbab

Defines rule #3.

[7] abbaaab=aaabbab

Simplify [3] abbaaab=aabbaab.

Reduce RHS:

[4]a(abbaab)
⇒ aaabbab

Defines rule #2.