Certificate for #16098 ⟨a, b | aab=aa, abaa=ab⟩

Back:⟨a, b | aab=aa, abaa=ab⟩

Completion settings:

[1] aab=aa

Axiom: aab=aa.

Defines rule #1.

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

[2] abaa=ab

Axiom: abaa=ab.

Defines rule #4.

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

[3] aaaa=aa

Overlap of [1] aab=aa with [2] abaa=ab:

a ab abaa

Critical pair: aab=aaaa.

Reduce LHS:

[1](aab)
⇒ aa

Flip LHS and RHS.

Defines rule #3.

[4] abb=ab

Overlap of [2] abaa=ab with [1] aab=aa:

ab aa aab

Critical pair: abaa=abb.

Reduce LHS:

[2](abaa)
⇒ ab

Flip LHS and RHS.

Defines rule #2.

[5] abab=aba

Overlap of [2] abaa=ab with [1] aab=aa:

aba a aab

Critical pair: abaaa=abab.

Reduce LHS:

[2](abaa)a
⇒ aba

Flip LHS and RHS.

Defines rule #5.