Certificate for #1122 ⟨a, b | ababba=aab

Completion settings:

[1] ababba=aab

Axiom: ababba=aab.

Defines rule #1.

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

[2] aabbabba=aabab

Overlap of [1] ababba=aab with [1] ababba=aab:

ababb a ababba

Critical pair: ababbaab=aabbabba.

Reduce LHS:

[1](ababba)ab
aabab

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [5].

[3] aababab=aaabbba

Overlap of [1] ababba=aab with [2] aabbabba=aabab:

ababb a aabbabba

Critical pair: ababbaabab=aababbabba.

Reduce LHS:

[1](ababba)abab
aababab

Reduce RHS:

[1]a(ababba)bba
aaabbba

Defines rule #2.

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

[4] aabaabbba=aaabbbaab

Overlap of [1] ababba=aab with [3] aababab=aaabbba:

ababb a aababab

Critical pair: ababbaaabbba=aabababab.

Reduce LHS:

[1](ababba)aabbba
aabaabbba

Reduce RHS:

[3](aababab)ab
aaabbbaab

Defines rule #5.

[5] aababaabbba=aaabbbaabab

Overlap of [2] aabbabba=aabab with [3] aababab=aaabbba:

aabbabb a aababab

Critical pair: aabbabbaaabbba=aababababab.

Reduce LHS:

[2](aabbabba)aabbba
aababaabbba

Reduce RHS:

[3](aababab)abab
aaabbbaabab

Defines rule #7.

[6] aaabbbaba=aabaab

Overlap of [3] aababab=aaabbba with [1] ababba=aab:

aab abab ababba

Critical pair: aabaab=aaabbbaba.

Flip LHS and RHS.

Defines rule #4.

[7] aaabbbaabba=aababaab

Overlap of [3] aababab=aaabbba with [1] ababba=aab:

aabab ab ababba

Critical pair: aababaab=aaabbbaabba.

Flip LHS and RHS.

Defines rule #6.