Certificate for #14345 ⟨a, b | aaaa=a, abaab=a⟩

Back:⟨a, b | aaaa=a, abaab=a⟩

Completion settings:

[1] aaaa=a

Axiom: aaaa=a.

Defines rule #3.

Referenced by [4], [5].

[2] abaab=a

Axiom: abaab=a.

Referenced by [3], [5].

[3] abaa=aaab

Overlap of [2] abaab=a with [2] abaab=a:

aba ab abaab

Critical pair: abaa=aaab.

Referenced by [4].

[4] aba=aab

Overlap of [3] abaa=aaab with [1] aaaa=a:

ab aa aaaa

Critical pair: aba=aaabaa.

Reduce RHS:

[3]aa(abaa)
[1]⇒ (aaaa)ab
⇒ aab

Defines rule #1.

Referenced by [5].

[5] abb=aa

Overlap of [2] abaab=a with [4] aba=aab:

aba ab aba

Critical pair: abaaab=aa.

Reduce LHS:

[4](aba)aab
[4]⇒ a(aba)ab
[4]⇒ aa(aba)b
[1]⇒ (aaaa)bb
⇒ abb

Defines rule #2.