Certificate for #5388 ⟨a, b | aab=ab, bba=ab⟩

Completion settings:

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

[1] aab=ab

Axiom: aab=ab.

Referenced by [3].

[2] ab=bba

Axiom: bba=ab.

Flip LHS and RHS.

Defines rule #2.

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

[3] aab=bba

Simplify [1] aab=ab.

Reduce RHS:

[2]	(ab)
	⇒ bba

Referenced by [4].

[4] bbbbaa=bba

Overlap of [3] aab=bba with [2] ab=bba:

a ab ab

Critical pair: abba=bba.

Reduce LHS:

[2]	(ab)ba
[2]	⇒ bb(ab)a
	⇒ bbbbaa

Referenced by [5], [6].

[5] bbbba=bba

Overlap of [2] ab=bba with [4] bbbbaa=bba:

a b bbbbaa

Critical pair: abba=bbabbbaa.

Reduce LHS:

[2]	(ab)ba
[2]	⇒ bb(ab)a
[4]	⇒ (bbbbaa)
	⇒ bba

Reduce RHS:

[2]	bb(ab)bbaa
[2]	⇒ bbbb(ab)baa
[2]	⇒ bbbbbb(ab)aa
[4]	⇒ bbbb(bbbbaa)a
[4]	⇒ bb(bbbbaa)
	⇒ bbbba

Flip LHS and RHS.

Defines rule #1.

Referenced by [6].

[6] bbaa=bba

Overlap of [4] bbbbaa=bba with [2] ab=bba:

bbbba a ab

Critical pair: bbbbabba=bbab.

Reduce LHS:

[5]	(bbbba)bba
[2]	⇒ bb(ab)ba
[5]	⇒ (bbbba)ba
[2]	⇒ bb(ab)a
[5]	⇒ (bbbba)a
	⇒ bbaa

Reduce RHS:

[2]	bb(ab)
[5]	⇒ (bbbba)
	⇒ bba

Defines rule #3.