Certificate for #3449 ⟨a, b | aaabaabbaa=a⟩

Back:⟨a, b | aaabaabbaa=a⟩

Completion settings:

[1] aaabaabbaa=a

Axiom: aaabaabbaa=a.

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

[2] aabaabbaa=aaabaabba

Overlap of [1] aaabaabbaa=a with [1] aaabaabbaa=a:

aaabaabb aa aaabaabbaa

Critical pair: aaabaabba=aabaabbaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] abaabbaa=aabaabba

Overlap of [1] aaabaabbaa=a with [2] aabaabbaa=aaabaabba:

aaabaabb aa aabaabbaa

Critical pair: aaabaabbaaabaabba=abaabbaa.

Reduce LHS:

[1](aaabaabbaa)abaabba
⇒ aabaabba

Flip LHS and RHS.

Defines rule #1.

[4] aaaabaabba=a

Overlap of [1] aaabaabbaa=a with [2] aabaabbaa=aaabaabba:

a aabaabbaa aabaabbaa

Critical pair: aaaabaabba=a.

Defines rule #2.