Certificate for #19673 ⟨a, b | aba=a, abbab=aa⟩

Back:⟨a, b | aba=a, abbab=aa⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #2.

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

[2] abbab=aa

Axiom: abbab=aa.

Referenced by [3], [4].

[3] abba=aaa

Overlap of [2] abbab=aa with [1] aba=a:

abb ab aba

Critical pair: abba=aaa.

Defines rule #4.

Referenced by [4].

[4] aab=aaaa

Overlap of [2] abbab=aa with [2] abbab=aa:

abb ab abbab

Critical pair: abbaa=aabab.

Reduce LHS:

[3](abba)a
⇒ aaaa

Reduce RHS:

[1]a(aba)b
⇒ aab

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] aaaaa=aa

Overlap of [4] aab=aaaa with [1] aba=a:

a ab aba

Critical pair: aa=aaaaa.

Flip LHS and RHS.

Defines rule #1.