Certificate for #1642 ⟨a, b | aab=ba, bba=a⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(a) = 0; deg(b) = 1

[1] aab=ba

Axiom: aab=ba.

Referenced by [3], [4], [6], [8].

[2] bba=a

Axiom: bba=a.

Defines rule #3.

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

[3] baba=aaa

Overlap of [1] aab=ba with [2] bba=a:

aa b bba

Critical pair: aaa=baba.

Flip LHS and RHS.

Referenced by [4], [5].

[4] aaaaa=aa

Overlap of [1] aab=ba with [3] baba=aaa:

aa b baba

Critical pair: aaaaa=baaba.

Reduce RHS:

[1]	b(aab)a
[2]	⇒ (bba)a
	⇒ aa

Referenced by [6].

[5] aba=baaa

Overlap of [2] bba=a with [3] baba=aaa:

b ba baba

Critical pair: baaa=aba.

Flip LHS and RHS.

Referenced by [6].

[6] baaaa=ba

Overlap of [4] aaaaa=aa with [1] aab=ba:

aaa aa aab

Critical pair: aaaba=aab.

Reduce LHS:

[1]	a(aab)a
[5]	⇒ (aba)a
	⇒ baaaa

Reduce RHS:

[1]	(aab)
	⇒ ba

Referenced by [7].

[7] aaaa=a

Overlap of [2] bba=a with [6] baaaa=ba:

b ba baaaa

Critical pair: bba=aaaa.

Reduce LHS:

[2]	(bba)
	⇒ a

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[8] ab=baa

Overlap of [7] aaaa=a with [1] aab=ba:

aa aa aab

Critical pair: aaba=ab.

Reduce LHS:

[1]	(aab)a
	⇒ baa

Flip LHS and RHS.

Defines rule #2.