  Order-sorted algebras and many sorted algebras exist in a long history with
many different implementations and applications. A lot of language
specifications have been defined in order-sorted algebra frameworks such as the
language specifications in K (an order-sorted algebra framework). The biggest
problem in a lot of the order-sorted algebra frameworks is that even if they
might allow developers to write programs and language specifications easily,
but they do not have a large set of tools to provide reasoning infrastructures
to reason about the specifications built on the frameworks, which are very
common in some many-sorted algebra framework such as Isabelle/HOL, Coq and FDR.
This fact brings us the necessity to marry the worlds of order-sorted algebras
and many sorted algebras. In this paper, we propose an algorithm to translate a
strictly sensible order-sorted algebra to a many-sorted one in a restricted
domain by requiring the order-sorted algebra to be strictly sensible. The key
idea of the translation is to add an equivalence relation called core equality
to the translated many-sorted algebras. By defining this relation, we reduce
the complexity of translating a strictly sensible order-sorted algebra to a
many-sorted one, make the translated many-sorted algebra equations only
increasing by a very small amount of new equations, and keep the number of
rewrite rules in the algebra in the same amount. We then prove the order-sorted
algebra and its translated many-sorted algebra are bisimilar. To the best of
our knowledge, our translation and bisimilar proof is the first attempt in
translating and relating an order-sorted algebra with a many-sorted one in a
way that keeps the size of the translated many-sorted algebra relatively small.
