Certificate for #3631 ⟨a, b | aabbaaabba=a⟩

Back:⟨a, b | aabbaaabba=a⟩

Completion settings:

[1] aabbaaabba=a

Axiom: aabbaaabba=a.

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

[2] aabbaa=aaabba

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

aabba aabba aabbaaabba

Critical pair: aabbaa=aaabba.

Referenced by [3], [4].

[3] aaaabbabba=a

Overlap of [1] aabbaaabba=a with [2] aabbaa=aaabba:

aabbaaabba aabbaa

Critical pair: aaabbaabba=a.

Reduce LHS:

[2]a(aabbaa)bba
⇒ aaaabbabba

Defines rule #2.

Referenced by [4].

[4] aaabbabbaa=a

Overlap of [2] aabbaa=aaabba with [2] aabbaa=aaabba:

aabb aa aabbaa

Critical pair: aabbaaabba=aaabbabbaa.

Reduce LHS:

[2](aabbaa)abba
[2]⇒ a(aabbaa)bba
[3]⇒ (aaaabbabba)
⇒ a

Flip LHS and RHS.

Referenced by [5].

[5] abbaa=aabba

Overlap of [1] aabbaaabba=a with [4] aaabbabbaa=a:

aabb aaabba aaabbabbaa

Critical pair: aabba=abbaa.

Flip LHS and RHS.

Defines rule #1.