Decidability of equivalence of deterministic one-way multitape finite automata

I will present an old decidability result by Harju and Karhumäki, as in the title. The original proof involves some very nice algebraic constructions, which constitute the motivation for this presentation. We start from the well-known problem of deciding equivalence of one-dimensional linear recursive sequences (LRS) over a field. We then recall that decidability holds even for coefficients in a division ring (noncommutative field). Using Harju and Karhumäki's ingenious trick, we reduce two-tape finite automata to one-dimensional LRS over a suitable division ring. The construction of the division ring is the crux of the approach: it relies on the existence of a total ordering of the free group, which is a nontrivial result.