Certificate for #3390 ⟨a, b | aaaababbaa=a⟩

Back:⟨a, b | aaaababbaa=a⟩

Completion settings:

[1] aaaababbaa=a

Axiom: aaaababbaa=a.

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

[2] aaababbaa=aaaababba

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

aaaababb aa aaaababbaa

Critical pair: aaaababba=aaababbaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] ababbaa=aababba

Overlap of [2] aaababbaa=aaaababba with [2] aaababbaa=aaaababba:

aaababb aa aaababbaa

Critical pair: aaababbaaaababba=aaaababbaababbaa.

Reduce LHS:

[2](aaababbaa)aababba
[1]⇒ (aaaababbaa)ababba
⇒ aababba

Reduce RHS:

[1](aaaababbaa)babbaa
⇒ ababbaa

Flip LHS and RHS.

Defines rule #1.

[4] aaaaababba=a

Overlap of [1] aaaababbaa=a with [2] aaababbaa=aaaababba:

a aaababbaa aaababbaa

Critical pair: aaaaababba=a.

Defines rule #2.