Certificate for #27639 ⟨a, b | aa=1, ababab=bab

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [3], [5].

[2] ababab=bab

Axiom: ababab=bab.

Referenced by [3], [4].

[3] babab=abab

Overlap of [1] aa=1 with [2] ababab=bab:

a a ababab

Critical pair: abab=babab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] abbab=abab

Overlap of [2] ababab=bab with [2] ababab=bab:

ab abab ababab

Critical pair: abbab=babab.

Reduce RHS:

[3](babab)
abab

Referenced by [5].

[5] bbab=bab

Overlap of [1] aa=1 with [4] abbab=abab:

a a abbab

Critical pair: aabab=bbab.

Reduce LHS:

[1](aa)bab
bab

Flip LHS and RHS.

Defines rule #2.