Certificate for #16165 ⟨a, b | aab=ab, abab=aa⟩

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

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Defines rule #2.

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

[2] abab=aa

Axiom: abab=aa.

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

[3] aaa=aa

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

a ab abab

Critical pair: aaa=abab.

Reduce RHS:

[2](abab)
⇒ aa

Defines rule #1.

Referenced by [4], [6].

[4] abaa=ab

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

ab ab abab

Critical pair: abaa=aaab.

Reduce RHS:

[3](aaa)b
[1]⇒ (aab)
⇒ ab

Referenced by [5], [6].

[5] abb=aa

Overlap of [4] abaa=ab with [1] aab=ab:

ab aa aab

Critical pair: abab=abb.

Reduce LHS:

[2](abab)
⇒ aa

Flip LHS and RHS.

Defines rule #4.

[6] aba=ab

Overlap of [4] abaa=ab with [3] aaa=aa:

ab aa aaa

Critical pair: abaa=aba.

Reduce LHS:

[4](abaa)
⇒ ab

Flip LHS and RHS.

Defines rule #3.