Certificate for #5324 ⟨a, b | abaabba=aaab

Completion settings:

[1] abaabba=aaab

Axiom: abaabba=aaab.

Defines rule #1.

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

[2] aaabbaabba=aaabaab

Overlap of [1] abaabba=aaab with [1] abaabba=aaab:

abaabb a abaabba

Critical pair: abaabbaaab=aaabbaabba.

Reduce LHS:

[1](abaabba)aab
aaabaab

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [5].

[3] aaabaabaab=aaaaababba

Overlap of [1] abaabba=aaab with [2] aaabbaabba=aaabaab:

abaabb a aaabbaabba

Critical pair: abaabbaaabaab=aaabaabbaabba.

Reduce LHS:

[1](abaabba)aabaab
aaabaabaab

Reduce RHS:

[1]aa(abaabba)abba
aaaaababba

Defines rule #2.

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

[4] aaabaaaababba=aaaaababbaaab

Overlap of [1] abaabba=aaab with [3] aaabaabaab=aaaaababba:

abaabb a aaabaabaab

Critical pair: abaabbaaaaababba=aaabaabaabaab.

Reduce LHS:

[1](abaabba)aaaababba
aaabaaaababba

Reduce RHS:

[3](aaabaabaab)aab
aaaaababbaaab

Defines rule #5.

[5] aaabaabaaaababba=aaaaababbaaabaab

Overlap of [2] aaabbaabba=aaabaab with [3] aaabaabaab=aaaaababba:

aaabbaabb a aaabaabaab

Critical pair: aaabbaabbaaaaababba=aaabaabaabaabaab.

Reduce LHS:

[2](aaabbaabba)aaaababba
aaabaabaaaababba

Reduce RHS:

[3](aaabaabaab)aabaab
aaaaababbaaabaab

Defines rule #7.

[6] aaaaababbaba=aaabaaaab

Overlap of [3] aaabaabaab=aaaaababba with [1] abaabba=aaab:

aaaba abaab abaabba

Critical pair: aaabaaaab=aaaaababbaba.

Flip LHS and RHS.

Defines rule #4.

[7] aaaaababbaaabba=aaabaabaaaab

Overlap of [3] aaabaabaab=aaaaababba with [1] abaabba=aaab:

aaabaaba ab abaabba

Critical pair: aaabaabaaaab=aaaaababbaaabba.

Flip LHS and RHS.

Defines rule #6.